diff options
| author | Arnaud Spiwack | 2015-03-19 13:38:58 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-03-31 11:28:18 +0200 |
| commit | 82abccdc576e3eff3adb617e90fc9c4ececae329 (patch) | |
| tree | 4001a39072740a5be5b24533c05c1fe449906469 | |
| parent | 829238f2fe74c782023989e1871e15411b3e4ada (diff) | |
Generalisation of the "end command" argument of the goal printer.
This is meant to help integrate the printers of the declarative mode.
| -rw-r--r-- | printing/printer.ml | 11 | ||||
| -rw-r--r-- | printing/printer.mli | 4 |
2 files changed, 7 insertions, 8 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index fb98f6073c..3ef009e1b5 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -548,9 +548,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals | [] -> begin match close_cmd with - Some cmd -> - (str "Subproof completed, now type " ++ str cmd ++ - str ".") + Some cmd -> cmd | None -> let exl = Evarutil.non_instantiated sigma in if Evar.Map.is_empty exl then @@ -563,7 +561,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++ str "You can use Grab Existential Variables.") end - | [g] when not !Flags.print_emacs -> + | [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 @@ -572,8 +570,9 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals ) | g1::rest -> let goals = print_multiple_goals g1 rest in + let ngoals = List.length rest+1 in v 0 ( - int(List.length rest+1) ++ focused_if_needed ++ str"subgoals" ++ + 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 @@ -587,7 +586,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals type printer_pr = { - pr_subgoals : ?pr_first:bool -> string 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 -> std_ppcmds; pr_subgoal : int -> evar_map -> goal list -> std_ppcmds; pr_goal : goal sigma -> std_ppcmds; } diff --git a/printing/printer.mli b/printing/printer.mli index 42ed2b6d9e..a469a8dbed 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -128,7 +128,7 @@ val pr_transparent_state : transparent_state -> std_ppcmds (** Proofs *) val pr_goal : goal sigma -> std_ppcmds -val pr_subgoals : ?pr_first:bool -> string option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds +val pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds val pr_subgoal : int -> evar_map -> goal list -> std_ppcmds val pr_concl : int -> evar_map -> goal -> std_ppcmds @@ -168,7 +168,7 @@ val pr_assumptionset : val pr_goal_by_id : string -> std_ppcmds type printer_pr = { - pr_subgoals : ?pr_first:bool -> string 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 -> std_ppcmds; pr_subgoal : int -> evar_map -> goal list -> std_ppcmds; pr_goal : goal sigma -> std_ppcmds; };; |