From 679977b188fc9bbfd1b311e895ca48454876b7f4 Mon Sep 17 00:00:00 2001 From: Simon Van Casteren Date: Thu, 12 Dec 2019 22:50:35 +0100 Subject: Tweaks to autocompletion of datatype constructors --- src/lsp.sml | 6 +++--- 1 file 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) -- cgit v1.2.3