Merge pull request #831 from ejgallego/tweaks

[nits] Minor refactorings and tweaks from the JS branch.

controller/coq_lsp.ml

@@ -60,38 +60,6 @@ let concise_cb ofn =
     }
 
 (* Main loop *)
-module CB (O : sig
-  val ofn : Lsp.Base.Notification.t -> unit
-end) =
-struct
-  let ofn = O.ofn
-  let trace _hdr ?extra message = Lsp.Io.logTrace ~message ~extra
-  let message ~lvl ~message = Lsp.Io.logMessage ~lvl ~message
-
-  let diagnostics ~uri ~version diags =
-    Lsp.Core.mk_diagnostics ~uri ~version diags |> ofn
-
-  let fileProgress ~uri ~version progress =
-    Lsp.JFleche.mk_progress ~uri ~version progress |> ofn
-
-  let perfData ~uri ~version perf =
-    Lsp.JFleche.mk_perf ~uri ~version perf |> ofn
-
-  let serverVersion vi = Lsp.JFleche.mk_serverVersion vi |> ofn
-  let serverStatus st = Lsp.JFleche.mk_serverStatus st |> ofn
-
-  let cb =
-    Fleche.Io.CallBack.
-      { trace
-      ; message
-      ; diagnostics
-      ; fileProgress
-      ; perfData
-      ; serverVersion
-      ; serverStatus
-      }
-end
-
 let coq_init ~debug =
   let load_module = Dynlink.loadfile in
   let load_plugin = Coq.Loader.plugin_handler None in
@@ -130,7 +98,7 @@ let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path
 
   Lsp.Io.set_log_fn ofn_ntn;
 
-  let module CB = CB (struct
+  let module CB = Lsp_core.CB (struct
     let ofn = ofn_ntn
   end) in
   let io = CB.cb in

controller/lsp_core.ml

@@ -23,7 +23,11 @@ module F = Format
 module J = Yojson.Safe
 module U = Yojson.Safe.Util
 
-let field name dict = List.(assoc name dict)
+let field name dict =
+  try List.(assoc name dict)
+  with Not_found ->
+    raise (U.Type_error ("field " ^ name ^ " not found", `Assoc dict))
+
 let int_field name dict = U.to_int (field name dict)
 let list_field name dict = U.to_list (field name dict)
 let string_field name dict = U.to_string (field name dict)
@@ -710,3 +714,35 @@ let enqueue_message (com : LSP.Message.t) =
      general, to perform queue optimizations *)
   LspQueue.push_and_optimize com;
   set_current_token ()
+
+module CB (O : sig
+  val ofn : Lsp.Base.Notification.t -> unit
+end) =
+struct
+  let ofn = O.ofn
+  let trace _hdr ?extra message = Lsp.Io.logTrace ~message ~extra
+  let message ~lvl ~message = Lsp.Io.logMessage ~lvl ~message
+
+  let diagnostics ~uri ~version diags =
+    Lsp.Core.mk_diagnostics ~uri ~version diags |> ofn
+
+  let fileProgress ~uri ~version progress =
+    Lsp.JFleche.mk_progress ~uri ~version progress |> ofn
+
+  let perfData ~uri ~version perf =
+    Lsp.JFleche.mk_perf ~uri ~version perf |> ofn
+
+  let serverVersion vi = Lsp.JFleche.mk_serverVersion vi |> ofn
+  let serverStatus st = Lsp.JFleche.mk_serverStatus st |> ofn
+
+  let cb =
+    Fleche.Io.CallBack.
+      { trace
+      ; message
+      ; diagnostics
+      ; fileProgress
+      ; perfData
+      ; serverVersion
+      ; serverStatus
+      }
+end

controller/lsp_core.mli

@@ -63,3 +63,10 @@ val dispatch_or_resume_check :
 
 (** Add a message to the queue *)
 val enqueue_message : Lsp.Base.Message.t -> unit
+
+(** Generic output handler *)
+module CB (O : sig
+  val ofn : Lsp.Base.Notification.t -> unit
+end) : sig
+  val cb : Fleche.Io.CallBack.t
+end

coq/workspace.mli

@@ -42,6 +42,7 @@ module Require : sig
     }
 end
 
+(* Generated from a _CoqProject, dune (in the future) or command line args *)
 type t = private
   { coqlib : string
   ; coqcorelib : string

editor/code/src/goals.ts

@@ -1,12 +1,4 @@
-import {
-  Uri,
-  WebviewPanel,
-  window,
-  ViewColumn,
-  extensions,
-  commands,
-  TextDocument,
-} from "vscode";
+import { Uri, WebviewPanel, window, ViewColumn } from "vscode";
 import {
   BaseLanguageClient,
   RequestType,

examples/documentSymbol.v

@@ -8,7 +8,7 @@ Inductive foo := A | B : a -> foo.
 Inductive eh1 := Ah1 : eh2 -> eh1
 with eh2 := Bh1 : eh1 -> eh2. 
 
-Variable (j : nat).
+Axiom (j : nat).
 
 Axiom test : False.
 
@@ -34,7 +34,7 @@ End Moo.
 
 Module Bar.
 
-  Variable (u : nat).
+  Parameter (u : nat).
 
   Parameter (v : nat).