From 7aca461a35fc3f593cf407e0b589579a13998010 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Wed, 14 Jul 2021 13:43:11 -0700 Subject: [PATCH] fix: hovers on elabFieldName fields --- src/Init/Data/Format/Syntax.lean | 2 +- src/Lean/Elab/App.lean | 14 ++++++++++---- src/Lean/Syntax.lean | 18 ++++++++++++++++++ .../interactive/hoverDot.lean.expected.out | 14 ++++++++------ 4 files changed, 37 insertions(+), 11 deletions(-) diff --git a/src/Init/Data/Format/Syntax.lean b/src/Init/Data/Format/Syntax.lean index bda8e9ae84..818c912c5f 100644 --- a/src/Init/Data/Format/Syntax.lean +++ b/src/Init/Data/Format/Syntax.lean @@ -15,7 +15,7 @@ open Std.Format private def formatInfo (showInfo : Bool) (info : SourceInfo) (f : Format) : Format := match showInfo, info with - | true, SourceInfo.original lead pos trail endPos => f!"{lead}:{f}:{pos}:{trail}:{endPos}" + | true, SourceInfo.original lead pos trail endPos => f!"{lead}:{pos}:{f}:{endPos}:{trail}" | true, SourceInfo.synthetic pos endPos => f!"{pos}:{f}:{endPos}" | _, _ => f diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 4c7342378a..185c09ea54 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -673,7 +673,7 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp | f, [] => elabAppArgs f namedArgs args expectedType? explicit ellipsis | f, lval::lvals => do if let LVal.fieldName (ref := fieldStx) (targetStx := targetStx) .. := lval then - addDotCompletionInfo targetStx f expectedType? fieldStx + addDotCompletionInfo targetStx f expectedType? fieldStx let (f, lvalRes) ← resolveLVal f lval match lvalRes with | LValResolution.projIdx structName idx => @@ -785,9 +785,15 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra f.getArgs.foldlM (fun acc f => elabAppFn f lvals namedArgs args expectedType? explicit ellipsis true acc) acc else let elabFieldName (e field : Syntax) := do - let newLVals := field.getId.eraseMacroScopes.components.map fun n => - -- We use `none` here since `field` can't be part of a composite name - LVal.fieldName field (toString n) none e + let newLVals := + -- We use `none` in `suffix?` since `field` can't be part of a composite name + if field.getId.hasMacroScopes then + -- We assume that names with macro scopes have no meaningful syntax associated + field.getId.eraseMacroScopes.components.map fun n => + LVal.fieldName Syntax.missing (toString n) none e + else + field.identComponents.map fun comp => + LVal.fieldName comp (toString comp.getId) none e elabAppFn e (newLVals ++ lvals) namedArgs args expectedType? explicit ellipsis overloaded acc let elabFieldIdx (e idxStx : Syntax) := do let idx := idxStx.isFieldIdx?.get! diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean index e98e1088bc..c7075b008c 100644 --- a/src/Lean/Syntax.lean +++ b/src/Lean/Syntax.lean @@ -172,6 +172,24 @@ partial def getTailWithPos : Syntax → Option Syntax | node _ args => args.findSomeRev? getTailWithPos | _ => none +open SourceInfo in +/-- Splits an `ident` into its dot-separated components while preserving source info. +For example, `` `foo.bla.boo `` ↦ `` [`foo, `bla, `boo] ``. -/ +def identComponents : Syntax → List Syntax + | ident info rawStr val _ => + rawStr.splitOn "." |>.map fun ss => + let off := ss.startPos - rawStr.startPos + let info := match info with + | original lead pos trail _ => + let lead := if off == 0 then lead else "".toSubstring + let trail := if ss.stopPos == rawStr.stopPos then trail else "".toSubstring + original lead (pos + off) trail (pos + off + ss.bsize) + | synthetic pos _ => + synthetic (pos + off) (pos + off + ss.bsize) + | SourceInfo.none => SourceInfo.none + ident info ss (Name.mkSimple ss.toString) [] + | _ => unreachable! + structure TopDown where firstChoiceOnly : Bool stx : Syntax diff --git a/tests/lean/interactive/hoverDot.lean.expected.out b/tests/lean/interactive/hoverDot.lean.expected.out index a444dacddd..7adb2e511f 100644 --- a/tests/lean/interactive/hoverDot.lean.expected.out +++ b/tests/lean/interactive/hoverDot.lean.expected.out @@ -28,20 +28,22 @@ {"textDocument": {"uri": "file://hoverDot.lean"}, "position": {"line": 18, "character": 13}} {"range": - {"start": {"line": 18, "character": 13}, "end": {"line": 18, "character": 20}}, + {"start": {"line": 18, "character": 13}, "end": {"line": 18, "character": 15}}, "contents": {"value": "```lean\nf₂ : Foo → Nat\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hoverDot.lean"}, "position": {"line": 18, "character": 16}} {"range": - {"start": {"line": 18, "character": 13}, "end": {"line": 18, "character": 20}}, - "contents": {"value": "```lean\nf₂ : Foo → Nat\n```", "kind": "markdown"}} + {"start": {"line": 18, "character": 16}, "end": {"line": 18, "character": 20}}, + "contents": + {"value": "```lean\nNat.succ : Nat → Nat\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hoverDot.lean"}, "position": {"line": 21, "character": 14}} {"range": - {"start": {"line": 21, "character": 14}, "end": {"line": 21, "character": 21}}, + {"start": {"line": 21, "character": 14}, "end": {"line": 21, "character": 16}}, "contents": {"value": "```lean\nf₂ : Foo → Nat\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hoverDot.lean"}, "position": {"line": 21, "character": 17}} {"range": - {"start": {"line": 21, "character": 14}, "end": {"line": 21, "character": 21}}, - "contents": {"value": "```lean\nf₂ : Foo → Nat\n```", "kind": "markdown"}} + {"start": {"line": 21, "character": 17}, "end": {"line": 21, "character": 21}}, + "contents": + {"value": "```lean\nNat.succ : Nat → Nat\n```", "kind": "markdown"}}