From 1fe73e6af81759fa8b78c8660745492ed886d477 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Wed, 26 Apr 2017 11:57:58 +0200 Subject: Adding an option "Printing Unfocused". Off by default. + small refactoring of emacs hacks in printer.ml. --- ide/coq.ml | 6 +++++- ide/coq.mli | 2 ++ ide/coqide_ui.ml | 1 + ide/ide_slave.ml | 3 ++- ide/wg_ProofView.ml | 35 +++++++++++++++++++++++++---------- 5 files changed, 35 insertions(+), 12 deletions(-) (limited to 'ide') diff --git a/ide/coq.ml b/ide/coq.ml index 3a1d877872..cd45e2fcdc 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -519,6 +519,7 @@ struct let all_basic = ["Printing"; "All"] let existential = ["Printing"; "Existential"; "Instances"] let universes = ["Printing"; "Universes"] + let unfocused = ["Printing"; "Unfocused"] type bool_descr = { opts : t list; init : bool; label : string } @@ -534,7 +535,8 @@ struct label = "Display _existential variable instances" }; { opts = [universes]; init = false; label = "Display _universe levels" }; { opts = [all_basic;existential;universes]; init = false; - label = "Display all _low-level contents" } + label = "Display all _low-level contents" }; + { opts = [unfocused]; init = false; label = "Display _unfocused goals" } ] (** The current status of the boolean options *) @@ -549,6 +551,8 @@ struct let _ = reset () + let printing_unfocused () = Hashtbl.find current_state unfocused + (** Transmitting options to coqtop *) let enforce h k = diff --git a/ide/coq.mli b/ide/coq.mli index ab8c12a6f1..e8e2f5239e 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -140,6 +140,8 @@ sig val set : t -> bool -> unit + val printing_unfocused: unit -> bool + (** [enforce] transmits to coq the current option values. It is also called by [goals] and [evars] above. *) diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index 91c281c8d8..717c4000f5 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -85,6 +85,7 @@ let init () = \n \ \n \ \n \ +\n \ \n \ \n \ \n \ diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 966a94da91..56ada9d132 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -54,7 +54,8 @@ let coqide_known_option table = List.mem table [ ["Printing";"All"]; ["Printing";"Records"]; ["Printing";"Existential";"Instances"]; - ["Printing";"Universes"]] + ["Printing";"Universes"]; + ["Printing";"Unfocused"]] let is_known_option cmd = match cmd with | VernacSetOption (o,BoolValue true) diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index f801091cfc..60b2d9e60d 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -47,7 +47,7 @@ let hook_tag_cb tag menu_content sel_cb hover_cb = hover_cb start stop; false | _ -> false)) -let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with +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 -> let on_hover sel_start sel_stop = @@ -65,8 +65,11 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with let head_str = Printf.sprintf "%d subgoal%s\n" goals_cnt (if 1 < goals_cnt then "s" else "") in - let goal_str index total = Printf.sprintf - "______________________________________(%d/%d)\n" index total + let goal_str shownum index total = + if shownum then Printf.sprintf + "______________________________________(%d/%d)\n" index total + else Printf.sprintf + "______________________________________\n" in (* Insert current goal and its hypotheses *) let hyps_hints, goal_hints = match hints with @@ -97,18 +100,29 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with [tag] else [] in - proof#buffer#insert (goal_str 1 goals_cnt); + proof#buffer#insert (goal_str true 1 goals_cnt); insert_xml proof#buffer (Richpp.richpp_of_pp width cur_goal); proof#buffer#insert "\n" in (* Insert remaining goals (no hypotheses) *) - let fold_goal i _ { Interface.goal_ccl = g } = - proof#buffer#insert (goal_str i goals_cnt); + let fold_goal shownum i _ { Interface.goal_ccl = g } = + proof#buffer#insert (goal_str shownum i goals_cnt); insert_xml proof#buffer (Richpp.richpp_of_pp width g); proof#buffer#insert "\n" in - let () = Util.List.fold_left_i fold_goal 2 () rem_goals in - + let () = Util.List.fold_left_i (fold_goal true) 2 () rem_goals in + (* show unfocused goal if option set *) + (* Insert remaining goals (no hypotheses) *) + if Coq.PrintOpt.printing_unfocused () then + begin + ignore(proof#buffer#place_cursor ~where:(proof#buffer#end_iter)); + let unfoc = List.flatten (List.rev (List.map (fun (x,y) -> x@y) unfoc_goals)) in + if unfoc<>[] then + begin + proof#buffer#insert "\nUnfocused Goals:\n"; + Util.List.fold_left_i (fold_goal false) 0 () unfoc + end + end; ignore(proof#buffer#place_cursor ~where:(proof#buffer#end_iter#backward_to_tag_toggle (Some Tags.Proof.goal))); @@ -172,8 +186,9 @@ let display mode (view : #GText.view_skel) goals hints evars = in List.iteri iter bg end - | Some { Interface.fg_goals = fg } -> - mode view fg hints + | Some { Interface.fg_goals = fg; bg_goals = bg } -> + mode view fg bg hints + let proof_view () = let buffer = GSourceView2.source_buffer -- cgit v1.2.3 From 8bcf71360261d789ac3ab919bc49309df678628f Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Tue, 2 May 2017 21:32:26 +0200 Subject: labelizing arguments --- ide/wg_ProofView.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'ide') diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index 60b2d9e60d..0bf5afbfdb 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -47,7 +47,7 @@ let hook_tag_cb tag menu_content sel_cb hover_cb = hover_cb start stop; false | _ -> false)) -let mode_tactic sel_cb (proof : #GText.view_skel) goals unfoc_goals hints = match goals with +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 -> let on_hover sel_start sel_stop = @@ -65,7 +65,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals unfoc_goals hints = matc let head_str = Printf.sprintf "%d subgoal%s\n" goals_cnt (if 1 < goals_cnt then "s" else "") in - let goal_str shownum index total = + let goal_str ?(shownum=false) index total = if shownum then Printf.sprintf "______________________________________(%d/%d)\n" index total else Printf.sprintf @@ -100,17 +100,17 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals unfoc_goals hints = matc [tag] else [] in - proof#buffer#insert (goal_str true 1 goals_cnt); + proof#buffer#insert (goal_str ~shownum:true 1 goals_cnt); insert_xml proof#buffer (Richpp.richpp_of_pp width cur_goal); proof#buffer#insert "\n" in (* Insert remaining goals (no hypotheses) *) - let fold_goal shownum i _ { Interface.goal_ccl = g } = - proof#buffer#insert (goal_str shownum i goals_cnt); + let fold_goal ?(shownum=false) i _ { Interface.goal_ccl = g } = + proof#buffer#insert (goal_str ~shownum i goals_cnt); insert_xml proof#buffer (Richpp.richpp_of_pp width g); proof#buffer#insert "\n" in - let () = Util.List.fold_left_i (fold_goal true) 2 () rem_goals in + let () = Util.List.fold_left_i (fold_goal ~shownum:true) 2 () rem_goals in (* show unfocused goal if option set *) (* Insert remaining goals (no hypotheses) *) if Coq.PrintOpt.printing_unfocused () then @@ -120,7 +120,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals unfoc_goals hints = matc if unfoc<>[] then begin proof#buffer#insert "\nUnfocused Goals:\n"; - Util.List.fold_left_i (fold_goal false) 0 () unfoc + Util.List.fold_left_i (fold_goal ~shownum:false) 0 () unfoc end end; ignore(proof#buffer#place_cursor @@ -187,7 +187,7 @@ let display mode (view : #GText.view_skel) goals hints evars = List.iteri iter bg end | Some { Interface.fg_goals = fg; bg_goals = bg } -> - mode view fg bg hints + mode view fg ~unfoc_goals:bg hints let proof_view () = -- cgit v1.2.3