Merge pull request #563 from coq-community/ocaml-lsp

Use ocaml-lsp datatypes for base LSP

Author: maximedenes

flake.nix

@@ -47,9 +47,10 @@
           ppx_assert
           ppx_sexp_conv
           ppx_deriving
+          ppx_import
           sexplib
           ppx_yojson_conv
-          uri
+          lsp
         ]);
       };
 

language-server/dm/completionSuggester.ml

@@ -11,6 +11,7 @@
 (*   See LICENSE file.                                                    *)
 (*                                                                        *)
 (**************************************************************************)
+open Protocol
 
 module CompactedDecl = Context.Compacted.Declaration
 open Printer
@@ -326,7 +327,7 @@ module Structured = struct
 
   (* A Lower score is better as we are sorting in ascending order *)
 
-  let rank (options: Lsp.LspData.Settings.Completion.t) (goal, goal_evar) sigma env lemmas : CompletionItems.completion_item list =
+  let rank (options: Settings.Completion.t) (goal, goal_evar) sigma env lemmas : CompletionItems.completion_item list =
     let size_impact = options.sizeFactor in
     let atomic_factor = options.atomicFactor in
     let finalScore score size = Float.sub size (Float.mul score size_impact) in
@@ -379,7 +380,7 @@ module SelectiveUnification = struct
     |> List.stable_sort (fun a b -> compare (snd a) (snd b))
     |> List.map fst
 
-  let selectiveRank (options: Lsp.LspData.Settings.Completion.t) (goal : Evd.econstr) sigma env (lemmas : CompletionItems.completion_item list) : CompletionItems.completion_item list =
+  let selectiveRank (options: Settings.Completion.t) (goal : Evd.econstr) sigma env (lemmas : CompletionItems.completion_item list) : CompletionItems.completion_item list =
     try 
       let take, skip = takeSkip options.unificationLimit lemmas in
       List.append (rankByUnifiability goal sigma env take) skip
@@ -390,8 +391,8 @@ module SelectiveUnification = struct
   let rank = selectiveRank
 end
 
-let rank_choices (options: Lsp.LspData.Settings.Completion.t) (goal, goal_evar) sigma env lemmas = 
-  let open Lsp.LspData.Settings.Completion.RankingAlgoritm in
+let rank_choices (options: Settings.Completion.t) (goal, goal_evar) sigma env lemmas = 
+  let open Settings.Completion.RankingAlgoritm in
   match options.algorithm with
   | SplitTypeIntersection -> TypeIntersection.rank goal sigma env lemmas
   | StructuredSplitUnification -> SelectiveUnification.rank options goal sigma env (Structured.rank options (goal, goal_evar) sigma env lemmas)

language-server/dm/completionSuggester.mli

@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-open Lsp.LspData
+open Protocol
 open CompletionItems
 
 val get_completions : Settings.Completion.t -> Vernacstate.t -> completion_item list option

language-server/dm/document.ml

@@ -12,9 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 open Gramlib
-open Lsp
-open LspData
 open Types
+open Lsp.Types
 open Scheduler
 
 let Log log = Log.mk_log "document"

language-server/dm/document.mli

@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 open Types
-open Lsp.LspData
+open Lsp.Types
 
 (** This file defines operations on the content of a document (text, parsing
     of sentences, scheduling). *)

language-server/dm/documentManager.ml

@@ -12,13 +12,15 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Lsp.Types
+open Protocol
+open Protocol.LspWrapper
 open Types
