Merge pull request #1045 from KacperFKorban/symbol-search/handle-indu…

…ctive-and-fixpoint Symbol search: handle inductive, fixpoint, and cofixpoint
coq · Feb 21, 2025 · 412a8c3 · 412a8c3
2 parents 4dafbd4 + f293259
commit 412a8c3
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 0 deletions.
diff --git a/language-server/dm/document.ml b/language-server/dm/document.ml
@@ -25,6 +25,7 @@ module SM = Map.Make (Stateid)
 type proof_block_type =
   | TheoremKind of Decls.theorem_kind
   | DefinitionType of Decls.definition_object_kind
+  | InductiveType of Vernacexpr.inductive_kind
   | Other
 
 type proof_step = {
@@ -189,6 +190,8 @@ let record_outline document id (ast : Synterp.vernac_control_entry) classif (out
         match pure with
         | Vernacexpr.VernacStartTheoremProof (kind, _) -> Some (TheoremKind kind)
         | Vernacexpr.VernacDefinition ((_, def), _, _) -> Some (DefinitionType def)
+        | Vernacexpr.VernacFixpoint (_, _) -> Some (DefinitionType Decls.Fixpoint)
+        | Vernacexpr.VernacCoFixpoint (_, _) -> Some (DefinitionType Decls.CoFixpoint)
         | _ -> None
     in
     let name = match names with
@@ -212,6 +215,9 @@ let record_outline document id (ast : Synterp.vernac_control_entry) classif (out
         match pure with
         | Vernacexpr.VernacStartTheoremProof (kind, _) -> Some (TheoremKind kind), string_of_id document id
         | Vernacexpr.VernacDefinition ((_, def), _, _) -> Some (DefinitionType def), string_of_id document id
+        | Vernacexpr.VernacInductive (kind, _) -> Some (InductiveType kind), string_of_id document id
+        | Vernacexpr.VernacFixpoint (_, _) -> Some (DefinitionType Decls.Fixpoint), string_of_id document id
+        | Vernacexpr.VernacCoFixpoint (_, _) -> Some (DefinitionType Decls.CoFixpoint), string_of_id document id
         | _ -> None, ""
     in
     let name = match names with

diff --git a/language-server/dm/document.mli b/language-server/dm/document.mli
@@ -25,6 +25,7 @@ type document
 type proof_block_type =
   | TheoremKind of Decls.theorem_kind
   | DefinitionType of Decls.definition_object_kind
+  | InductiveType of Vernacexpr.inductive_kind
   | Other
 
 type proof_step = {

diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml
@@ -358,6 +358,7 @@ let get_document_symbols st =
     let kind = begin match type_ with
     | TheoremKind _ -> SymbolKind.Function
     | DefinitionType _ -> SymbolKind.Variable
+    | InductiveType _ -> SymbolKind.Struct
     | Other -> SymbolKind.Null
     end in
     DocumentSymbol.{name; detail=(Some statement); kind; range; selectionRange=range; children=None; deprecated=None; tags=None;}