Skip to content

Commit 66f0bd7

Browse files
mhuisimhuisi
committed
test: make 1265.lean more stable
1 parent 87db0bf commit 66f0bd7

File tree

2 files changed

+2
-184
lines changed

2 files changed

+2
-184
lines changed

‎tests/lean/interactive/1265.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
11
example (id : Lean.Syntax.Ident) : Lean.Name := id.
2-
--^ completion
2+
--^ textDocument/completion
33
example (id : Lean.TSyntax `ident) : Lean.Name := id.
4-
--^ completion
4+
--^ textDocument/completion

‎tests/lean/interactive/1265.lean.expected.out‎

Lines changed: 0 additions & 182 deletions
Original file line numberDiff line numberDiff line change
@@ -41,97 +41,6 @@
4141
"kind": 3,
4242
"data": ["«external:file:///1265.lean»", 0, 51, 1, "cLean.TSyntax.getId"]}],
4343
"isIncomplete": false}
44-
Resolution of getScientific:
45-
{"label": "getScientific",
46-
"kind": 3,
47-
"documentation":
48-
{"value":
49-
"Extracts the components of a scientific numeric literal.\n\nReturns a triple `(n, sign, e) : Nat × Bool × Nat`; the number's value is given by:\n\n```\nif sign then n * 10 ^ (-e) else n * 10 ^ e\n```\n\nReturns `(0, false, 0)` if the syntax is malformed.\n",
50-
"kind": "markdown"},
51-
"detail": "Lean.ScientificLit → Nat × Bool × Nat",
52-
"data":
53-
["«external:file:///1265.lean»", 0, 51, 1, "cLean.TSyntax.getScientific"]}
54-
Resolution of getString:
55-
{"label": "getString",
56-
"kind": 3,
57-
"documentation":
58-
{"value":
59-
"Decodes a string literal, removing quotation marks and unescaping escaped characters.\n\nReturns `\"\"` if the syntax is malformed.\n",
60-
"kind": "markdown"},
61-
"detail": "Lean.StrLit → String",
62-
"data": ["«external:file:///1265.lean»", 0, 51, 1, "cLean.TSyntax.getString"]}
63-
Resolution of getNat:
64-
{"label": "getNat",
65-
"kind": 3,
66-
"documentation":
67-
{"value":
68-
"Interprets a numeric literal as a natural number.\n\nReturns `0` if the syntax is malformed.\n",
69-
"kind": "markdown"},
70-
"detail": "Lean.NumLit → Nat",
71-
"data": ["«external:file:///1265.lean»", 0, 51, 1, "cLean.TSyntax.getNat"]}
72-
Resolution of getName:
73-
{"label": "getName",
74-
"kind": 3,
75-
"documentation":
76-
{"value":
77-
"Decodes a quoted name literal, returning the name.\n\nReturns `Lean.Name.anonymous` if the syntax is malformed.\n",
78-
"kind": "markdown"},
79-
"detail": "Lean.NameLit → Lean.Name",
80-
"data": ["«external:file:///1265.lean»", 0, 51, 1, "cLean.TSyntax.getName"]}
81-
Resolution of getChar:
82-
{"label": "getChar",
83-
"kind": 3,
84-
"documentation":
85-
{"value":
86-
"Decodes a character literal.\n\nReturns `(default : Char)` if the syntax is malformed.\n",
87-
"kind": "markdown"},
88-
"detail": "Lean.CharLit → Char",
89-
"data": ["«external:file:///1265.lean»", 0, 51, 1, "cLean.TSyntax.getChar"]}
90-
Resolution of raw:
91-
{"label": "raw",
92-
"kind": 5,
93-
"documentation":
94-
{"value": "The underlying `Syntax` value. ", "kind": "markdown"},
95-
"detail": "Lean.TSyntax ks → Lean.Syntax",
96-
"data": ["«external:file:///1265.lean»", 0, 51, 1, "cLean.TSyntax.raw"]}
97-
Resolution of getDocString:
98-
{"label": "getDocString",
99-
"kind": 3,
100-
"detail": "Lean.TSyntax `Lean.Parser.Command.docComment → String",
101-
"data":
102-
["«external:file:///1265.lean»", 0, 51, 1, "cLean.TSyntax.getDocString"]}
103-
Resolution of expandInterpolatedStr:
104-
{"label": "expandInterpolatedStr",
105-
"kind": 3,
106-
"documentation":
107-
{"value":
108-
"Expand `interpStr` into a term of type `type` (which supports ` ++ `),\ncalling `ofInterpFn` on terms within `{}`,\nand `ofLitFn` on the literals between the interpolations. ",
109-
"kind": "markdown"},
110-
"detail":
111-
"Lean.TSyntax Lean.interpolatedStrKind →\n Lean.Term → (ofInterpFn : Lean.Term) → optParam Lean.Term ofInterpFn → Lean.MacroM Lean.Term",
112-
"data":
113-
["«external:file:///1265.lean»",
114-
0,
115-
51,
116-
1,
117-
"cLean.TSyntax.expandInterpolatedStr"]}
118-
Resolution of getHygieneInfo:
119-
{"label": "getHygieneInfo",
120-
"kind": 3,
121-
"documentation":
122-
{"value": "Decodes macro hygiene information.\n", "kind": "markdown"},
123-
"detail": "Lean.HygieneInfo → Lean.Name",
124-
"data":
125-
["«external:file:///1265.lean»", 0, 51, 1, "cLean.TSyntax.getHygieneInfo"]}
126-
Resolution of getId:
127-
{"label": "getId",
128-
"kind": 3,
129-
"documentation":
130-
{"value":
131-
"Extracts the parsed name from the syntax of an identifier.\n\nReturns `Name.anonymous` if the syntax is malformed.\n",
132-
"kind": "markdown"},
133-
"detail": "Lean.Ident → Lean.Name",
134-
"data": ["«external:file:///1265.lean»", 0, 51, 1, "cLean.TSyntax.getId"]}
13544
{"textDocument": {"uri": "file:///1265.lean"},
13645
"position": {"line": 2, "character": 53}}
13746
{"items":
@@ -175,94 +84,3 @@ Resolution of getId:
17584
"kind": 3,
17685
"data": ["«external:file:///1265.lean»", 2, 53, 1, "cLean.TSyntax.getId"]}],
17786
"isIncomplete": false}
178-
Resolution of getScientific:
179-
{"label": "getScientific",
180-
"kind": 3,
181-
"documentation":
182-
{"value":
183-
"Extracts the components of a scientific numeric literal.\n\nReturns a triple `(n, sign, e) : Nat × Bool × Nat`; the number's value is given by:\n\n```\nif sign then n * 10 ^ (-e) else n * 10 ^ e\n```\n\nReturns `(0, false, 0)` if the syntax is malformed.\n",
184-
"kind": "markdown"},
185-
"detail": "Lean.ScientificLit → Nat × Bool × Nat",
186-
"data":
187-
["«external:file:///1265.lean»", 2, 53, 1, "cLean.TSyntax.getScientific"]}
188-
Resolution of getString:
189-
{"label": "getString",
190-
"kind": 3,
191-
"documentation":
192-
{"value":
193-
"Decodes a string literal, removing quotation marks and unescaping escaped characters.\n\nReturns `\"\"` if the syntax is malformed.\n",
194-
"kind": "markdown"},
195-
"detail": "Lean.StrLit → String",
196-
"data": ["«external:file:///1265.lean»", 2, 53, 1, "cLean.TSyntax.getString"]}
197-
Resolution of getNat:
198-
{"label": "getNat",
199-
"kind": 3,
200-
"documentation":
201-
{"value":
202-
"Interprets a numeric literal as a natural number.\n\nReturns `0` if the syntax is malformed.\n",
203-
"kind": "markdown"},
204-
"detail": "Lean.NumLit → Nat",
205-
"data": ["«external:file:///1265.lean»", 2, 53, 1, "cLean.TSyntax.getNat"]}
206-
Resolution of getName:
207-
{"label": "getName",
208-
"kind": 3,
209-
"documentation":
210-
{"value":
211-
"Decodes a quoted name literal, returning the name.\n\nReturns `Lean.Name.anonymous` if the syntax is malformed.\n",
212-
"kind": "markdown"},
213-
"detail": "Lean.NameLit → Lean.Name",
214-
"data": ["«external:file:///1265.lean»", 2, 53, 1, "cLean.TSyntax.getName"]}
215-
Resolution of getChar:
216-
{"label": "getChar",
217-
"kind": 3,
218-
"documentation":
219-
{"value":
220-
"Decodes a character literal.\n\nReturns `(default : Char)` if the syntax is malformed.\n",
221-
"kind": "markdown"},
222-
"detail": "Lean.CharLit → Char",
223-
"data": ["«external:file:///1265.lean»", 2, 53, 1, "cLean.TSyntax.getChar"]}
224-
Resolution of raw:
225-
{"label": "raw",
226-
"kind": 5,
227-
"documentation":
228-
{"value": "The underlying `Syntax` value. ", "kind": "markdown"},
229-
"detail": "Lean.TSyntax ks → Lean.Syntax",
230-
"data": ["«external:file:///1265.lean»", 2, 53, 1, "cLean.TSyntax.raw"]}
231-
Resolution of getDocString:
232-
{"label": "getDocString",
233-
"kind": 3,
234-
"detail": "Lean.TSyntax `Lean.Parser.Command.docComment → String",
235-
"data":
236-
["«external:file:///1265.lean»", 2, 53, 1, "cLean.TSyntax.getDocString"]}
237-
Resolution of expandInterpolatedStr:
238-
{"label": "expandInterpolatedStr",
239-
"kind": 3,
240-
"documentation":
241-
{"value":
242-
"Expand `interpStr` into a term of type `type` (which supports ` ++ `),\ncalling `ofInterpFn` on terms within `{}`,\nand `ofLitFn` on the literals between the interpolations. ",
243-
"kind": "markdown"},
244-
"detail":
245-
"Lean.TSyntax Lean.interpolatedStrKind →\n Lean.Term → (ofInterpFn : Lean.Term) → optParam Lean.Term ofInterpFn → Lean.MacroM Lean.Term",
246-
"data":
247-
["«external:file:///1265.lean»",
248-
2,
249-
53,
250-
1,
251-
"cLean.TSyntax.expandInterpolatedStr"]}
252-
Resolution of getHygieneInfo:
253-
{"label": "getHygieneInfo",
254-
"kind": 3,
255-
"documentation":
256-
{"value": "Decodes macro hygiene information.\n", "kind": "markdown"},
257-
"detail": "Lean.HygieneInfo → Lean.Name",
258-
"data":
259-
["«external:file:///1265.lean»", 2, 53, 1, "cLean.TSyntax.getHygieneInfo"]}
260-
Resolution of getId:
261-
{"label": "getId",
262-
"kind": 3,
263-
"documentation":
264-
{"value":
265-
"Extracts the parsed name from the syntax of an identifier.\n\nReturns `Name.anonymous` if the syntax is malformed.\n",
266-
"kind": "markdown"},
267-
"detail": "Lean.Ident → Lean.Name",
268-
"data": ["«external:file:///1265.lean»", 2, 53, 1, "cLean.TSyntax.getId"]}

0 commit comments

Comments
 (0)