feat: add checkInsideQuot/checkOutsideQuot/toggleInsideQuot parsers

One use case is to obtain fine-grained control over at what stage changed syntax is activated

src/Lean/Parser/Basic.lean

@@ -120,9 +120,10 @@ instance InputContext.inhabited : Inhabited InputContext :=
 ⟨{ input := "", fileName := "", fileMap := arbitrary _ }⟩
 
 structure ParserContext extends InputContext :=
-(prec     : Nat)
-(env      : Environment)
-(tokens   : TokenTable)
+(prec       : Nat)
+(env        : Environment)
+(tokens     : TokenTable)
+(insideQuot : Bool := false)
 
 structure Error :=
 (unexpected : String := "")
@@ -360,6 +361,31 @@ fun c s =>
 { info := epsilonInfo,
   fn   := checkPrecFn prec }
 
+def checkInsideQuotFn : ParserFn :=
+fun c s =>
+  if c.insideQuot then s
+  else s.mkUnexpectedError "unexpected syntax outside syntax quotation"
+
+@[inline] def checkInsideQuot : Parser :=
+{ info := epsilonInfo,
+  fn   := checkInsideQuotFn }
+
+def checkOutsideQuotFn : ParserFn :=
+fun c s =>
+  if !c.insideQuot then s
+  else s.mkUnexpectedError "unexpected syntax inside syntax quotation"
+
+@[inline] def checkOutsideQuot : Parser :=
+{ info := epsilonInfo,
+  fn   := checkOutsideQuotFn }
+
+def toggleInsideQuotFn (p : ParserFn) : ParserFn :=
+fun c s => p { c with insideQuot := !c.insideQuot } s
+
+@[inline] def toggleInsideQuot (p : Parser) : Parser :=
+{ info := epsilonInfo,
+  fn   := toggleInsideQuotFn p.fn }
+
 @[inline] def leadingNode (n : SyntaxNodeKind) (prec : Nat) (p : Parser) : Parser :=
 checkPrec prec >> node n p
 

src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -406,12 +406,18 @@ p ⟨0, 0⟩
 def setExpected.parenthesizer (expected : List String) (p : Parenthesizer) : Parenthesizer :=
 p
 
+@[combinatorParenthesizer Lean.Parser.toggleInsideQuot]
+def toggleInsideQuot.parenthesizer (p : Parenthesizer) : Parenthesizer :=
+p
+
 @[combinatorParenthesizer Lean.Parser.checkStackTop] def checkStackTop.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.checkWsBefore] def checkWsBefore.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.checkNoWsBefore] def checkNoWsBefore.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.checkTailWs] def checkTailWs.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.checkColGe] def checkColGe.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.checkNoImmediateColon] def checkNoImmediateColon.parenthesizer : Parenthesizer := pure ()
+@[combinatorParenthesizer Lean.Parser.checkInsideQuot] def checkInsideQuot.parenthesizer : Parenthesizer := pure ()
+@[combinatorParenthesizer Lean.Parser.checkOutsideQuot] def checkOutsideQuot.parenthesizer : Parenthesizer := pure ()
 
 @[combinatorParenthesizer Lean.Parser.pushNone] def pushNone.parenthesizer : Parenthesizer := goLeft