summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Simon Van Casteren <simonvancasteren@localhost.localdomain>2019-12-13 10:58:11 +0100
committerGravatar Simon Van Casteren <simonvancasteren@localhost.localdomain>2019-12-13 11:46:57 +0100
commitf2ada9d9761c3aa7575571fd93629b79350a1425 (patch)
tree4dd385ff8a2fd742a48ecb1db7d385574f6a679c /src
parent8ef0d043574638a48c71b7c4c9844fc05973f13d (diff)
Trial version of completing table fields
Diffstat (limited to 'src')
-rw-r--r--src/elab_env.sml7
-rw-r--r--src/lsp.sml13
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
| _ =>