From c3dcb5ac72bd33ffa24e0fa64ff3293135267fdd Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 4 Oct 2020 23:03:37 +0200 Subject: Adding support for printing goal names in CoqIDE. Co-authored-by: Théo Zimmermann Co-authored-by: Pierre-Marie Pédrot --- ide/coqide/coq.ml | 4 +++- ide/coqide/coqide_ui.ml | 1 + ide/coqide/idetop.ml | 4 ++-- ide/coqide/wg_ProofView.ml | 28 ++++++++++++++++------------ 4 files changed, 22 insertions(+), 15 deletions(-) (limited to 'ide') 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 \ \n \ \n \ +\n \ \n \ \n \ \n \ 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 -- cgit v1.2.3