summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Simon Van Casteren <simonvancasteren@localhost.localdomain>2019-12-12 22:44:50 +0100
committerGravatar Simon Van Casteren <simonvancasteren@localhost.localdomain>2019-12-13 11:46:57 +0100
commitfaff2d8ac927fd49f13fbaf9b84ffc99bbb6f9b8 (patch)
tree557c53bb80d4cbf286149504580886cd4259b3f2
parent9b00dc724363ac7b0a31687f14cc3bb2f2460f9b (diff)
Added tracking of text of source files and autocomplete
-rw-r--r--derivation.nix4
-rw-r--r--shell.nix8
-rw-r--r--src/elab_env.sig4
-rw-r--r--src/elab_env.sml9
-rw-r--r--src/elab_print.sig1
-rw-r--r--src/getinfo.sig20
-rw-r--r--src/getinfo.sml51
-rw-r--r--src/json.sml11
-rw-r--r--src/lsp.sml399
9 files changed, 438 insertions, 69 deletions
diff --git a/derivation.nix b/derivation.nix
index f956a619..19582948 100644
--- a/derivation.nix
+++ b/derivation.nix
@@ -1,6 +1,6 @@
{ stdenv, lib, fetchFromGitHub, file, openssl, mlton
, mysql, postgresql, sqlite, gcc
-, automake, autoconf, libtool, icu
+, automake, autoconf, libtool, icu, nix-gitignore
}:
stdenv.mkDerivation rec {
@@ -18,7 +18,7 @@ stdenv.mkDerivation rec {
# rev = "e52ce9f542f64750941cfd84efdb6d993ee20ff0";
# sha256 = "19ba5n7g1dxy7q9949aakqplchsyzwrrnxv8v604vx5sg7fdfn3b";
# };
- src = ./.;
+ src = nix-gitignore.gitignoreSource [] ./.;
buildInputs = [ openssl mlton mysql.connector-c postgresql sqlite automake autoconf libtool icu.dev openssl.dev];
diff --git a/shell.nix b/shell.nix
index 95da550b..e9b047ee 100644
--- a/shell.nix
+++ b/shell.nix
@@ -1 +1,7 @@
-import ./default.nix
+let
+ pkgs = import <nixpkgs> {};
+ def = import ./default.nix;
+in
+pkgs.mkShell {
+ buildInputs = def.buildInputs;
+}
diff --git a/src/elab_env.sig b/src/elab_env.sig
index 47b31c08..55909b53 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -85,6 +85,8 @@ signature ELAB_ENV = sig
val pushENamedAs : env -> string -> int -> Elab.con -> env
val lookupENamed : env -> int -> string * Elab.con
val checkENamed : env -> int -> bool
+ val matchNamedEByPrefix: env -> string -> (string * Elab.con) list
+ val matchRelEByPrefix: env -> string -> (string * Elab.con) list
val lookupE : env -> string -> Elab.con var
@@ -100,6 +102,8 @@ signature ELAB_ENV = sig
val lookupStrNamed : env -> int -> string * Elab.sgn
val lookupStr : env -> string -> (int * Elab.sgn) option
+ val matchStrByPrefix: env -> string -> (string * (int * Elab.sgn)) list
+
val edeclBinds : env -> Elab.edecl -> env
val declBinds : env -> Elab.decl -> env
diff --git a/src/elab_env.sml b/src/elab_env.sml
index a2097aa9..e79b665d 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -932,6 +932,12 @@ 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 checkENamed (env : env) n =
Option.isSome (IM.find (#namedE env, n))
@@ -985,7 +991,8 @@ fun lookupStrNamed (env : env) n =
| SOME x => x
fun lookupStr (env : env) x = SM.find (#renameStr env, x)
-
+fun matchStrByPrefix (env: env) prefix =
+ List.filter (fn (name,_) => String.isPrefix prefix name) (SM.listItemsi (#renameStr env))
fun sgiSeek (sgi, (sgns, strs, cons)) =
case sgi of
diff --git a/src/elab_print.sig b/src/elab_print.sig
index 1eb832b3..84715b9d 100644
--- a/src/elab_print.sig
+++ b/src/elab_print.sig
@@ -38,6 +38,7 @@ signature ELAB_PRINT = sig
val p_sgn : ElabEnv.env -> Elab.sgn Print.printer
val p_str : ElabEnv.env -> Elab.str Print.printer
val p_file : ElabEnv.env -> Elab.file Print.printer
+
val debug : bool ref
end
diff --git a/src/getinfo.sig b/src/getinfo.sig
index 334e19f1..50eee70a 100644
--- a/src/getinfo.sig
+++ b/src/getinfo.sig
@@ -26,11 +26,29 @@
*)
signature GET_INFO = sig
+
+ datatype item =
+ Kind of Elab.kind
+ | Con of Elab.con
+ | Exp of Elab.exp
+ | Sgn_item of Elab.sgn_item
+ | Sgn of Elab.sgn
+ | Str of Elab.str
+ | Decl of Elab.decl
+
val getInfo:
ElabEnv.env ->
Elab.str' ->
string (* fileName *) ->
{ line: int , character: int} ->
- Print.PD.pp_desc
+ { smallest : { span : ErrorMsg.span
+ , item : item
+ , env : ElabEnv.env }
+ , smallestgoodpart : { span : ErrorMsg.span
+ , desc : Print.PD.pp_desc
+ , env : ElabEnv.env
+ , item : item
+ } option
+}
end
diff --git a/src/getinfo.sml b/src/getinfo.sml
index 7925aba3..1d657637 100644
--- a/src/getinfo.sml
+++ b/src/getinfo.sml
@@ -73,6 +73,19 @@ fun getSpan (f: item * E.env) =
| Str s => #2 s
| Decl d => #2 d
+(* Just use ElabPrint functions. *)
+(* These are better for compiler error messages, but it's better than nothing *)
+fun printLiterally {span = span, item = item, env = env} =
+ P.box [ case item of
+ Kind k => P.box [P.PD.string "KIND: ", ElabPrint.p_kind env k]
+ | Con c => P.box [P.PD.string "CON: ", ElabPrint.p_con env c]
+ | Exp e => P.box [P.PD.string "EXP: ", ElabPrint.p_exp env e]
+ | Sgn_item si => P.box [P.PD.string "SGN_ITEM: ", ElabPrint.p_sgn_item env si]
+ | Sgn s => P.box [P.PD.string "SGN: ", ElabPrint.p_sgn env s]
+ | Str s => P.box [P.PD.string "STR: ", ElabPrint.p_str env s]
+ | Decl d => P.box [P.PD.string "DECL: ", ElabPrint.p_decl env d]
+ ]
+
fun getInfo env str fileName {line = row, character = col} =
let
val () = U.mliftConInCon := E.mliftConInCon
@@ -89,19 +102,6 @@ fun getInfo env str fileName {line = row, character = col} =
else env) env decls
| _ => env)
- (* Just use ElabPrint functions. *)
- (* These are better for compiler error messages, but it's better than nothing *)
- fun printLiterally {span = span, item = item, env = env} =
- P.box [ case item of
- Kind k => P.box [P.PD.string "KIND: ", ElabPrint.p_kind env k]
- | Con c => P.box [P.PD.string "CON: ", ElabPrint.p_con env c]
- | Exp e => P.box [P.PD.string "EXP: ", ElabPrint.p_exp env e]
- | Sgn_item si => P.box [P.PD.string "SGN_ITEM: ", ElabPrint.p_sgn_item env si]
- | Sgn s => P.box [P.PD.string "SGN: ", ElabPrint.p_sgn env s]
- | Str s => P.box [P.PD.string "STR: ", ElabPrint.p_str env s]
- | Decl d => P.box [P.PD.string "DECL: ", ElabPrint.p_decl env d]
- ]
-
(* TODO We lose some really useful information, like eg. inferred parameters, *)
(* which we do have in the actual items (L.Decl, L.Exp, etc) *)
(* but not when we do a lookup into the Env *)
@@ -161,7 +161,16 @@ fun getInfo env str fileName {line = row, character = col} =
| Str s => NONE
| Decl d => NONE)
- fun add env item span acc =
+ fun add (env: ElabEnv.env) (item: item) (span: ErrorMsg.span) (acc: { smallest : { span : ErrorMsg.span
+ , item : item
+ , env : ElabEnv.env }
+ , smallestgoodpart : { span : ErrorMsg.span
+ , desc : P.PD.pp_desc
+ , env : ElabEnv.env
+ , item : item
+ } option
+ }
+ ) =
if not (isPosIn fileName row col span)
then
acc
@@ -176,14 +185,14 @@ fun getInfo env str fileName {line = row, character = col} =
NONE =>
(case printGoodPart env item span of
NONE => NONE
- | SOME desc => SOME (desc, span))
- | SOME (desc', span') =>
+ | SOME desc => SOME {desc = desc, span = span, env = env, item = item})
+ | SOME (prev as {desc = desc', span = span', env = env', item = item'}) =>
if isSmallerThan span span'
then
(case printGoodPart env item span of
- NONE => SOME (desc', span')
- | SOME desc => SOME (desc, span))
- else SOME (desc', span')
+ NONE => SOME prev
+ | SOME desc => SOME {desc = desc, span = span, env = env, item = item})
+ else SOME prev
in
{smallest = smallest, smallestgoodpart = smallestgoodpart}
end
@@ -228,8 +237,6 @@ fun getInfo env str fileName {line = row, character = col} =
( L.DStr (Compiler.moduleOf "fileName", 0, (L.SgnError, ErrorMsg.dummySpan), (str, {file = fileName, first = ErrorMsg.dummyPos, last = ErrorMsg.dummyPos}))
, {file = fileName, first = ErrorMsg.dummyPos, last = ErrorMsg.dummyPos})
in
- case #smallestgoodpart result of
- NONE => printLiterally (#smallest result)
- | SOME (desc, span) => desc
+ result
end
end
diff --git a/src/json.sml b/src/json.sml
index 656d28ff..4f604cc4 100644
--- a/src/json.sml
+++ b/src/json.sml
@@ -113,13 +113,20 @@ struct
and parseChars () =
let
+ val escapedchars = ["n", "r", "b", "f", "t"]
fun pickChars s =
- if peek () = #"\"" (* " *)
+ if peek () = #"\"" (* " = end of string *)
then s
else
if peek () = #"\\" andalso (String.sub (!inputData, 1)) = #"\""
then (consume "\\\""; pickChars (s ^ "\""))
- else pickChars (s ^ String.str (take ()))
+ else
+ if peek () = #"\\" andalso (String.sub (!inputData, 1)) = #"n"
+ then (consume "\\n"; pickChars (s ^ "\n"))
+ else
+ if peek () = #"\\" andalso (String.sub (!inputData, 1)) = #"r"
+ then (consume "\\r"; pickChars (s ^ "\r"))
+ else pickChars (s ^ String.str (take ()))
in
pickChars ""
end
diff --git a/src/lsp.sml b/src/lsp.sml
index cfdec863..aaef422c 100644
--- a/src/lsp.sml
+++ b/src/lsp.sml
@@ -11,13 +11,17 @@ fun joinStr (sep: string) (strs: string list): string =
List.foldl (fn (str, acc) => if acc = "" then str else acc ^ sep ^ str) "" strs
structure FromJson = struct
+fun getO (s: string) (l: Json.json): Json.json option =
+ case l of
+ Json.Obj pairs =>
+ (case List.find (fn tup => #1 tup = s) pairs of
+ NONE => NONE
+ | SOME tup => SOME (#2 tup))
+ | _ => raise Fail ("Expected JSON object, got: " ^ Json.print l)
fun get (s: string) (l: Json.json): Json.json =
- case l of
- Json.Obj pairs =>
- (case List.find (fn tup => #1 tup = s) pairs of
- NONE => raise Fail ("Failed to find JSON object key " ^ s ^ " in " ^ Json.print l)
- | SOME tup => #2 tup)
- | _ => raise Fail ("Expected JSON object, got: " ^ Json.print l)
+ (case getO s l of
+ NONE => raise Fail ("Failed to find JSON object key " ^ s ^ " in " ^ Json.print l)
+ | SOME a => a)
fun asInt (j: Json.json): int =
case j of
@@ -161,6 +165,10 @@ structure LspSpec (* :> LSPSPEC *) = struct
type range = { start: position
, end_: position }
+ fun parseRange (j: Json.json): range =
+ { start = parsePosition (FromJson.get "start" j)
+ , end_ = parsePosition (FromJson.get "end" j)
+ }
fun printRange (r: range): Json.json = Json.Obj [ ("start", printPosition (#start r))
, ("end", printPosition (#end_ r))]
@@ -194,10 +202,23 @@ structure LspSpec (* :> LSPSPEC *) = struct
fun parseDidOpenParams (params: Json.json): didOpenParams =
{ textDocument = parseTextDocumentItem (FromJson.get "textDocument" params) }
- type didChangeParams = { textDocument: versionedTextDocumentIdentifier }
+ type contentChange = { range: range option
+ , rangeLength: int option
+ , text: string }
+ type didChangeParams =
+ { textDocument: versionedTextDocumentIdentifier
+ , contentChanges: contentChange list
+ }
fun parseDidChangeParams (params: Json.json): didChangeParams =
{ textDocument = parseVersionedTextDocumentIdentifier (FromJson.get "textDocument" params)
- (* , contentChanges = ... *)
+ , contentChanges = case FromJson.get "contentChanges" params of
+ Json.Array js =>
+ List.map (fn j => { range = Option.map parseRange (FromJson.getO "range" j)
+ , rangeLength = Option.map FromJson.asInt (FromJson.getO "rangeLength" j)
+ , text = FromJson.asString (FromJson.get "text" j)
+ }
+ ) js
+ | j => raise Fail ("Expected JSON array, got: " ^ Json.print j)
}
type didSaveParams = { textDocument: textDocumentIdentifier }
@@ -232,11 +253,77 @@ structure LspSpec (* :> LSPSPEC *) = struct
fun printPublishDiagnosticsParams (p: publishDiagnosticsParams): Json.json =
Json.Obj [ ("uri", Json.String (printDocumentUri (#uri p)))
, ("diagnostics", Json.Array (List.map printDiagnostic (#diagnostics p)))]
-
+
+ type completionReq =
+ { textDocument: textDocumentIdentifier
+ , position: position
+ , context: { triggerCharacter: string option
+ , triggerKind: int (* 1 = Invoked = typing an identifier or manual invocation or API
+ 2 = TriggerCharacter
+ 3 = TriggerForIncompleteCompletions*)} option
+ }
+ fun parseCompletionReq (j: Json.json): completionReq =
+ { textDocument = parseTextDocumentIdentifier (FromJson.get "textDocument" j)
+ , position = parsePosition (FromJson.get "position" j)
+ , context = case FromJson.getO "context" j of
+ NONE => NONE
+ | SOME ctx => SOME { triggerCharacter = Option.map FromJson.asString (FromJson.getO "triggerCharacter" ctx)
+ , triggerKind = FromJson.asInt (FromJson.get "triggerKind" ctx)
+ }
+ }
+
+ datatype completionItemKind = Text | Method | Function | Constructor | Field | Variable | Class | Interface | Module | Property | Unit | Value | Enum | Keyword | Snippet | Color | File | Reference | Folder | EnumMember | Constant | Struct | Event | Operator | TypeParameter
+ fun completionItemKindToInt (a: completionItemKind) =
+ case a of
+ Text => 1
+ | Method => 2
+ | Function => 3
+ | Constructor => 4
+ | Field => 5
+ | Variable => 6
+ | Class => 7
+ | Interface => 8
+ | Module => 9
+ | Property => 10
+ | Unit => 11
+ | Value => 12
+ | Enum => 13
+ | Keyword => 14
+ | Snippet => 15
+ | Color => 16
+ | File => 17
+ | Reference => 18
+ | Folder => 19
+ | EnumMember => 20
+ | Constant => 21
+ | Struct => 22
+ | Event => 23
+ | Operator => 24
+ | TypeParameter => 25
+
+ type completionItem = { label: string
+ , kind: completionItemKind
+ , detail: string
+ }
+ type completionResp = { isIncomplete: bool
+ , items: completionItem list
+ }
+
+ fun printCompletionItem (a: completionItem): Json.json =
+ Json.Obj [ ("label", Json.String (#label a))
+ , ("kind", Json.Int (completionItemKindToInt (#kind a)))
+ , ("detail", Json.String (#detail a))
+ ]
+ fun printCompletionResp (a: completionResp): Json.json =
+ Json.Obj [ ("isIncomplete", Json.Bool (#isIncomplete a))
+ , (("items", Json.Array (List.map printCompletionItem (#items a))))]
+
type initializeResponse = { capabilities:
{ hoverProvider: bool
+ , completionProvider: {triggerCharacters: string list} option
, textDocumentSync:
{ openClose: bool
+ , change: int (* 0 = None, 1 = Full, 2 = Incremental *)
, save: { includeText: bool } option
}
}}
@@ -246,11 +333,16 @@ structure LspSpec (* :> LSPSPEC *) = struct
val capabilities = #capabilities res
in
Json.Obj [ ("hoverProvider", Json.Bool (#hoverProvider capabilities))
+ , ("completionProvider", case #completionProvider capabilities of
+ NONE => Json.Null
+ | SOME cp => Json.Obj [("triggerCharacters", Json.Array (List.map Json.String (#triggerCharacters cp)))]
+ )
, ("textDocumentSync",
let
val textDocumentSync = #textDocumentSync capabilities
in
Json.Obj [ ("openClose", Json.Bool (#openClose textDocumentSync ))
+ , ("change", Json.Int (#change textDocumentSync))
, ("save", case #save textDocumentSync of
NONE => Json.Null
| SOME save => Json.Obj [("includeText", Json.Bool (#includeText save) )])]
@@ -273,6 +365,7 @@ structure LspSpec (* :> LSPSPEC *) = struct
{ initialize: initializeParams -> initializeResponse result
, shutdown: unit -> unit result
, textDocument_hover: toclient -> hoverReq -> hoverResp result
+ , textDocument_completion: completionReq -> completionResp result
}
fun showMessage str typ =
@@ -316,13 +409,19 @@ structure LspSpec (* :> LSPSPEC *) = struct
((#textDocument_hover handlers)
toclient
(parseHoverReq (#params requestMessage)))
+ | "textDocument/completion" =>
+ mapResult
+ printCompletionResp
+ ((#textDocument_completion handlers)
+ (parseCompletionReq (#params requestMessage)))
| "shutdown" =>
mapResult
(fn () => Json.Null)
((#shutdown handlers) ())
| "exit" =>
OS.Process.exit OS.Process.success
- | method => Error (~32601, "Method not supported: " ^ method)
+ | method => (debug ("Method not supported: " ^ method);
+ Error (~32601, "Method not supported: " ^ method))
(* val () = (TextIO.output (TextIO.stdErr, "Got result: " ^ (case result of Success _ => "success\n" *)
(* | Error _ => "error\n")); TextIO.flushOut TextIO.stdErr) *)
in
@@ -418,13 +517,21 @@ structure SM = BinaryMapFn(SK)
type fileState =
{ envBeforeThisModule: ElabEnv.env
- , decls : Elab.decl list }
+ , decls: Elab.decl list
+ , text: string}
type state =
{ urpPath : string
, fileStates : fileState SM.map
}
val stateRef = ref (NONE: state option)
+fun insertFileState (state: state) (fileName: string) (fs: fileState) =
+ stateRef := SOME { urpPath = #urpPath state
+ , fileStates = SM.insert ( #fileStates state
+ , fileName
+ , fs)
+ }
+
fun scanDir (f: string -> bool) (path: string) =
let
val dir = OS.FileSys.openDir path
@@ -491,12 +598,12 @@ fun errorToDiagnostic (err: { span: ErrorMsg.span , message: string }): LspSpec.
(* TODO FFI modules ? Check compiler.sml -> parse -> parseFfi *)
(* TODO Optim: cache parsed urp file? *)
-fun calculateFileState (state: state) (fileName: string): (fileState option * LspSpec.diagnostic list) =
+fun elabFile (state: state) (fileName: string): ({ decls: Elab.decl list, envBeforeThisModule: ElabEnv.env} option * LspSpec.diagnostic list) =
let
val () = if (OS.Path.ext fileName = SOME "ur")
then ()
else raise Fail ("Can only handle .ur files for now")
- val () = Elaborate.unifyMore := true
+ (* val () = Elaborate.unifyMore := true *)
(* To reuse Basis and Top *)
val () = Elaborate.incremental := true
(* Parsing .urp *)
@@ -597,20 +704,29 @@ fun calculateFileState (state: state) (fileName: string): (fileState option * Ls
end
end
-fun handleFullDocument (state: state) (toclient: LspSpec.toclient) (documentUri: LspSpec.documentUri) =
+fun handleDocumentSavedOrOpened (state: state) (toclient: LspSpec.toclient) (documentUri: LspSpec.documentUri) (textO: string option) =
let
- val path = #path documentUri
- val res = calculateFileState state path
+ val fileName = #path documentUri
+ val res = elabFile state fileName
+ val text = case textO of
+ NONE => (case SM.find (#fileStates state, fileName) of
+ NONE => ((#showMessage toclient) ("No previous state for file " ^ fileName) 2; NONE)
+ | SOME previousState => SOME (#text previousState))
+ | SOME text => SOME text
in
- (case #1 res of
- NONE => ()
- | SOME fs =>
- stateRef := SOME { urpPath = #urpPath state
- , fileStates = SM.insert ( #fileStates state
- , path
- , fs)
- }) ;
- #publishDiagnostics toclient { uri = documentUri , diagnostics = #2 res}
+ case text of
+ NONE => ()
+ | SOME text =>
+ (case #1 res of
+ NONE =>
+ insertFileState state fileName { text = text
+ , envBeforeThisModule = ElabEnv.empty
+ , decls = [] }
+ | SOME fs =>
+ (insertFileState state fileName { text = text
+ , envBeforeThisModule = #envBeforeThisModule fs
+ , decls = #decls fs });
+ #publishDiagnostics toclient { uri = documentUri , diagnostics = #2 res})
end
fun scanDir (f: string -> bool) (path: string) =
@@ -640,6 +756,19 @@ fun readFile (fileName: string): string =
end
+(* TODO I couldn't figure out how to print just to a string, so writing to a temp file, then reading it, then deleting it, ... *)
+fun ppToString (pp: Print.PD.pp_desc) (width: int): string =
+ let
+ val tempfile = OS.FileSys.tmpName ()
+ val outStr = TextIO.openOut tempfile
+ val outDev = TextIOPP.openOut {dst = outStr, wid = width}
+ val () = Print.fprint outDev pp
+ val res = readFile tempfile
+ val () = TextIO.closeOut outStr
+ in
+ res
+ end
+
fun handleHover (state: state) (p: LspSpec.hoverReq): LspSpec.hoverResp LspSpec.result =
let
val fileName = #path (#uri (#textDocument p))
@@ -652,17 +781,203 @@ fun handleHover (state: state) (p: LspSpec.hoverReq): LspSpec.hoverResp LspSpec.
val env = #envBeforeThisModule s
val decls = #decls s
val loc = #position p
- val pp = GetInfo.getInfo env (Elab.StrConst decls) fileName { line = #line loc + 1
- , character = #character loc + 1}
- (* TODO I couldn't figure out how to print just to a string, so writing to a temp file, then reading it, then deleting it, ... *)
- val tempfile = OS.FileSys.tmpName ()
- val outStr = TextIO.openOut tempfile
- val outDev = TextIOPP.openOut {dst = outStr, wid = 70}
- val () = Print.fprint outDev pp
- val res = readFile tempfile
- val () = TextIO.closeOut outStr
+ val result = GetInfo.getInfo env (Elab.StrConst decls) fileName { line = #line loc + 1
+ , character = #character loc + 1}
+ in
+ case #smallestgoodpart result of
+ NONE => LspSpec.Success NONE
+ | SOME {desc = desc, ...} =>
+ LspSpec.Success (SOME {contents = ppToString desc 70})
+ end
+ end
+
+fun getCompletionsFromFields (env: ElabEnv.env) (prefix: string) (searchStr: string) (fields: (Elab.con * Elab.con) list): LspSpec.completionItem list =
+ let
+ fun mapF (c1, c2) =
+ case c1 of
+ (Elab.CName fieldName, _) =>
+ if String.isPrefix searchStr fieldName
+ then SOME { label = prefix ^ fieldName
+ , kind = LspSpec.Field
+ , detail = ppToString (ElabPrint.p_con env c2) 150
+ }
+ else NONE
+ | _ => NONE
+ in
+ List.mapPartial mapF fields
+ end
+
+fun getCompletionsFromSignatureItems (env: ElabEnv.env) (prefix: string) (searchStr: string) (items: Elab.sgn_item list): LspSpec.completionItem list =
+ let
+ fun mapF item =
+ case item of
+ (Elab.SgiVal (name, _, con), _) =>
+ if String.isPrefix searchStr name
+ then [{ label = prefix ^ name
+ , kind = LspSpec.Value
+ , detail = ppToString (ElabPrint.p_con env con) 150
+ }]
+ else []
+ | (Elab.SgiCon (name, _, _, con), _) =>
+ if String.isPrefix searchStr name
+ then [{ label = prefix ^ name
+ , kind = LspSpec.Variable
+ , detail = ppToString (ElabPrint.p_con env con) 150
+ }]
+ else []
+ | (Elab.SgiDatatype cs, _) =>
+ (List.concat
+ (List.map (fn (constr as (dtName, n, xs, constrs)) =>
+ (* Copied from elab_print *)
+ 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
+ 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
+ }
+ else NONE) constrs
+ end)
+ cs))
+ | (Elab.SgiDatatypeImp _, _) =>
+ (* TODO ??? no idea what this is *)
+ []
+ | (Elab.SgiStr (_, name, _, _), _) =>
+ if String.isPrefix searchStr name
+ then [{ label = prefix ^ name
+ , kind = LspSpec.Module
+ , detail = ""
+ }]
+ else []
+ | (Elab.SgiClass (name, _, _, con), _) =>
+ if String.isPrefix searchStr name
+ then [{ label = prefix ^ name
+ , kind = LspSpec.Class
+ , detail = ppToString (ElabPrint.p_con env con) 150
+ }]
+ else []
+ | _ => []
+ in
+ List.concat (List.map mapF items)
+ end
+
+fun findMatchingStringInEnv (env: ElabEnv.env) (str: string): LspSpec.completionItem list =
+ let
+ val splitted = Substring.fields (fn c => c = #".") (Substring.full str)
+ in
+ case splitted of
+ (_ :: []) =>
+ if str = ""
+ then []
+ else (List.map (fn (name,con) =>
+ { label = name
+ , kind = LspSpec.Variable
+ , detail = ppToString (ElabPrint.p_con env con) 150
+ })
+ (ElabEnv.matchRelEByPrefix env str
+ @ ElabEnv.matchNamedEByPrefix env str))
+ | (r :: str :: []) =>
+ if Char.isUpper (Substring.sub (r, 0))
+ then (* r should be a structure *)
+ let
+ (* TODO Perf: first match and then equal is not perfect *)
+ val foundStrs = ElabEnv.matchStrByPrefix env (Substring.string r)
+ val filteredStrs = List.filter (fn (name,_) => name = Substring.string r) foundStrs
+ in
+ (case List.map (fn (name, (i, sgn)) => (name, ElabEnv.hnormSgn env sgn)) filteredStrs of
+ [] => []
+ | (name, (Elab.SgnConst sgis, _)) :: _ =>
+ getCompletionsFromSignatureItems env (name ^ ".") (Substring.string str) sgis
+ | _ => [])
+ end
+ else (* r should be a record *)
+ (* TODO is it correct to first try RelE and then NamedE? *)
+ let
+ (* TODO Perf: first match and then equal is not perfect *)
+ val foundRelEs = ElabEnv.matchRelEByPrefix env (Substring.string r)
+ val foundNamedEs = ElabEnv.matchNamedEByPrefix env (Substring.string r)
+ val filteredEs = List.filter (fn (name,_) => name = Substring.string r) (foundRelEs @ foundNamedEs)
+ in
+ (case List.map (fn (name, c) => (name, ElabOps.reduceCon env c)) filteredEs of
+ [] => []
+ | (name, (Elab.TRecord (Elab.CRecord (_, fields), _), _)) :: _ =>
+ getCompletionsFromFields env (name ^ ".") (Substring.string str) fields
+ | _ => [])
+ end
+ | _ => []
+ end
+
+(* TODO can we use the real parser to figure out what we're typing (exp, con, field, etc) to predict better? *)
+fun handleCompletion (state: state) (p: LspSpec.completionReq) =
+ let
+ val fileName = #path (#uri (#textDocument p))
+ val s = SM.find (#fileStates state, fileName)
+ in
+ case s of
+ NONE => LspSpec.Success { isIncomplete = false, items = []}
+ | SOME s =>
+ let
+ val pos = #position p
+ val line = List.nth (Substring.fields (fn c => c = #"\n") (Substring.full (#text s)), #line pos)
+ val () = debug ("line" ^ Substring.string line)
+ val chars = [ (* #".", *) #"(", #")", #"{", #"}", #"[", #"]", #"<", #">", #"-", #"=", #":"
+ , #" ", #"\n", #"#", #",", #"*", #"\"", #"|", #"&", #"$", #"^", #"+", #";"]
+ val lineUntilPos = Substring.slice (line, 0, SOME (#character pos))
+ val () = debug ("lineUntilPos: \"" ^ Substring.string lineUntilPos ^ "\"")
+ val searchStr = Substring.string (Substring.taker (fn c => not (List.exists (fn c' => c = c') chars)) lineUntilPos)
+ val () = debug ("Looking for completions for: \"" ^ searchStr ^ "\"")
+ val env = #envBeforeThisModule s
+ val decls = #decls s
+ val getInfoRes = GetInfo.getInfo env (Elab.StrConst decls) fileName { line = #line pos + 1
+ , character = #character pos + 1}
+ val envOfSmallest = #env (#smallest getInfoRes)
+ in
+ LspSpec.Success { isIncomplete = false
+ , items = findMatchingStringInEnv envOfSmallest searchStr}
+ end
+ end
+
+fun applyContentChange ((c, s): LspSpec.contentChange * string): string =
+ case (#range c, #rangeLength c) of
+ (SOME range, SOME _) =>
+ let
+ val lines = Substring.fields (fn c => c = #"\n") (Substring.full s)
+ val linesBefore = List.take (lines, #line (#start range))
+ val linesAfter = List.drop (lines, #line (#end_ range) + 1)
+ val startLine = List.nth (lines, #line (#start range))
+ val startText = Substring.slice (startLine, 0, SOME (#character (#start range)))
+ val endLine = List.nth (lines, #line (#end_ range))
+ val endText = Substring.triml (#character (#end_ range)) endLine
+ in
+ Substring.concatWith "\n" (linesBefore
+ @ [Substring.full (Substring.concat [startText, Substring.full (#text c), endText])]
+ @ linesAfter)
+ end
+ | _ =>
+ #text c
+
+fun handleDocumentDidChange (state: state) (toclient: LspSpec.toclient) (p: LspSpec.didChangeParams): unit =
+ let
+ val fileName = #path (#uri (#textDocument p))
+ val s = SM.find (#fileStates state, fileName)
+ in
+ case s of
+ NONE =>
+ (debug ("Got change event for file that isn't open: " ^ fileName);
+ (#showMessage toclient) ("Got change event for file that isn't open: " ^ fileName) 1)
+ | SOME s =>
+ let
+ val newtext = List.foldl applyContentChange (#text s) (#contentChanges p)
in
- LspSpec.Success (SOME {contents = res})
+ insertFileState state fileName { text = newtext
+ , decls = #decls s
+ , envBeforeThisModule = #envBeforeThisModule s}
end
end
@@ -686,14 +1001,17 @@ fun serverLoop () =
LspSpec.Success
{ capabilities =
{ hoverProvider = true
+ , completionProvider = SOME { triggerCharacters = ["."]}
, textDocumentSync = { openClose = true
+ , change = 2
, save = SOME { includeText = false }
}}
}
end)
handle (Fail str) => LspSpec.Error (~32602, str)
, shutdown = fn () => LspSpec.Error (~32002, "Server not initialized")
- , textDocument_hover = fn ctx => fn _ => LspSpec.Error (~32002, "Server not initialized")
+ , textDocument_hover = fn toclient => fn _ => LspSpec.Error (~32002, "Server not initialized")
+ , textDocument_completion = fn _ => LspSpec.Error (~32002, "Server not initialized")
}
| LspSpec.Notification n => ())
| SOME state =>
@@ -702,9 +1020,9 @@ fun serverLoop () =
((LspSpec.handleNotification
n
{ initialized = fn () => ()
- , textDocument_didOpen = fn ctx => fn p => handleFullDocument state ctx (#uri (#textDocument p))
- , textDocument_didChange = fn ctx => fn didChangeParams => ()
- , textDocument_didSave = fn ctx => fn p => handleFullDocument state ctx (#uri (#textDocument p))
+ , textDocument_didOpen = fn toclient => fn p => handleDocumentSavedOrOpened state toclient (#uri (#textDocument p)) (SOME (#text (#textDocument p)))
+ , textDocument_didChange = handleDocumentDidChange state
+ , textDocument_didSave = fn toclient => fn p => handleDocumentSavedOrOpened state toclient (#uri (#textDocument p)) NONE
})
handle LspError e => handleLspErrorInNotification e
| ex => handleLspErrorInNotification (InternalError (General.exnMessage ex)))
@@ -714,7 +1032,8 @@ fun serverLoop () =
m
{ initialize = fn _ => LspSpec.Error (~32600, "Server already initialized")
, shutdown = fn () => LspSpec.Success ()
- , textDocument_hover = fn ctx => fn p => handleHover state p
+ , textDocument_hover = fn toclient => handleHover state
+ , textDocument_completion = handleCompletion state
})
handle LspError e => handleLspErrorInRequest (#id m) e
| ex => handleLspErrorInRequest (#id m) (InternalError (General.exnMessage ex)))