-open Lsp.LspData
 
 let Log log = Log.mk_log "documentManager"
 
 type state = {
-  uri : Uri.t;
+  uri : DocumentUri.t;
   init_vs : Vernacstate.t;
   opts : Coqargs.injection_command list;
   document : Document.document;
@@ -115,7 +117,7 @@ let make_diagnostic doc range oloc message severity =
     | Some loc ->
       RawDocument.range_of_loc (Document.raw_document doc) loc
   in
-  Diagnostic.{ range; message; severity }
+  Diagnostic.create ~range ~message ~severity ()
 
 let make_coq_feedback doc range oloc message channel = 
   let range =
@@ -144,15 +146,15 @@ let diagnostics st =
   (* we are resilient to a state where invalidate was not called yet *)
   let exists (id,_) = Option.has_some (Document.get_sentence st.document id) in
   let exec_errors = all_exec_errors |> List.filter exists in
-  let warnings_and_errors  (id, (lvl, oloc, msg)) = Option.map (fun lvl -> id, (lvl, oloc, msg)) (Severity.t_of_feedback_level lvl) in
+  let warnings_and_errors  (id, (lvl, oloc, msg)) = Option.map (fun lvl -> id, (lvl, oloc, msg)) (DiagnosticSeverity.of_feedback_level lvl) in
   let diags = all_feedback |> List.filter exists |> List.filter_map warnings_and_errors in
   let mk_diag (id,(lvl,oloc,msg)) = 
       make_diagnostic st.document (Document.range_of_id st.document id) oloc msg lvl
   in
-  let mk_error_diag (id,(oloc,msg)) = mk_diag (id,(Severity.Error,oloc,msg)) in
+  let mk_error_diag (id,(oloc,msg)) = mk_diag (id,(DiagnosticSeverity.Error,oloc,msg)) in
   let mk_parsing_error_diag Document.{ msg = (oloc,msg); start; stop } =
     let doc = Document.raw_document st.document in
-    let severity = Severity.Error in
+    let severity = DiagnosticSeverity.Error in
     let start = RawDocument.position_of_loc doc start in
     let end_ = RawDocument.position_of_loc doc stop in
     let range = Range.{ start; end_ } in
@@ -242,7 +244,7 @@ let validate_document state =
 
 let init init_vs ~opts uri ~text =
   Vernacstate.unfreeze_full_state init_vs;
-  let top = Coqargs.(dirpath_of_top (TopPhysical (Uri.path uri))) in
+  let top = Coqargs.(dirpath_of_top (TopPhysical (DocumentUri.to_path uri))) in
   Coqinit.start_library ~top opts;
   let init_vs = Vernacstate.freeze_full_state () in 
   let document = Document.create_document init_vs.Vernacstate.synterp text in
@@ -290,7 +292,7 @@ let get_proof st pos =
   in
   let oid = Option.cata id_of_pos st.observe_id pos in
   let ost = Option.bind oid (ExecutionManager.get_vernac_state st.execution_state) in
-  Option.bind ost Lsp.ProofState.get_proof
+  Option.bind ost ProofState.get_proof
 
 let get_context st pos =
   let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in

language-server/dm/documentManager.mli

@@ -13,7 +13,9 @@
 (**************************************************************************)
 
 open Types
-open Lsp.LspData
+open Lsp.Types
+open Protocol
+open Protocol.LspWrapper
 open CompletionItems
 
 (** The document manager holds the view that Coq has of the currently open
@@ -28,7 +30,7 @@ val pp_event : Format.formatter -> event -> unit
 
 type events = event Sel.event list
 
-val init : Vernacstate.t -> opts:Coqargs.injection_command list -> Uri.t -> text:string -> state * events
+val init : Vernacstate.t -> opts:Coqargs.injection_command list -> DocumentUri.t -> text:string -> state * events
 (** [init st opts uri text] initializes the document manager with initial vernac state
     [st] on which command line opts will be set. *)
 
@@ -72,7 +74,7 @@ val executed_ranges : state -> exec_overview
 (** returns the ranges corresponding to the sentences
     that have been executed and remotely executes *)
 
-val observe_id_range : state -> Lsp.LspData.Range.t option
+val observe_id_range : state -> Range.t option
 (** returns the range of the sentence referenced by observe_id **)
 
 val diagnostics : state -> Diagnostic.t list
@@ -83,7 +85,7 @@ val feedbacks : state -> CoqFeedback.t list
 (** feedback [doc] returns notice, info and debug level feedbacks from coq corresponding
     to the sentences that have been executed in [doc]. *)
 
-val get_proof : state -> Position.t option -> Lsp.ProofState.t option
+val get_proof : state -> Position.t option -> ProofState.t option
 
 val get_completions : state -> Position.t -> (completion_item list, string) Result.t
 
@@ -94,7 +96,7 @@ val search : state -> id:string -> Position.t -> string -> notification Sel.even
 
 val about : state -> Position.t -> pattern:string -> (string,string) Result.t
 
-val hover : state -> Position.t -> (string list) option
+val hover : state -> Position.t -> MarkupContent.t option
 (** Returns an optional Result:
     if None, the position did not have a word,
     if Some, an Ok/Error result is returned. *)

language-server/dm/dune

@@ -2,20 +2,20 @@
  (name dm)
  (public_name vscoq-language-server.dm)
  (modules :standard \ vscoqtop_proof_worker vscoqtop_tactic_worker)
- (libraries base coq-core.sysinit coq-core.vernac coq-core.parsing sel lsp language))
+ (libraries base coq-core.sysinit coq-core.vernac coq-core.parsing lsp sel protocol language))
 
 (executable
  (name vscoqtop_proof_worker)
  (public_name vscoqtop_proof_worker.opt)
  (modules vscoqtop_proof_worker)
  (flags -linkall)
  (package vscoq-language-server)
- (libraries coq-core.sysinit coq-core.tactics dm lsp))
+ (libraries coq-core.sysinit coq-core.tactics lsp dm protocol))
 
 (executable
  (name vscoqtop_tactic_worker)
  (public_name vscoqtop_tactic_worker.opt)
  (modules vscoqtop_tactic_worker)
  (flags -linkall)
  (package vscoq-language-server)
- (libraries coq-core.sysinit coq-core.tactics dm lsp))
+ (libraries coq-core.sysinit coq-core.tactics lsp dm protocol))

language-server/dm/executionManager.ml

@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Protocol
 open Scheduler
 open Types
 
