Generalize support for hover

We are still missing some cases (tactics, local context, notations).

Author: maximedenes

language-server/dm/documentManager.ml

@@ -274,7 +274,7 @@ let get_proof st pos =
 let get_context st pos =
   let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in
   match Document.find_sentence_before st.document loc with
-  | None -> None
+  | None -> Some (ExecutionManager.get_initial_context st.execution_state)
   | Some sentence ->
     ExecutionManager.get_context st.execution_state sentence.id
 

language-server/dm/executionManager.ml

@@ -571,24 +571,30 @@ let rec invalidate schedule id st =
   let deps = Scheduler.dependents schedule id in
   Stateid.Set.fold (invalidate schedule) deps { st with of_sentence }
 
-let get_context st id =
-  match find_fulfilled_opt id st.of_sentence with
-  | None -> log "Cannot find state for get_context"; None
-  | Some (Error _) -> log "Context requested in error state"; None
-  | Some (Success None) -> log "Context requested in a remotely checked state"; None
-  | Some (Success (Some { interp = st })) ->
+let context_of_state st =
     Vernacstate.Interp.unfreeze_interp_state st;
     begin match st.lemmas with
     | None ->
       let env = Global.env () in
       let sigma = Evd.from_env env in
-      Some (sigma, env)
+      sigma, env
     | Some lemmas ->
       let open Declare in
       let open Vernacstate in
-      lemmas |> LemmaStack.with_top ~f:Proof.get_current_context |> Option.make
+      lemmas |> LemmaStack.with_top ~f:Proof.get_current_context
     end
 
+let get_context st id =
+  match find_fulfilled_opt id st.of_sentence with
+  | None -> log "Cannot find state for get_context"; None
+  | Some (Error _) -> log "Context requested in error state"; None
+  | Some (Success None) -> log "Context requested in a remotely checked state"; None
+  | Some (Success (Some { interp = st })) ->
+    Some (context_of_state st)
+
+let get_initial_context st =
+  context_of_state st.initial.Vernacstate.interp
+
 let get_vernac_state st id =
   match find_fulfilled_opt id st.of_sentence with
   | None -> log "Cannot find state for get_context"; None

language-server/dm/executionManager.mli

@@ -52,6 +52,7 @@ val is_executed : state -> sentence_id -> bool
 val is_remotely_executed : state -> sentence_id -> bool
 
 val get_context : state -> sentence_id -> (Evd.evar_map * Environ.env) option
+val get_initial_context : state -> Evd.evar_map * Environ.env
 
 (** Returns the vernac state after the sentence *)
 val get_vernac_state : state -> sentence_id -> Vernacstate.t option

language-server/language/hover.ml

@@ -222,10 +222,19 @@ let ref_info env _sigma ref udecl =
   let impargs = List.map Impargs.binding_kind_of_status impargs in
   let typ = pr_ltype_env env sigma ~impargs typ in
   let path = Libnames.pr_path (Nametab.path_of_global ref) ++ canonical_name_info ref in
-  [md_code_block @@ compactify @@ Pp.string_of_ppcmds typ
-  ; "**Args:** " ^ (Pp.string_of_ppcmds (print_arguments ref))
-  ; Format.sprintf "**%s** %s" (pr_globref_kind ref) (Pp.string_of_ppcmds path)
-  ]
+  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@
+  [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))]
+
+let modtype_info 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))]
 
 let get_hover_contents env sigma ref_or_by_not =
   match ref_or_by_not.CAst.v with
@@ -234,6 +243,19 @@ let get_hover_contents env sigma ref_or_by_not =
       let udecl = None in
       let ref = Nametab.locate qid in
       Some (ref_info env sigma ref udecl)
-    with Not_found -> None
+    with Not_found ->
+    try
+      let kn = Nametab.locate_abbreviation qid in
+      Some (syndef_info kn)
+    with Not_found ->
+    try
+      let mp = Nametab.locate_module qid in
+      Some (mod_info mp)
+    with Not_found ->
+    try
+      let mp = Nametab.locate_modtype qid in
+      Some (modtype_info mp)
+    with Not_found ->
+      None
     end
   | Constrexpr.ByNotation (_ntn,_sc) -> assert false