Merge pull request #795 from coq-community/overview

Capabilities for outline

Author: rtetley

language-server/dm/document.ml

@@ -22,6 +22,20 @@ module LM = Map.Make (Int)
 
 module SM = Map.Make (Stateid)
 
+type proof_block_type =
+  | TheoremKind of Decls.theorem_kind
+  | DefinitionType of Decls.definition_object_kind
+
+type outline_element = {
+  id: sentence_id;
+  name: string;
+  type_: proof_block_type;
+  statement: string;
+  range: Range.t
+}
+
+type outline = outline_element list
+
 type parsed_ast = {
   ast: Synterp.vernac_control_entry;
   classification: Vernacextend.vernac_classification;
@@ -71,15 +85,12 @@ type document = {
   parsing_errors_by_end : parsing_error LM.t;
   comments_by_end : comment LM.t;
   schedule : Scheduler.schedule;
+  outline : outline;
   parsed_loc : int;
   raw_doc : RawDocument.t;
   init_synterp_state : Vernacstate.Synterp.t;
 }
 
-let schedule doc = doc.schedule
-
-let raw_document doc = doc.raw_doc
-
 let range_of_sentence raw (sentence : sentence) =
   let start = RawDocument.position_of_loc raw sentence.start in
   let end_ = RawDocument.position_of_loc raw sentence.stop in
@@ -100,6 +111,61 @@ let range_of_id_with_blank_space document id =
   | None -> CErrors.anomaly Pp.(str"Trying to get range of non-existing sentence " ++ Stateid.print id)
   | Some sentence -> range_of_sentence_with_blank_space document.raw_doc sentence
 
+
+let record_outline document id (ast : Synterp.vernac_control_entry) classif (outline : outline) =
+  let open Vernacextend in
+  match classif with
+  | VtStartProof (_, names) ->
+    let vernac_gen_expr = ast.v.expr in
+    let type_ = match vernac_gen_expr with
+      | VernacSynterp _ -> None
+      | VernacSynPure pure -> 
+        match pure with
+        | Vernacexpr.VernacStartTheoremProof (kind, _) -> Some (TheoremKind kind)
+        | Vernacexpr.VernacDefinition ((_, def), _, _) -> Some (DefinitionType def)
+        | _ -> None
+    in
+    let name = match names with
+    |[] -> "default"
+    | n :: _ -> Names.Id.to_string n 
+    in
+    let statement = "" in
+    begin match type_ with
+    | None -> outline
+    | Some type_ ->
+      let range = range_of_id document id in
+      let element = {id; type_; name; statement; range} in
+      element :: outline
+    end
+  | VtSideff (names, _) ->
+    let vernac_gen_expr = ast.v.expr in
+    let type_ = match vernac_gen_expr with
+      | VernacSynterp _ -> None
+      | VernacSynPure pure -> 
+        match pure with
+        | Vernacexpr.VernacStartTheoremProof (kind, _) -> Some (TheoremKind kind)
+        | Vernacexpr.VernacDefinition ((_, def), _, _) -> Some (DefinitionType def)
+        | _ -> None
+    in
+    let name = match names with
+    |[] -> "default"
+    | n :: _ -> Names.Id.to_string n 
+    in
+    let statement = "" in
+    begin match type_ with
+    | None -> outline
+    | Some type_ ->
+      let range = range_of_id document id in
+      let element = {id; type_; name; statement; range} in
+      element :: outline
+    end
+  | _ -> outline
+
+let schedule doc = doc.schedule
+
+let raw_document doc = doc.raw_doc
+
+let outline doc = doc.outline
 let parse_errors parsed =
   List.map snd (LM.bindings parsed.parsing_errors_by_end)
 
@@ -111,19 +177,23 @@ let add_sentence parsed parsing_start start stop (ast: parsed_ast) synterp_state
   in
   (* FIXME may invalidate scheduler_state_XXX for following sentences -> propagate? *)
   let sentence = { parsing_start; start; stop; ast; id; synterp_state; scheduler_state_before; scheduler_state_after } in
-  { parsed with sentences_by_end = LM.add stop sentence parsed.sentences_by_end;
+  let document = { 
+    parsed with sentences_by_end = LM.add stop sentence parsed.sentences_by_end;
     sentences_by_id = SM.add id sentence parsed.sentences_by_id;
-    schedule
-  }, scheduler_state_after
+    schedule;
+  } in
+  let outline = record_outline document id ast.ast ast.classification parsed.outline in
+  {document with outline}, scheduler_state_after
 
 let remove_sentence parsed id =
   match SM.find_opt id parsed.sentences_by_id with
   | None -> parsed
   | Some sentence ->
     let sentences_by_id = SM.remove id parsed.sentences_by_id in
     let sentences_by_end = LM.remove sentence.stop parsed.sentences_by_end in
+    let outline = List.filter (fun (e : outline_element) -> e.id != id) parsed.outline in
     (* TODO clean up the schedule and free cached states *)
-    { parsed with sentences_by_id; sentences_by_end; }
+    { parsed with sentences_by_id; sentences_by_end; outline }
 
 let sentences parsed =
   List.map snd @@ SM.bindings parsed.sentences_by_id
@@ -490,6 +560,7 @@ let create_document init_synterp_state text =
       parsing_errors_by_end = LM.empty;
       comments_by_end = LM.empty;
       schedule = initial_schedule;
+      outline = [];
       init_synterp_state;
     }
 

