diff options
-rw-r--r-- | ide/coq.ml | 6 | ||||
-rw-r--r-- | ide/coq.mli | 2 | ||||
-rw-r--r-- | ide/coqide_ui.ml | 1 | ||||
-rw-r--r-- | ide/ide_slave.ml | 3 | ||||
-rw-r--r-- | ide/wg_ProofView.ml | 35 | ||||
-rw-r--r-- | printing/printer.ml | 139 | ||||
-rw-r--r-- | printing/printer.mli | 21 | ||||
-rw-r--r-- | toplevel/coqtop.ml | 1 |
8 files changed, 147 insertions, 61 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 3a1d87787..cd45e2fcd 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 ab8c12a6f..e8e2f5239 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 91c281c8d..717c4000f 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -85,6 +85,7 @@ let init () = \n <menuitem action='Display existential variable instances' />\ \n <menuitem action='Display universe levels' />\ \n <menuitem action='Display all low-level contents' />\ +\n <menuitem action='Display unfocused goals' />\ \n </menu>\ \n <menu action='Navigation'>\ \n <menuitem action='Forward' />\ diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 966a94da9..56ada9d13 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 f801091cf..60b2d9e60 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 diff --git a/printing/printer.ml b/printing/printer.ml index 93d221f03..3d67e89f5 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -34,6 +34,49 @@ let delayed_emacs_cmd s = let get_current_context () = Pfedit.get_current_context () +let enable_unfocused_goal_printing = ref false +let enable_goal_tags_printing = ref false +let enable_goal_names_printing = ref false + +let should_tag() = !enable_goal_tags_printing +let should_unfoc() = !enable_unfocused_goal_printing +let should_gname() = !enable_goal_names_printing + + +let _ = + let open Goptions in + declare_bool_option + { optsync = true; + optdepr = false; + optname = "printing of unfocused goal"; + optkey = ["Printing";"Unfocused"]; + optread = (fun () -> !enable_unfocused_goal_printing); + optwrite = (fun b -> enable_unfocused_goal_printing:=b) } + +(* This is set on by proofgeneral proof-tree mode. But may be used for + other purposes *) +let _ = + let open Goptions in + declare_bool_option + { optsync = true; + optdepr = false; + optname = "printing of goal tags"; + optkey = ["Printing";"Goal";"Tags"]; + optread = (fun () -> !enable_goal_tags_printing); + optwrite = (fun b -> enable_goal_tags_printing:=b) } + + +let _ = + let open Goptions in + declare_bool_option + { optsync = true; + optdepr = false; + optname = "printing of goal names"; + optkey = ["Printing";"Goal";"Names"]; + optread = (fun () -> !enable_goal_names_printing); + optwrite = (fun b -> enable_goal_names_printing:=b) } + + (**********************************************************************) (** Terms *) @@ -419,23 +462,25 @@ let default_pr_goal gs = (* display a goal tag *) let pr_goal_tag g = let s = " (ID " ^ Goal.uid g ^ ")" in - str (emacs_str s) - -let display_name = false + str s (* display a goal name *) let pr_goal_name sigma g = - if display_name then str " " ++ Pp.surround (pr_existential_key sigma g) + if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g) else mt () +let pr_goal_header nme sigma g = + let (g,sigma) = Goal.V82.nf_evar sigma g in + str "subgoal " ++ nme ++ (if should_tag() then pr_goal_tag g else str"") + ++ (if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g) else mt ()) + (* display the conclusion of a goal *) let pr_concl n sigma g = let (g,sigma) = Goal.V82.nf_evar sigma g in let env = Goal.V82.env sigma g in let pc = pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) in - str (emacs_str "") ++ - str "subgoal " ++ int n ++ pr_goal_tag g ++ pr_goal_name sigma g ++ - str " is:" ++ cut () ++ str" " ++ pc + let header = pr_goal_header (int n) sigma g in + header ++ str " is:" ++ cut () ++ str" " ++ pc (* display evar type: a context and a type *) let pr_evgl_sign sigma evi = @@ -491,8 +536,8 @@ let pr_ne_evar_set hd tl sigma l = let pr_selected_subgoal name sigma g = let pg = default_pr_goal { sigma=sigma ; it=g; } in - v 0 (str "subgoal " ++ name ++ pr_goal_tag g ++ pr_goal_name sigma g - ++ str " is:" ++ cut () ++ pg) + let header = pr_goal_header name sigma g in + v 0 (header ++ str " is:" ++ cut () ++ pg) let default_pr_subgoal n sigma = let rec prrec p = function @@ -585,27 +630,27 @@ let print_dependent_evars gl sigma seeds = end i (str ",") end evars (str "") in - fnl () ++ - str "(dependent evars:" ++ evars ++ str ")" ++ fnl () - else - fnl () ++ - str "(dependent evars: (printing disabled) )" ++ fnl () + cut () ++ cut () ++ + str "(dependent evars:" ++ evars ++ str ")" + else if !Flags.print_emacs then + (* IDEs prefer something dummy instead of nothing *) + cut () ++ cut () ++ str "(dependent evars: (printing disabled) )" + else mt () in - constraints ++ delayed_emacs_cmd evars + constraints ++ evars () (* Print open subgoals. Checks for uninstantiated existential variables *) (* spiwack: [seeds] is for printing dependent evars in emacs mode. *) (* spiwack: [pr_first] is true when the first goal must be singled out and printed in its entirety. *) -(* courtieu: in emacs mode, even less cases where the first goal is printed - in its entirety *) -let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals = +let default_pr_subgoals ?(pr_first=true) + close_cmd sigma seeds shelf stack unfocused goals = (** Printing functions for the extra informations. *) let rec print_stack a = function | [] -> Pp.int a | b::l -> Pp.int a ++ str"-" ++ print_stack b l in - let print_unfocused l = + let print_unfocused_nums l = match l with | [] -> None | a::l -> Some (str"unfocused: " ++ print_stack a l) @@ -625,7 +670,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals | [] -> Pp.mt () | a::l -> Pp.spc () ++ str"(" ++ print_comma_separated_list a l ++ str")" in - let extra = Option.List.flatten [ print_unfocused stack ; print_shelf shelf ] in + let extra = Option.List.flatten [ print_unfocused_nums stack ; print_shelf shelf ] in let print_extra = print_extra_list extra in let focused_if_needed = let needed = not (CList.is_empty extra) && pr_first in @@ -642,8 +687,9 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals in let print_multiple_goals g l = if pr_first then - default_pr_goal { it = g ; sigma = sigma; } ++ fnl () ++ - pr_rec 2 l + default_pr_goal { it = g ; sigma = sigma; } + ++ (if l=[] then str"" else cut ()) + ++ pr_rec 2 l else pr_rec 1 (g::l) in @@ -658,32 +704,27 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals begin let exl = Evarutil.non_instantiated sigma in if Evar.Map.is_empty exl then - (str"No more subgoals." - ++ print_dependent_evars None sigma seeds) + (str"No more subgoals." ++ print_dependent_evars None sigma seeds) else let pei = pr_evars_int sigma 1 exl in - (str "No more subgoals, but there are non-instantiated existential variables:" - ++ fnl () ++ (hov 0 pei) - ++ print_dependent_evars None sigma seeds ++ fnl () ++ - str "You can use Grab Existential Variables.") + v 0 ((str "No more subgoals," + ++ str " but there are non-instantiated existential variables:" + ++ cut () ++ (hov 0 pei) + ++ print_dependent_evars None sigma seeds + ++ cut () ++ str "You can use Grab Existential Variables.")) end - | [g] when not !Flags.print_emacs && pr_first -> - let pg = default_pr_goal { it = g ; sigma = sigma; } in - v 0 ( - str "1" ++ focused_if_needed ++ str"subgoal" ++ print_extra - ++ pr_goal_tag g ++ pr_goal_name sigma g ++ cut () ++ pg - ++ print_dependent_evars (Some g) sigma seeds - ) | g1::rest -> let goals = print_multiple_goals g1 rest in let ngoals = List.length rest+1 in v 0 ( - int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal") ++ - print_extra ++ - str ((if display_name then (fun x -> x) else emacs_str) ", subgoal 1") - ++ pr_goal_tag g1 - ++ pr_goal_name sigma g1 ++ cut () - ++ goals + int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal") + ++ print_extra + ++ str (if (should_gname()) then ", subgoal 1" else "") + ++ (if should_tag() then pr_goal_tag g1 else str"") + ++ pr_goal_name sigma g1 ++ cut () ++ goals + ++ (if unfocused=[] then str "" + else (cut() ++ cut() ++ str "*** Unfocused goals:" ++ cut() + ++ pr_rec (List.length rest + 2) unfocused)) ++ print_dependent_evars (Some g1) sigma seeds ) @@ -692,7 +733,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals type printer_pr = { - pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds; + pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> std_ppcmds; pr_subgoal : int -> evar_map -> goal list -> std_ppcmds; pr_goal : goal sigma -> std_ppcmds; } @@ -726,16 +767,16 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = begin match goals with | [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in begin match bgoals,shelf,given_up with - | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack goals + | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack [] goals | [] , [] , _ -> Feedback.msg_info (str "No more subgoals, but there are some goals you gave up:"); fnl () - ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] given_up + ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] [] given_up ++ fnl () ++ str "You need to go back and solve them." | [] , _ , _ -> Feedback.msg_info (str "All the remaining goals are on the shelf."); fnl () - ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf + ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] [] shelf | _ , _, _ -> let end_cmd = str "This subproof is complete, but there are some unfocused goals." ++ @@ -743,9 +784,13 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = if Pp.ismt s then s else fnl () ++ s) ++ fnl () in - pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] bgoals + pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] [] bgoals end - | _ -> pr_subgoals None sigma seeds shelf stack goals + | _ -> + let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in + let bgoals_focused, bgoals_unfocused = List.partition (fun x -> List.mem x goals) bgoals in + let unfocused_if_needed = if should_unfoc() then bgoals_unfocused else [] in + pr_subgoals ~pr_first:true None bsigma seeds shelf [] unfocused_if_needed bgoals_focused end let pr_nth_open_subgoal n = diff --git a/printing/printer.mli b/printing/printer.mli index 504392e35..c28295054 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -18,6 +18,11 @@ open Glob_term (** These are the entry points for printing terms, context, tac, ... *) + +val enable_unfocused_goal_printing: bool ref +val enable_goal_tags_printing : bool ref +val enable_goal_names_printing : bool ref + (** Terms *) val pr_lconstr_env : env -> evar_map -> constr -> std_ppcmds @@ -135,7 +140,19 @@ val pr_transparent_state : transparent_state -> std_ppcmds (** Proofs *) val pr_goal : goal sigma -> std_ppcmds -val pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds + +(** [pr_subgoals ~pr_first pp sigma seeds shelf focus_stack unfocused goals] + prints the goals of the list [goals] followed by the goals in + [unfocused], in a short way (typically only the conclusion) except + for the first goal if [pr_first] is true. This function can be + replaced by another one by calling [set_printer_pr] (see below), + typically by plugin writers. The default printer prints only the + focused goals unless the conrresponding option + [enable_unfocused_goal_printing] is set. [seeds] is for printing + dependent evars (mainly for emacs proof tree mode). *) +val pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list + -> goal list -> goal list -> std_ppcmds + val pr_subgoal : int -> evar_map -> goal list -> std_ppcmds val pr_concl : int -> evar_map -> goal -> std_ppcmds @@ -190,7 +207,7 @@ val pr_goal_by_id : Id.t -> std_ppcmds val pr_goal_by_uid : string -> std_ppcmds type printer_pr = { - pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds; + pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> std_ppcmds; pr_subgoal : int -> evar_map -> goal list -> std_ppcmds; pr_goal : goal sigma -> std_ppcmds; };; diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c3a755860..5687418f2 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -247,6 +247,7 @@ let set_emacs () = if not (Option.is_empty !toploop) then error "Flag -emacs is incompatible with a custom toplevel loop"; Flags.print_emacs := true; + Printer.enable_goal_tags_printing := true; color := `OFF (** Options for CoqIDE *) |