diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean
index 0d0dd7dd13..17dd6d2aef 100644
--- a/src/Init/Data/String/Basic.lean
+++ b/src/Init/Data/String/Basic.lean
@@ -515,6 +515,12 @@ def replace (s pattern replacement : String) : String :=
       termination_by s.endPos.1 - pos.1
     loop "" 0 0
 
+/-- Return the beginning of the line that contains character `pos`. -/
+def findLineStart (s : String) (pos : String.Pos) : String.Pos :=
+  match s.revFindAux (· = '\n') pos with
+  | none => 0
+  | some n => ⟨n.byteIdx + 1⟩
+
 end String
 
 namespace Substring
diff --git a/src/Lean/Data/Position.lean b/src/Lean/Data/Position.lean
index aba88c65ca..73780c72c8 100644
--- a/src/Lean/Data/Position.lean
+++ b/src/Lean/Data/Position.lean
@@ -84,6 +84,26 @@ partial def toPosition (fmap : FileMap) (pos : String.Pos) : Position :=
       -- Can also happen with EOF errors, which are not strictly inside the file.
       ⟨lines.back, (pos - ps.back).byteIdx⟩
 
+/-- Convert a `Lean.Position` to a `String.Pos`. -/
+def ofPosition (text : FileMap) (pos : Position) : String.Pos :=
+  let colPos :=
+    if h : pos.line - 1 < text.positions.size then
+      text.positions.get ⟨pos.line - 1, h⟩
+    else if text.positions.isEmpty then
+      0
+    else
+      text.positions.back
+  String.Iterator.nextn ⟨text.source, colPos⟩ pos.column |>.pos
+
+/--
+Returns the position of the start of (1-based) line `line`.
+This gives the stame result as `map.ofPosition ⟨line, 0⟩`, but is more efficient.
+-/
+def lineStart (map : FileMap) (line : Nat) : String.Pos :=
+  if h : line - 1 < map.positions.size then
+    map.positions.get ⟨line - 1, h⟩
+  else map.positions.back?.getD 0
+
 end FileMap
 end Lean
 
diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean
index 9c70b5a0f9..a0ef020fac 100644
--- a/src/Lean/Syntax.lean
+++ b/src/Lean/Syntax.lean
@@ -305,6 +305,10 @@ def getRange? (stx : Syntax) (canonicalOnly := false) : Option String.Range :=
   | some start, some stop => some { start, stop }
   | _,          _         => none
 
+/-- Returns a synthetic Syntax which has the specified `String.Range`. -/
+def ofRange (range : String.Range) (canonical := true) : Lean.Syntax :=
+  .atom (.synthetic range.start range.stop canonical) ""
+
 /--
 Represents a cursor into a syntax tree that can be read, written, and advanced down/up/left/right.
 Indices are allowed to be out-of-bound, in which case `cur` is `Syntax.missing`.