summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Simon Van Casteren <simonvancasteren@localhost.localdomain>2019-12-12 22:50:35 +0100
committerGravatar Simon Van Casteren <simonvancasteren@localhost.localdomain>2019-12-13 11:46:57 +0100
commit679977b188fc9bbfd1b311e895ca48454876b7f4 (patch)
tree6ee224027ce86997ffa673221c8ed5d7f7a22e52
parentfaff2d8ac927fd49f13fbaf9b84ffc99bbb6f9b8 (diff)
Tweaks to autocompletion of datatype constructors
-rw-r--r--src/lsp.sml6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/lsp.sml b/src/lsp.sml
index aaef422c..7aa7a98b 100644
--- a/src/lsp.sml
+++ b/src/lsp.sml
@@ -832,15 +832,15 @@ fun getCompletionsFromSignatureItems (env: ElabEnv.env) (prefix: string) (search
let
val k = (Elab.KType, ErrorMsg.dummySpan)
val env = ElabEnv.pushCNamedAs env dtName n k NONE
- val env = List.foldl (fn (x, env) => ElabEnv.pushCRel env dtName k) env xs
+ val env = List.foldl (fn (x, env) => ElabEnv.pushCRel env x k) env xs
in
List.mapPartial (fn (constrName, _, conO) =>
if String.isPrefix searchStr constrName
then SOME { label = prefix ^ constrName
, kind = LspSpec.Function
, detail = case conO of
- NONE => "Datatype " ^ dtName
- | SOME con => "Datatype " ^ dtName ^ " - " ^ ppToString (ElabPrint.p_con env con) 150
+ NONE => dtName
+ | SOME con => ppToString (ElabPrint.p_con env con) 150 ^ " -> " ^ dtName
}
else NONE) constrs
end)