From f2ada9d9761c3aa7575571fd93629b79350a1425 Mon Sep 17 00:00:00 2001 From: Simon Van Casteren Date: Fri, 13 Dec 2019 10:58:11 +0100 Subject: Trial version of completing table fields --- src/elab_env.sml | 7 +++---- src/lsp.sml | 13 ++++++++++++- 2 files changed, 15 insertions(+), 5 deletions(-) diff --git a/src/elab_env.sml b/src/elab_env.sml index 34071664..f492bc94 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -940,13 +940,12 @@ fun lookupENamed (env : env) n = NONE => raise UnboundNamed n | SOME x => x +(* TODO Why does this work better than using #renameE? *) fun matchEByPrefix (env: env) (prefix: string): (string * con) list = List.mapPartial (fn (name, value) => if String.isPrefix prefix name - then case value of - Rel' (_, x) => SOME (name, x) - | Named' (_, x) => SOME (name, x) + then SOME (name, value) else NONE) - (SM.listItemsi (#renameE env)) + (#relE env @ IM.listItems (#namedE env)) fun checkENamed (env : env) n = Option.isSome (IM.find (#namedE env, n)) diff --git a/src/lsp.sml b/src/lsp.sml index 2d80479b..920f9f35 100644 --- a/src/lsp.sml +++ b/src/lsp.sml @@ -931,8 +931,19 @@ fun findMatchingStringInEnv (env: ElabEnv.env) (str: string): LspSpec.completion in (case List.map (fn (name, c) => (name, ElabOps.reduceCon env c)) filteredEs of [] => [] - | (name, (Elab.TRecord (Elab.CRecord (_, fields), _), _)) :: _ => + | (name, (Elab.TRecord (Elab.CRecord (_, fields), l2_), l1_)) :: _ => getCompletionsFromFields env (name ^ ".") (Substring.string str) fields + | (name, (* TODO this doesn't always work. I've only managed to get it working for tables in a different module *) + ( ( Elab.CApp + ( ( (Elab.CApp + ( ( Elab.CModProj (_, _, "sql_table") + , l4_) + , ( Elab.CRecord (_, fields) + , l3_))) + , l2_) + , _)) + , l1_)) :: _ => + (debug "!!"; getCompletionsFromFields env (name ^ ".") (Substring.string str) fields) | _ => []) end | _ => -- cgit v1.2.3