76051ab1fe
This PR modifies dot identifier notation so that `(.a : T)` resolves `T.a` with respect to the root namespace, like for generalized field notation. This lets the notation refer to private names, follow aliases, and also use open namespaces. The LSP completions are improved to follow how dot ident notation is resolved, but it doesn't yet take into account aliases or open namespaces. Closes #9629
129 lines
4.2 KiB
Text
129 lines
4.2 KiB
Text
{"textDocument": {"uri": "file:///dottedIdentNotation.lean"},
|
|
"position": {"line": 11, "character": 22}}
|
|
{"items":
|
|
[{"label": "zero",
|
|
"kind": 4,
|
|
"data":
|
|
{"params":
|
|
{"textDocument": {"uri": "file:///dottedIdentNotation.lean"},
|
|
"position": {"line": 11, "character": 22}},
|
|
"id": {"const": {"declName": "MyNat.zero"}},
|
|
"cPos": 0}}],
|
|
"isIncomplete": false}
|
|
{"textDocument": {"uri": "file:///dottedIdentNotation.lean"},
|
|
"position": {"line": 14, "character": 30}}
|
|
{"items":
|
|
[{"label": "succ",
|
|
"kind": 4,
|
|
"data":
|
|
{"params":
|
|
{"textDocument": {"uri": "file:///dottedIdentNotation.lean"},
|
|
"position": {"line": 14, "character": 30}},
|
|
"id": {"const": {"declName": "MyNat.succ"}},
|
|
"cPos": 0}}],
|
|
"isIncomplete": false}
|
|
{"textDocument": {"uri": "file:///dottedIdentNotation.lean"},
|
|
"position": {"line": 23, "character": 23}}
|
|
{"items":
|
|
[{"label": "zero",
|
|
"kind": 4,
|
|
"data":
|
|
{"params":
|
|
{"textDocument": {"uri": "file:///dottedIdentNotation.lean"},
|
|
"position": {"line": 23, "character": 23}},
|
|
"id": {"const": {"declName": "MyNat.zero"}},
|
|
"cPos": 0}}],
|
|
"isIncomplete": false}
|
|
{"textDocument": {"uri": "file:///dottedIdentNotation.lean"},
|
|
"position": {"line": 26, "character": 32}}
|
|
{"items":
|
|
[{"label": "succ",
|
|
"kind": 4,
|
|
"data":
|
|
{"params":
|
|
{"textDocument": {"uri": "file:///dottedIdentNotation.lean"},
|
|
"position": {"line": 26, "character": 32}},
|
|
"id": {"const": {"declName": "MyNat.succ"}},
|
|
"cPos": 0}}],
|
|
"isIncomplete": false}
|
|
{"textDocument": {"uri": "file:///dottedIdentNotation.lean"},
|
|
"position": {"line": 33, "character": 31}}
|
|
{"items":
|
|
[{"label": "zero",
|
|
"kind": 4,
|
|
"data":
|
|
{"params":
|
|
{"textDocument": {"uri": "file:///dottedIdentNotation.lean"},
|
|
"position": {"line": 33, "character": 31}},
|
|
"id": {"const": {"declName": "MyNat.zero"}},
|
|
"cPos": 0}}],
|
|
"isIncomplete": false}
|
|
{"textDocument": {"uri": "file:///dottedIdentNotation.lean"},
|
|
"position": {"line": 38, "character": 31}}
|
|
{"items": [], "isIncomplete": false}
|
|
{"textDocument": {"uri": "file:///dottedIdentNotation.lean"},
|
|
"position": {"line": 51, "character": 24}}
|
|
{"items":
|
|
[{"label": "zero",
|
|
"kind": 4,
|
|
"data":
|
|
{"params":
|
|
{"textDocument": {"uri": "file:///dottedIdentNotation.lean"},
|
|
"position": {"line": 51, "character": 24}},
|
|
"id": {"const": {"declName": "MyNat.zero"}},
|
|
"cPos": 0}}],
|
|
"isIncomplete": false}
|
|
{"textDocument": {"uri": "file:///dottedIdentNotation.lean"},
|
|
"position": {"line": 64, "character": 32}}
|
|
{"items":
|
|
[{"label": "succ",
|
|
"kind": 4,
|
|
"data":
|
|
{"params":
|
|
{"textDocument": {"uri": "file:///dottedIdentNotation.lean"},
|
|
"position": {"line": 64, "character": 32}},
|
|
"id": {"const": {"declName": "MyNat.succ"}},
|
|
"cPos": 0}}],
|
|
"isIncomplete": false}
|
|
{"title": "Import IO.FS.Stream.chainLeft from Lean.Server.Utils",
|
|
"kind": "quickfix",
|
|
"edit":
|
|
{"documentChanges":
|
|
[{"textDocument": {"version": 1, "uri": "file:///dottedIdentNotation.lean"},
|
|
"edits":
|
|
[{"range":
|
|
{"start": {"line": 0, "character": 0},
|
|
"end": {"line": 0, "character": 0}},
|
|
"newText": "import Lean.Server.Utils\n"},
|
|
{"range":
|
|
{"start": {"line": 73, "character": 27},
|
|
"end": {"line": 73, "character": 35}},
|
|
"newText": "chainLeft"}]}]}}
|
|
{"title": "Import IO.FS.Stream.chainLeft from Lean.Server.Utils",
|
|
"kind": "quickfix",
|
|
"edit":
|
|
{"documentChanges":
|
|
[{"textDocument": {"version": 1, "uri": "file:///dottedIdentNotation.lean"},
|
|
"edits":
|
|
[{"range":
|
|
{"start": {"line": 0, "character": 0},
|
|
"end": {"line": 0, "character": 0}},
|
|
"newText": "import Lean.Server.Utils\n"},
|
|
{"range":
|
|
{"start": {"line": 76, "character": 36},
|
|
"end": {"line": 76, "character": 44}},
|
|
"newText": "chainLeft"}]}]}}
|
|
{"title": "Import IO.FS.Stream.chainLeft from Lean.Server.Utils",
|
|
"kind": "quickfix",
|
|
"edit":
|
|
{"documentChanges":
|
|
[{"textDocument": {"version": 1, "uri": "file:///dottedIdentNotation.lean"},
|
|
"edits":
|
|
[{"range":
|
|
{"start": {"line": 0, "character": 0},
|
|
"end": {"line": 0, "character": 0}},
|
|
"newText": "import Lean.Server.Utils\n"},
|
|
{"range":
|
|
{"start": {"line": 79, "character": 33},
|
|
"end": {"line": 79, "character": 41}},
|
|
"newText": "chainLeft"}]}]}}
|