@@ -41,9 +42,10 @@ type delegation_mode =
 
 type options = {
   delegation_mode : delegation_mode;
-  completion_options : Lsp.LspData.Settings.Completion.t;
+  completion_options : Settings.Completion.t;
   enableDiagnostics : bool
 }
+
 let default_options = {
   delegation_mode = CheckProofsInMaster;
   completion_options = {

language-server/dm/executionManager.mli

@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 open Types
+open Protocol
 
 (** The event manager is in charge of the actual event of tasks (as
     defined by the scheduler), caching event states and invalidating
@@ -25,7 +26,7 @@ type delegation_mode =
 
 type options = {
   delegation_mode : delegation_mode;
-  completion_options : Lsp.LspData.Settings.Completion.t;
+  completion_options : Settings.Completion.t;
   enableDiagnostics : bool;
 }
 

language-server/dm/rawDocument.ml

@@ -11,8 +11,7 @@
 (*   See LICENSE file.                                                    *)
 (*                                                                        *)
 (**************************************************************************)
-open Lsp
-open LspData
+open Lsp.Types
 
 type text_edit = Range.t * string
 

language-server/dm/rawDocument.mli

@@ -11,8 +11,7 @@
 (*   See LICENSE file.                                                    *)
 (*                                                                        *)
 (**************************************************************************)
-open Lsp
-open LspData
+open Lsp.Types
 
 type text_edit = Range.t * string
 

language-server/dm/searchQuery.ml

@@ -13,7 +13,7 @@
 (**************************************************************************)
 open Util
 open Printer
-open Lsp.LspData
+open Protocol.LspWrapper
 open Vernacexpr
 open Pp
 (* Note: this queue is not very useful today, as we process results in the main

language-server/dm/searchQuery.mli

@@ -11,7 +11,7 @@
 (*   See LICENSE file.                                                    *)
 (*                                                                        *)
 (**************************************************************************)
-open Lsp.LspData
+open Protocol.LspWrapper
 
 val query_feedback : notification Sel.event
 

language-server/dm/types.ml

@@ -11,7 +11,7 @@
 (*   See LICENSE file.                                                    *)
 (*                                                                        *)
 (**************************************************************************)
-open Lsp.LspData
+open Lsp.Types
 
 type sentence_id = Stateid.t
 type sentence_id_set = Stateid.Set.t

language-server/language/dune

@@ -1,4 +1,4 @@
 (library
  (name language)
  (public_name vscoq-language-server.language)
- (libraries coq-core.sysinit))
+ (libraries coq-core.sysinit lsp))

language-server/language/hover.ml

@@ -224,22 +224,22 @@ let ref_info env _sigma ref udecl =
   let path = Libnames.pr_path (Nametab.path_of_global ref) ++ canonical_name_info ref in
   let args = print_arguments ref in
   let args = if Pp.ismt args then [] else ["**Args:** " ^ (Pp.string_of_ppcmds (print_arguments ref))] in
-  [md_code_block @@ compactify @@ Pp.string_of_ppcmds typ]@args@
+  String.concat "\n" @@ [md_code_block @@ compactify @@ Pp.string_of_ppcmds typ]@args@
   [Format.sprintf "**%s** %s" (pr_globref_kind ref) (Pp.string_of_ppcmds path)]
 
 let mod_info mp =
-  [md_code_block @@ Format.sprintf "Module %s" (DirPath.to_string (Nametab.dirpath_of_module mp))]
+  md_code_block @@ Format.sprintf "Module %s" (DirPath.to_string (Nametab.dirpath_of_module mp))
 
 let modtype_info mp =
-  [md_code_block @@ Format.sprintf "Module Type %s" (Libnames.string_of_path (Nametab.path_of_modtype mp))]
+  md_code_block @@ Format.sprintf "Module Type %s" (Libnames.string_of_path (Nametab.path_of_modtype mp))
 
 let syndef_info kn =
-  [md_code_block @@ Format.sprintf "Notation %s" (Libnames.string_of_path (Nametab.path_of_abbreviation kn))]
+  md_code_block @@ Format.sprintf "Notation %s" (Libnames.string_of_path (Nametab.path_of_abbreviation kn))
 
 let get_hover_contents env sigma ref_or_by_not =
   match ref_or_by_not.CAst.v with
   | Constrexpr.AN qid ->
-    begin try
+    let r = begin try
       let udecl = None in
       let ref = Nametab.locate qid in
       Some (ref_info env sigma ref udecl)
@@ -258,4 +258,6 @@ let get_hover_contents env sigma ref_or_by_not =
     with Not_found ->
       None
     end
+    in
+    Option.map Lsp.Types.(fun value -> MarkupContent.create ~kind:MarkupKind.Markdown ~value) r
   | Constrexpr.ByNotation (_ntn,_sc) -> assert false

language-server/language/hover.mli

@@ -18,4 +18,4 @@ val get_hover_contents :
   env ->
   evar_map ->
   Libnames.qualid Constrexpr.or_by_notation ->
-  (string list) option
+  Lsp.Types.MarkupContent.t option