From 1fcdbaf223ca594f48e7bc8742d8efe47e267a5a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 28 Sep 2020 11:28:48 -0700
Subject: [PATCH] feat: add `withoutPosition` combinator

---
 src/Lean/Parser/Basic.lean                | 28 ++++++++++++++++-------
 src/Lean/PrettyPrinter/Formatter.lean     |  2 ++
 src/Lean/PrettyPrinter/Parenthesizer.lean |  2 ++
 3 files changed, 24 insertions(+), 8 deletions(-)

diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 32012ec56d..6538907c8d 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -125,7 +125,7 @@ structure ParserContext extends InputContext :=
 (env        : Environment)
 (tokens     : TokenTable)
 (insideQuot : Bool := false)
-(savedPos   : Position := { line := 1, column := 0 })
+(savedPos?  : Option Position := none)
 
 structure Error :=
 (unexpected : String := "")
@@ -1377,18 +1377,24 @@ def anyOfFn : List Parser → ParserFn
 
 @[inline] def checkColGeFn (errorMsg : String) : ParserFn :=
 fun c s =>
-  let pos := c.fileMap.toPosition s.pos;
-  if pos.column ≥ c.savedPos.column then s
-  else s.mkError errorMsg
+  match c.savedPos? with
+  | none => s
+  | some savedPos =>
+    let pos := c.fileMap.toPosition s.pos;
+    if pos.column ≥ savedPos.column then s
+    else s.mkError errorMsg
 
 @[inline] def checkColGe (errorMsg : String) : Parser :=
 { fn := checkColGeFn errorMsg }
 
 @[inline] def checkColGtFn (errorMsg : String) : ParserFn :=
 fun c s =>
-  let pos := c.fileMap.toPosition s.pos;
-  if pos.column > c.savedPos.column then s
-  else s.mkError errorMsg
+  match c.savedPos? with
+  | none => s
+  | some savedPos =>
+    let pos := c.fileMap.toPosition s.pos;
+    if pos.column > savedPos.column then s
+    else s.mkError errorMsg
 
 @[inline] def checkColGt (errorMsg : String) : Parser :=
 { fn := checkColGtFn errorMsg }
@@ -1397,7 +1403,13 @@ fun c s =>
 { info := p.info,
   fn   := fun c s =>
    let pos := c.fileMap.toPosition s.pos;
-   p.fn { c with savedPos := pos } s }
+   p.fn { c with savedPos? := pos } s }
+
+@[inline] def withoutPosition (p : Parser) : Parser :=
+{ info := p.info,
+  fn   := fun c s =>
+   let pos := c.fileMap.toPosition s.pos;
+   p.fn { c with savedPos? := none } s }
 
 def eoiFn : ParserFn :=
 fun c s =>
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 079887373c..ed6665bc07 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -367,6 +367,8 @@ else
 
 @[combinatorFormatter Lean.Parser.withPosition] def withPosition.formatter (p : Formatter) : Formatter := do
 p
+@[combinatorFormatter Lean.Parser.withoutPosition] def withoutPosition.formatter (p : Formatter) : Formatter := do
+p
 
 @[combinatorFormatter Lean.Parser.setExpected]
 def setExpected.formatter (expected : List String) (p : Formatter) : Formatter :=
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index e78d7632a8..77a566a09a 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -432,6 +432,8 @@ else
 
 @[combinatorParenthesizer Lean.Parser.withPosition] def withPosition.parenthesizer (p : Parenthesizer) : Parenthesizer := do
 p
+@[combinatorParenthesizer Lean.Parser.withoutPosition] def withoutPosition.parenthesizer (p : Parenthesizer) : Parenthesizer := do
+p
 
 @[combinatorParenthesizer Lean.Parser.setExpected]
 def setExpected.parenthesizer (expected : List String) (p : Parenthesizer) : Parenthesizer :=