From 995f71cf4e54387334b65621ef211ffd438d048e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 13 Aug 2019 14:32:14 -0700
Subject: [PATCH] feat(library/init/lean/elaborator/preterm): add `setPos`

---
 library/init/lean/elaborator/preterm.lean | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/library/init/lean/elaborator/preterm.lean b/library/init/lean/elaborator/preterm.lean
index ccd49e9d37..d9887cf8c5 100644
--- a/library/init/lean/elaborator/preterm.lean
+++ b/library/init/lean/elaborator/preterm.lean
@@ -79,6 +79,16 @@ partial def toLevel : Syntax → Elab Level
      pure $ level.addOffset k
   | other => throw "unexpected universe level syntax"
 
+private def setPos (stx : Syntax) (p : PreTerm) : Elab PreTerm :=
+if stx.isOfKind `Lean.Parser.Term.app then pure p
+else do
+  cfg ← read;
+  match stx.getPos with
+  | none => pure p
+  | some pos =>
+    let pos := cfg.fileMap.toPosition pos;
+    pure $ Expr.mdata ((MData.empty.setNat `column pos.column).setNat `row pos.line) p
+
 def toPreTerm (stx : Syntax) : Elab PreTerm :=
 stx.ifNode
   (fun n => do
@@ -86,7 +96,7 @@ stx.ifNode
     table ← runIO builtinPreTermElabTable.get;
     let k      := n.getKind;
     match table.find k with
-    | some fn => fn n
+    | some fn => fn n >>= setPos stx
     | none    => logErrorAndThrow stx ("`toPreTerm` failed, no support for syntax '" ++ toString k ++ "'"))
   (fun _ => throw "`toPreTerm` failed, unexpected syntax")