language-server/dm/document.mli

@@ -22,8 +22,24 @@ open Lsp.Types
     sentences *)
 type document
 
+type proof_block_type =
+  | TheoremKind of Decls.theorem_kind
+  | DefinitionType of Decls.definition_object_kind
+
+type outline_element = {
+    id: sentence_id;
+    name: string;
+    type_: proof_block_type;
+    statement: string;
+    range: Range.t
+  }
+
+type outline = outline_element list
+
 val raw_document : document -> RawDocument.t
 
+val outline : document -> outline
+
 val create_document : Vernacstate.Synterp.t -> string -> document
 (** [create_document init_synterp_state text] creates a fresh document with content defined by
     [text] under [init_synterp_state]. *)

language-server/dm/documentManager.ml

@@ -246,6 +246,18 @@ let clear_observe_id st =
 let reset_to_top st =
   { st with observe_id = Some Top }
 
+let get_document_symbols st =
+  let outline = Document.outline st.document in
+  let to_document_symbol elem =
+    let Document.{name; statement; range; type_} = elem in
+    let kind = begin match type_ with
+    | TheoremKind _ -> SymbolKind.Function
+    | DefinitionType _ ->SymbolKind.Variable
+    end in
+    DocumentSymbol.{name; detail=(Some statement); kind; range; selectionRange=range; children=None; deprecated=None; tags=None;}
+  in
+  List.map to_document_symbol outline
+
 let interpret_to st id =
   let observe_id = if st.observe_id = None then None else (Some (Id id)) in
   let st = { st with observe_id} in

language-server/dm/documentManager.mli

@@ -87,6 +87,8 @@ val observe_id_range : state -> Range.t option
 
 val get_messages : state -> Position.t option -> (DiagnosticSeverity.t * pp) list
 
+val get_document_symbols : state -> DocumentSymbol.t list
+
 val all_diagnostics : state -> Diagnostic.t list
 (** all_diagnostics [doc] returns the diagnostics corresponding to the sentences
     that have been executed in [doc]. *)

language-server/dm/scheduler.ml

@@ -44,6 +44,8 @@ type task =
   | SubProof of ast list
   | ModuleWithSignature of ast list
 *)
+
+
 type proof_block = {
   proof_sentences : executable_sentence list;
   opener_id : sentence_id;

language-server/vscoqtop/lspManager.ml

@@ -146,11 +146,13 @@ let do_initialize id params =
   end;
   let textDocumentSync = `TextDocumentSyncKind TextDocumentSyncKind.Incremental in
   let completionProvider = CompletionOptions.create ~resolveProvider:false () in
+  let documentSymbolProvider = `Bool true in
   let hoverProvider = `Bool true in
   let capabilities = ServerCapabilities.create
     ~textDocumentSync
     ~completionProvider
     ~hoverProvider
+    ~documentSymbolProvider
   ()
   in
   let initialize_result = Lsp.Types.InitializeResult.{
@@ -438,6 +440,14 @@ let textDocumentCompletion id params =
       let message = e in
       Error(message), []
 
+let documentSymbol id params =
+  let Lsp.Types.DocumentSymbolParams.{ textDocument = {uri}} = params in
+  match Hashtbl.find_opt states (DocumentUri.to_path uri) with
+  | None -> log @@ "[documentSymbol] ignoring event on non existant document"; Error("Document does not exist"), []
+  | Some tab -> log @@ "[documentSymbol] getting symbols";
+    let symbols = Dm.DocumentManager.get_document_symbols tab.st in
+    Ok(Some (`DocumentSymbol symbols)), []
+
 let coqtopResetCoq id params =
   let Request.Client.ResetParams.{ textDocument = { uri } } = params in
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
@@ -529,6 +539,8 @@ let dispatch_std_request : type a. Jsonrpc.Id.t -> a Lsp.Client_request.t -> (a,
     textDocumentCompletion id params
   | TextDocumentHover params ->
     textDocumentHover id params, []
+  | DocumentSymbol params ->
+    documentSymbol id params
   | UnknownRequest _ | _  -> Error "Received unknown request", []
 
 let dispatch_request : type a. Jsonrpc.Id.t -> a Request.Client.t -> (a,string) result * events =