From 8ef0d043574638a48c71b7c4c9844fc05973f13d Mon Sep 17 00:00:00 2001 From: Simon Van Casteren Date: Fri, 13 Dec 2019 09:58:15 +0100 Subject: Added completion suggestions for types --- src/elab_env.sml | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) (limited to 'src/elab_env.sml') diff --git a/src/elab_env.sml b/src/elab_env.sml index e79b665d..34071664 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -404,6 +404,14 @@ fun lookupC (env : env) x = | SOME (Rel' x) => Rel x | SOME (Named' x) => Named x +fun matchCByPrefix (env: env) (prefix: string): (string * kind) 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) + else NONE) + (SM.listItemsi (#renameC env)) + fun pushDatatype (env : env) n xs xncs = let val dk = U.classifyDatatype xncs @@ -932,11 +940,13 @@ fun lookupENamed (env : env) n = NONE => raise UnboundNamed n | SOME x => x -fun matchNamedEByPrefix (env: env) (str: string) = - List.filter (fn (name,con) => String.isPrefix str name) (IM.listItems (#namedE env)) - -fun matchRelEByPrefix (env: env) (str: string) = - List.filter (fn (name,con) => String.isPrefix str name) (#relE env) +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) + else NONE) + (SM.listItemsi (#renameE env)) fun checkENamed (env : env) n = Option.isSome (IM.find (#namedE env, n)) -- cgit v1.2.3