diff options
| author |  Simon Van Casteren <simonvancasteren@localhost.localdomain> | 2019-12-12 22:55:24 +0100 |
|---|---|---|
| committer | Simon Van Casteren <simonvancasteren@localhost.localdomain> | 2019-12-13 11:46:57 +0100 |
| commit | a16c342d75f96a530da30e85465328306f5412ef (patch) | |
| tree | b0313e6ab464edf0527017404ee7572ad1a7f568 | |
| parent | 679977b188fc9bbfd1b311e895ca48454876b7f4 (diff) | |
Last tweak to datatype constructors autocomplete
| -rw-r--r-- | src/lsp.sml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/lsp.sml b/src/lsp.sml index 7aa7a98b..50eea923 100644 --- a/src/lsp.sml +++ b/src/lsp.sml @@ -833,14 +833,15 @@ fun getCompletionsFromSignatureItems (env: ElabEnv.env) (prefix: string) (search 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 x k) env xs + val typeVarsString = List.foldl (fn (x, acc) => acc ^ " " ^ x) "" 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 => dtName - | SOME con => ppToString (ElabPrint.p_con env con) 150 ^ " -> " ^ dtName + NONE => dtName ^ typeVarsString + | SOME con => ppToString (ElabPrint.p_con env con) 150 ^ " -> " ^ dtName ^ typeVarsString } else NONE) constrs end) |