diff --git a/src/Lean/Server/Completion/CompletionUtils.lean b/src/Lean/Server/Completion/CompletionUtils.lean index 1ee43b47cb..0001c47bf4 100644 --- a/src/Lean/Server/Completion/CompletionUtils.lean +++ b/src/Lean/Server/Completion/CompletionUtils.lean @@ -22,7 +22,7 @@ where let ac := aPos.get' a ha let bc := bPos.get' b hb let bPos := bPos.next' b hb - if ac == bc then + if ac.toLower == bc.toLower then let aPos := aPos.next' a ha go aPos bPos else diff --git a/tests/lean/interactive/completionOption.lean.expected.out b/tests/lean/interactive/completionOption.lean.expected.out index 1b7463f9ed..3e9c34d1d7 100644 --- a/tests/lean/interactive/completionOption.lean.expected.out +++ b/tests/lean/interactive/completionOption.lean.expected.out @@ -273,6 +273,19 @@ Resolution of format.indent: "detail": "(false), enable/disable tracing for the given module and submodules", "data": ["«external:file:///completionOption.lean»", 7, 23, 0]}, + {"textEdit": + {"replace": + {"start": {"line": 7, "character": 11}, + "end": {"line": 7, "character": 23}}, + "newText": "trace.PrettyPrinter.parenthesize.backtrack", + "insert": + {"start": {"line": 7, "character": 11}, + "end": {"line": 7, "character": 23}}}, + "label": "trace.PrettyPrinter.parenthesize.backtrack", + "kind": 10, + "detail": + "(false), enable/disable tracing for the given module and submodules", + "data": ["«external:file:///completionOption.lean»", 7, 23, 0]}, {"textEdit": {"replace": {"start": {"line": 7, "character": 11}, @@ -337,6 +350,18 @@ Resolution of trace.pp.analyze.error: "detail": "(false), enable/disable tracing for the given module and submodules", "data": ["«external:file:///completionOption.lean»", 7, 23, 0]} +Resolution of trace.PrettyPrinter.parenthesize.backtrack: +{"textEdit": + {"replace": + {"start": {"line": 7, "character": 11}, "end": {"line": 7, "character": 23}}, + "newText": "trace.PrettyPrinter.parenthesize.backtrack", + "insert": + {"start": {"line": 7, "character": 11}, "end": {"line": 7, "character": 23}}}, + "label": "trace.PrettyPrinter.parenthesize.backtrack", + "kind": 10, + "detail": + "(false), enable/disable tracing for the given module and submodules", + "data": ["«external:file:///completionOption.lean»", 7, 23, 0]} Resolution of trace.pp.analyze: {"textEdit": {"replace":