From ed7edf5661ebc5cb5fa76c0d84810255ff55c417 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 19 Aug 2020 12:09:42 +0200
Subject: [PATCH] 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                | 32 ++++++++++++++++++++---
 src/Lean/PrettyPrinter/Parenthesizer.lean |  6 +++++
 2 files changed, 35 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index e04d58825e..4b1d7c3a3d 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/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
 
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index 02feef5345..9c1089543b 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/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