refinements/fixes from Marc review

src/Lean/Meta/Sorry.lean

@@ -11,16 +11,27 @@ import Lean.Util.Recognizers
 /-!
 # Utilities for creating and recognizing `sorry`
 
-This module
+This module develops material for creating and recognizing `sorryAx` terms that encode originating source positions.
+There are three orthogonal configurations for sorries:
+
+- The sorry could be *synthetic*. When elaboration fails on some subterm, then we can use a sorry to fill in the missing subterm.
+  In this case elaboration marks the sorry as being "synthetic" while logging an error.
+  The presence of synthetic sorries tends to suppress further errors. For example, the "this declaration contains sorry" error
+  is not triggered for synthetic sorries as we assume there is already an error message logged.
+
+- The sorry could be *unique*. A unique sorry is not definitionally equal to any other sorry, even if they have the same type.
+  Normally `sorryAx α s = sorryAx α s` is a definitional equality. Unique sorries insert a unique tag `t` using the encoding `sorryAx (τ → α) s t`.
+
+- The sorry could be *labeled*. A labeled sorry contains source position information, supporting the LSP "go to definition" feature in the Infoview,
+  and also supporting pretty printing the sorry with an indication of source position when the option `pp.sorrySource` is true.
 -/
 
 namespace Lean.Meta
 
 /--
 Returns `sorryAx type synthetic`. Recall that `synthetic` is true if this sorry is from an error.
 
-See also `Lean.Meta.mkLabeledSorry`, for creating a `sorry` that encodes the origin position of the `sorry`,
-and which has facilities for making a `sorry` that is not defeq to any other `sorry`.
+See also `Lean.Meta.mkLabeledSorry`, for creating a `sorry` that is labeled or unique.
 -/
 def mkSorry (type : Expr) (synthetic : Bool) : MetaM Expr := do
   let u ← getLevel type
@@ -30,7 +41,7 @@ structure SorryLabelView where
   /--
   Records the origin module name, logical source position, and LSP range for the `sorry`.
   The logical source position is used when displaying the sorry when the `pp.sorrySource` option is true,
-  and the LSP range is used for "go to definition".
+  and the LSP range is used for "go to definition" in the Infoview.
   -/
   module? : Option (Name × Position × Lsp.Range) := none
 
@@ -51,8 +62,12 @@ def SorryLabelView.decode? (name : Name) : Option SorryLabelView := do
     failure
 
 /--
-Makes a `sorryAx` that encodes the current ref into the term to support "go to definition" for the `sorry`.
-If `unique` is true, the `sorry` is unique, in the sense that it is not defeq to any other `sorry` created by `mkLabeledSorry`.
+Constructs a `sorryAx`.
+* If the current ref has a source position, then creates a labeled sorry.
+  This supports "go to definition" in the InfoView and pretty printing a source position when the `pp.sorrySource` option is true.
+* If `synthetic` is true, then the `sorry` is regarded as being generated by the elaborator.
+  The caller should ensure that there is an associated error logged.
+* If `unique` is true, the `sorry` is unique, in the sense that it is not defeq to any other `sorry` created by `mkLabeledSorry`.
 -/
 def mkLabeledSorry (type : Expr) (synthetic : Bool) (unique : Bool) : MetaM Expr := do
   let tag ←

src/Lean/Parser/Term.lean

@@ -223,7 +223,7 @@ Lean will give a warning whenever a declaration uses `sorry`, so you aren't like
 but you can double check if a declaration depends on `sorry` by looking for `sorryAx` in the output
 of the `#print axioms my_thm` command, the axiom used by the implementation of `sorry`.
 
-"Go to definition" on `sorry` will go to the source position where it was introduced.
+"Go to definition" on `sorry` in the Infoview will go to the source position where it was introduced, if such information is available.
 
 Each `sorry` is guaranteed to be unique, so for example the following fails:
 ```lean

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -321,7 +321,7 @@ def OmissionReason.toString : OmissionReason → String
   | maxSteps => "Term omitted due to reaching the maximum number of steps allowed for pretty printing this expression (see option `pp.maxSteps`)."
 
 def addOmissionInfo (pos : Pos) (stx : Syntax) (e : Expr) (reason : OmissionReason) : DelabM Unit := do
-  addDelabTermInfo pos stx e (docString? := reason.toString) (explicit := true)
+  addDelabTermInfo pos stx e (docString? := reason.toString) (explicit := false)
 
 /--
 Runs the delaborator `act` with increased depth.

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -166,8 +166,8 @@ def locationLinksOfInfo (kind : GoToKind) (ictx : InfoWithCtx)
     let mut expr := ti.expr
     if kind == type then
       expr ← ci.runMetaM i.lctx do
-        return Expr.getAppFn (← instantiateMVars (← Meta.inferType expr)) |>.consumeMData
-    match expr with
+        return Expr.getAppFn (← instantiateMVars (← Meta.inferType expr))
+    match expr.consumeMData with
     | Expr.const n .. => return ← ci.runMetaM i.lctx <| locationLinksFromDecl i n
     | Expr.fvar id .. => return ← ci.runMetaM i.lctx <| locationLinksFromBinder i id
     | _ => pure ()
@@ -212,15 +212,17 @@ def locationLinksOfInfo (kind : GoToKind) (ictx : InfoWithCtx)
     locationLinksDefault
 
   match i with
-  | .ofDelabTermInfo { location? := some (module, range), .. } =>
-    let targetUri := (← documentUriFromModule rc.srcSearchPath module).getD doc.meta.uri
-    let result : LocationLink := {
-      targetUri, targetRange := range, targetSelectionRange := range,
-      originSelectionRange? := (·.toLspRange text) <$> i.range?
-    }
-    return #[result]
-  | .ofTermInfo ti
-  | .ofDelabTermInfo { toTermInfo := ti } =>
+  | .ofTermInfo ti =>
+    return ← locationLinksFromTermInfo ti
+  | .ofDelabTermInfo { toTermInfo := ti, location?, .. } =>
+    if let some (module, range) := location? then
+      if let some targetUri ← documentUriFromModule rc.srcSearchPath module then
+        let result : LocationLink := {
+          targetUri, targetRange := range, targetSelectionRange := range,
+          originSelectionRange? := (·.toLspRange text) <$> i.range?
+        }
+        return #[result]
+      -- If we fail to find a DocumentUri, fall through and use the default method to at least try to have something to jump to.
     return ← locationLinksFromTermInfo ti
   | .ofFieldInfo fi =>
     if kind == type then