From 3d891be49e0d5f55141cb402100bb760c5317d6f Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 14 May 2020 19:02:48 +0200
Subject: [PATCH] feat: delaborator: do not set whitespace information

---
 src/Init/Lean/Delaborator.lean        | 7 ++-----
 src/Init/Lean/Elab/Binders.lean       | 2 +-
 src/Init/Lean/Elab/Util.lean          | 2 +-
 src/Init/Lean/Syntax.lean             | 2 +-
 tests/lean/run/CommandExtOverlap.lean | 2 +-
 tests/lean/run/tacticExtOverlap.lean  | 2 +-
 6 files changed, 7 insertions(+), 10 deletions(-)

diff --git a/src/Init/Lean/Delaborator.lean b/src/Init/Lean/Delaborator.lean
index 4b02a91874..6d1e159663 100644
--- a/src/Init/Lean/Delaborator.lean
+++ b/src/Init/Lean/Delaborator.lean
@@ -194,11 +194,8 @@ def withProj {α} (d : DelabM α) : DelabM α := do
 Expr.app fn _ _ ← getExpr | unreachable!;
 descend fn 0 d
 
-def infoForPos (pos : Nat) : SourceInfo :=
-{ leading := " ".toSubstring, pos := pos, trailing := " ".toSubstring }
-
 partial def annotatePos (pos : Nat) : Syntax → Syntax
-| stx@(Syntax.ident _ _ _ _)                   => stx.setInfo (infoForPos pos)
+| stx@(Syntax.ident _ _ _ _)                   => stx.setInfo { pos := pos }
 -- Term.ids => annotate ident
 -- TODO: universes?
 | stx@(Syntax.node `Lean.Parser.Term.id args)  => stx.modifyArg 0 annotatePos
@@ -206,7 +203,7 @@ partial def annotatePos (pos : Nat) : Syntax → Syntax
 | stx@(Syntax.node `Lean.Parser.Term.app args) => stx.modifyArg 0 annotatePos
 -- otherwise, annotate first direct child token if any
 | stx => match stx.getArgs.findIdx? Syntax.isAtom with
-  | some idx => stx.modifyArg idx (Syntax.setInfo (infoForPos pos))
+  | some idx => stx.modifyArg idx (Syntax.setInfo { pos := pos })
   | none     => stx
 
 def annotateCurPos (stx : Syntax) : Delab := do
diff --git a/src/Init/Lean/Elab/Binders.lean b/src/Init/Lean/Elab/Binders.lean
index 8231a0b21d..5f44fc0451 100644
--- a/src/Init/Lean/Elab/Binders.lean
+++ b/src/Init/Lean/Elab/Binders.lean
@@ -52,7 +52,7 @@ partial def quoteAutoTactic : Syntax → TermElabM Syntax
         arg ← quoteAutoTactic arg;
         `(Array.push $args $arg)) empty;
     `(Syntax.node $(quote k) $args)
-| Syntax.atom info val => `(Syntax.atom none $(quote val))
+| Syntax.atom info val => `(Syntax.atom {} $(quote val))
 | Syntax.missing       => unreachable!
 
 def declareTacticSyntax (tactic : Syntax) : TermElabM Name :=
diff --git a/src/Init/Lean/Elab/Util.lean b/src/Init/Lean/Elab/Util.lean
index c8670e0ffc..9594f77402 100644
--- a/src/Init/Lean/Elab/Util.lean
+++ b/src/Init/Lean/Elab/Util.lean
@@ -11,7 +11,7 @@ import Init.Lean.KeyedDeclsAttribute
 namespace Lean
 
 def Syntax.prettyPrint (stx : Syntax) : Format :=
-match stx.truncateTrailing.reprint with -- TODO use syntax pretty printer
+match stx.unsetTrailing.reprint with -- TODO use syntax pretty printer
 | some str => format str.toFormat
 | none     => format stx
 
diff --git a/src/Init/Lean/Syntax.lean b/src/Init/Lean/Syntax.lean
index 6353100763..1ff8e957b5 100644
--- a/src/Init/Lean/Syntax.lean
+++ b/src/Init/Lean/Syntax.lean
@@ -214,7 +214,7 @@ match setTailInfoAux info stx with
 | some stx => stx
 | none     => stx
 
-def truncateTrailing (stx : Syntax) : Syntax :=
+def unsetTrailing (stx : Syntax) : Syntax :=
 match stx.getTailInfo with
 | none      => stx
 | some info => stx.setTailInfo { info with trailing := none }
diff --git a/tests/lean/run/CommandExtOverlap.lean b/tests/lean/run/CommandExtOverlap.lean
index c93741b2a8..551984dfe5 100644
--- a/tests/lean/run/CommandExtOverlap.lean
+++ b/tests/lean/run/CommandExtOverlap.lean
@@ -6,7 +6,7 @@ open Lean
 
 macro_rules [mycheck]
 | `(#check $es*) =>
-  let cmds := es.getSepElems.map $ fun e => Syntax.node `Lean.Parser.Command.check #[Syntax.atom none "#check", e];
+  let cmds := es.getSepElems.map $ fun e => Syntax.node `Lean.Parser.Command.check #[Syntax.atom {} "#check", e];
   pure $ mkNullNode cmds
 
 #check true
diff --git a/tests/lean/run/tacticExtOverlap.lean b/tests/lean/run/tacticExtOverlap.lean
index befde51446..35a844170a 100644
--- a/tests/lean/run/tacticExtOverlap.lean
+++ b/tests/lean/run/tacticExtOverlap.lean
@@ -5,7 +5,7 @@ open Lean
 syntax [myintro] "intros" (sepBy ident ",") : tactic
 
 macro_rules [myintro]
-| `(tactic| intros $x*) => pure $ Syntax.node `Lean.Parser.Tactic.intros #[Syntax.atom none "intros", mkNullNode x.getSepElems]
+| `(tactic| intros $x*) => pure $ Syntax.node `Lean.Parser.Tactic.intros #[Syntax.atom {} "intros", mkNullNode x.getSepElems]
 
 theorem tst1 {p q : Prop} : p → q → p :=
 begin