Added tracking of text of source files and autocomplete

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)))