feat: adding sections and modules in outlines

We now support sections and modules which contain document symbols in
the outline.

Author: rtetley

language-server/dm/document.ml

@@ -26,6 +26,9 @@ type proof_block_type =
   | TheoremKind of Decls.theorem_kind
   | DefinitionType of Decls.definition_object_kind
   | InductiveType of Vernacexpr.inductive_kind
+  | BeginSection
+  | BeginModule
+  | End
   | Other
 
 type proof_step = {
@@ -210,6 +213,11 @@ let record_outline document id (ast : Synterp.vernac_control_entry) classif (out
     let vernac_gen_expr = ast.v.expr in
     let type_, statement = match vernac_gen_expr with
       | VernacSynterp (Synterp.EVernacExtend _) when names <> [] -> Some Other, "external"
+      | VernacSynterp (Synterp.EVernacBeginSection  _) -> log (fun () -> Format.sprintf "BEGIN SECTION %s" (string_of_id document id)); Some BeginSection, ""
+      | VernacSynterp (Synterp.EVernacDeclareModuleType  _) -> log (fun () -> Format.sprintf "BEGIN MODULE %s" (string_of_id document id)); Some BeginModule, ""
+      | VernacSynterp (Synterp.EVernacDefineModule  _) -> log (fun () -> Format.sprintf "BEGIN MODULE %s" (string_of_id document id)); Some BeginModule, ""
+      | VernacSynterp (Synterp.EVernacDeclareModule  _) -> log (fun () -> Format.sprintf "BEGIN MODULE %s" (string_of_id document id)); Some BeginModule, ""
+      | VernacSynterp (Synterp.EVernacEndSegment  _) -> log (fun () -> Format.sprintf "END SEGMENT"); Some End, ""
       | VernacSynterp _ -> None, ""
       | VernacSynPure pure -> 
         match pure with

language-server/dm/document.mli

@@ -26,6 +26,9 @@ type proof_block_type =
   | TheoremKind of Decls.theorem_kind
   | DefinitionType of Decls.definition_object_kind
   | InductiveType of Vernacexpr.inductive_kind
+  | BeginSection
+  | BeginModule
+  | End
   | Other
 
 type proof_step = {

language-server/dm/documentManager.ml

@@ -351,19 +351,55 @@ let get_document_proofs st =
   let proofs, _  = List.partition is_theorem outline in
   List.map mk_proof_block proofs
 
-let get_document_symbols st =
-  let outline = Document.outline st.document in
+let rec get_document_symbols outline (sec_or_m: DocumentSymbol.t option) symbols =
+  let record_in_outline outline symbol sec_or_m =
+    match sec_or_m with
+    | None ->
+      let symbols = symbols @ [symbol] in
+      get_document_symbols outline sec_or_m symbols
+    | Some sec_or_m ->
+      let children = match sec_or_m.children with
+        | None -> Some [symbol]
+        | Some l -> Some (l @ [symbol])
+      in
+      let sec_or_m = Some {sec_or_m with children} in
+      get_document_symbols outline sec_or_m symbols
+  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
     | InductiveType _ -> SymbolKind.Struct
     | Other -> SymbolKind.Null
+    | BeginSection | BeginModule -> SymbolKind.Class
+    | End -> SymbolKind.Null
     end in
     DocumentSymbol.{name; detail=(Some statement); kind; range; selectionRange=range; children=None; deprecated=None; tags=None;}
   in
-  List.map to_document_symbol outline
+  match outline with
+  | [] -> symbols
+  | e :: l ->
+    let Document.{type_} = e in
+    match type_ with
+    | TheoremKind _ | DefinitionType _ | InductiveType _  | Other ->
+      let symbol = to_document_symbol e in
+      record_in_outline l symbol sec_or_m
+    | BeginSection ->
+      let symbol = to_document_symbol e in
+      get_document_symbols l (Some symbol) symbols
+    | BeginModule ->
+      let symbol = to_document_symbol e in
+      get_document_symbols l (Some symbol) symbols
+    | End ->
+      match sec_or_m with
+      | None -> log(fun () -> "Trying to end a module or section with no begin"); get_document_symbols l None symbols
+      | Some symbol ->
+        get_document_symbols l None (symbols @ [symbol])
+
+let get_document_symbols st =
+  let outline = List.rev @@ Document.outline st.document in
+  get_document_symbols outline None []
 
 let interpret_to st id check_mode =
   let observe_id = (Id id) in