Adding support for printing goal names in CoqIDE.

Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
Co-authored-by: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>

4 files changed, 22 insertions, 15 deletions

diff --git a/ide/coqide/coq.ml b/ide/coqide/coq.ml
index 1167b8199e..b8228df2aa 100644
--- a/ide/coqide/coq.ml
+++ b/ide/coqide/coq.ml
@@ -550,6 +550,7 @@ struct
   let existential = BoolOpt ["Printing"; "Existential"; "Instances"]
   let universes = BoolOpt ["Printing"; "Universes"]
   let unfocused = BoolOpt ["Printing"; "Unfocused"]
+  let goal_names = BoolOpt ["Printing"; "Goal"; "Names"]
   let diff = StringOpt ["Diffs"]
 
   type 'a descr = { opts : 'a t list; init : 'a; label : string }
@@ -568,7 +569,8 @@ struct
     { opts = [universes]; init = false; label = "Display _universe levels" };
     { opts = [all_basic;existential;universes]; init = false;
       label = "Display all _low-level contents" };
-    { opts = [unfocused]; init = false; label = "Display _unfocused goals" }
+    { opts = [unfocused]; init = false; label = "Display _unfocused goals" };
+    { opts = [goal_names]; init = false; label = "Display _goal names" }
   ]
 
   let diff_item = { opts = [diff]; init = "off"; label = "Display _proof diffs" }
diff --git a/ide/coqide/coqide_ui.ml b/ide/coqide/coqide_ui.ml
index 6540fc6fca..badfabf07e 100644
--- a/ide/coqide/coqide_ui.ml
+++ b/ide/coqide/coqide_ui.ml
@@ -85,6 +85,7 @@ let init () =
 \n    <menuitem action='Display universe levels' />\
 \n    <menuitem action='Display all low-level contents' />\
 \n    <menuitem action='Display unfocused goals' />\
+\n    <menuitem action='Display goal names' />\
 \n    <separator/>\
 \n    <menuitem action='Unset diff' />\
 \n    <menuitem action='Set diff' />\
diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml
index ddfa3a80bd..602acefa7c 100644
--- a/ide/coqide/idetop.ml
+++ b/ide/coqide/idetop.ml
@@ -195,7 +195,7 @@ let concl_next_tac =
 let process_goal sigma g =
   let env = Goal.V82.env sigma g in
   let min_env = Environ.reset_context env in
-  let id = Goal.uid g in
+  let id = if Printer.print_goal_names () then Names.Id.to_string (Termops.evar_suggested_name g sigma) else "" in
   let ccl =
     pr_letype_env ~goal_concl_style:true env sigma (Goal.V82.concl sigma g)
   in
@@ -206,7 +206,7 @@ let process_goal sigma g =
   let (_env, hyps) =
     Context.Compacted.fold process_hyp
       (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in
-  { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }
+  { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id }
 
 let process_goal_diffs diff_goal_map oldp nsigma ng =
   let open Evd in
diff --git a/ide/coqide/wg_ProofView.ml b/ide/coqide/wg_ProofView.ml
index 1de63953af..8e451c9917 100644
--- a/ide/coqide/wg_ProofView.ml
+++ b/ide/coqide/wg_ProofView.ml
@@ -52,7 +52,7 @@ let hook_tag_cb tag menu_content sel_cb hover_cb =
 
 let mode_tactic sel_cb (proof : #GText.view_skel) goals ~unfoc_goals hints = match goals with
   | [] -> assert false
-  | { Interface.goal_hyp = hyps; Interface.goal_ccl = cur_goal; } :: rem_goals ->
+  | { Interface.goal_hyp = hyps; Interface.goal_ccl = cur_goal; Interface.goal_id = cur_id } :: rem_goals ->
       let on_hover sel_start sel_stop =
         proof#buffer#remove_tag
           ~start:proof#buffer#start_iter
@@ -68,11 +68,11 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals ~unfoc_goals hints = mat
       let head_str = Printf.sprintf
         "%d subgoal%s\n" goals_cnt (if 1 < goals_cnt then "s" else "")
       in
-      let goal_str ?(shownum=false) index total =
-        if shownum then Printf.sprintf
-                          "______________________________________(%d/%d)\n" index total
-        else Printf.sprintf
-               "______________________________________\n"
+      let goal_str ?(shownum=false) index total id =
+        let annot =
+          if CString.is_empty id then if shownum then Printf.sprintf "(%d/%d)" index total else ""
+          else Printf.sprintf "(?%s)" id in
+        Printf.sprintf "______________________________________%s\n" annot
       in
       (* Insert current goal and its hypotheses *)
       let hyps_hints, goal_hints = match hints with
@@ -103,13 +103,13 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals ~unfoc_goals hints = mat
           [tag]
           else []
         in
-        proof#buffer#insert (goal_str ~shownum:true 1 goals_cnt);
+        proof#buffer#insert (goal_str ~shownum:true 1 goals_cnt cur_id);
         insert_xml ~tags:[Tags.Proof.goal] proof#buffer (Richpp.richpp_of_pp width cur_goal);
         proof#buffer#insert "\n"
       in
       (* Insert remaining goals (no hypotheses) *)
-      let fold_goal ?(shownum=false) i _ { Interface.goal_ccl = g } =
-        proof#buffer#insert (goal_str ~shownum i goals_cnt);
+      let fold_goal ?(shownum=false) i _ { Interface.goal_ccl = g; Interface.goal_id = id } =
+        proof#buffer#insert (goal_str ~shownum i goals_cnt id);
         insert_xml proof#buffer (Richpp.richpp_of_pp width g);
         proof#buffer#insert "\n"
       in
@@ -178,12 +178,16 @@ let display mode (view : #GText.view_skel) goals hints evars =
     | _, _, _, _ ->
       (* No foreground proofs, but still unfocused ones *)
       let total = List.length bg in
-      let goal_str index = Printf.sprintf
-        "______________________________________(%d/%d)\n" index total
+      let goal_str index id =
+        let annot =
+          if CString.is_empty id then Printf.sprintf "(%d/%d)" index total
+          else Printf.sprintf "(?%s)" id in
+        Printf.sprintf
+               "______________________________________%s\n" annot
       in
       view#buffer#insert "This subproof is complete, but there are some unfocused goals:\n\n";
       let iter i goal =
-        let () = view#buffer#insert (goal_str (succ i)) in
+        let () = view#buffer#insert (goal_str (succ i) goal.Interface.goal_id) in
         insert_xml view#buffer (Richpp.richpp_of_pp width goal.Interface.goal_ccl);
         view#buffer#insert "\n"
       in