From 82abccdc576e3eff3adb617e90fc9c4ececae329 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Thu, 19 Mar 2015 13:38:58 +0100 Subject: Generalisation of the "end command" argument of the goal printer. This is meant to help integrate the printers of the declarative mode. --- printing/printer.ml | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) (limited to 'printing/printer.ml') 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; } -- cgit v1.2.3 From 721e4b7bf963fa6541ecf66bb3643f7388dca896 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Tue, 24 Mar 2015 15:52:15 +0100 Subject: Better formatting of messages in proofs. --- printing/printer.ml | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) (limited to 'printing/printer.ml') diff --git a/printing/printer.ml b/printing/printer.ml index 3ef009e1b5..467395c92c 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -630,10 +630,15 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf | _ , _, _ -> - msg_info (str "This subproof is complete, but there are still unfocused goals." ++ - (match Proof_global.Bullet.suggest p - with None -> str"" | Some s -> fnl () ++ str s)); - fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds shelf [] bgoals + let end_cmd = + strbrk "This subproof is complete, but there are still \ + unfocused goals." ++ + (match Proof_global.Bullet.suggest p + with None -> str"" | Some s -> fnl () ++ str s) ++ + fnl () + in + msg_info end_cmd; + pr_subgoals ~pr_first:false None bsigma seeds shelf [] bgoals end | _ -> pr_subgoals None sigma seeds shelf stack goals end -- cgit v1.2.3 From a615382472ee21e288bd7115be147415e465e897 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Mon, 16 Mar 2015 17:56:48 +0100 Subject: Declarative mode: plug the specialised printers back. It will not work in CoqIDE though, which handles printing its own way. It's a general remark that we have many ways of printing things in Coq and we should look for a unified structured framework to be shared between interfaces. --- printing/printer.ml | 32 +++++++++++++++++--------------- 1 file changed, 17 insertions(+), 15 deletions(-) (limited to 'printing/printer.ml') diff --git a/printing/printer.ml b/printing/printer.ml index 467395c92c..0d3a1c17e4 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -544,22 +544,25 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals else pr_rec 1 (g::l) in + (* Side effect! This has to be made more robust *) + let () = + match close_cmd with + | Some cmd -> msg_info cmd + | None -> () + in match goals with | [] -> begin - match close_cmd with - Some cmd -> cmd - | None -> - let exl = Evarutil.non_instantiated sigma in - if Evar.Map.is_empty exl then - (str"No more subgoals." - ++ emacs_print_dependent_evars sigma seeds) - else - let pei = pr_evars_int sigma 1 exl in - (str "No more subgoals but non-instantiated existential " ++ - str "variables:" ++ fnl () ++ (hov 0 pei) - ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++ - str "You can use Grab Existential Variables.") + let exl = Evarutil.non_instantiated sigma in + if Evar.Map.is_empty exl then + (str"No more subgoals." + ++ emacs_print_dependent_evars sigma seeds) + else + let pei = pr_evars_int sigma 1 exl in + (str "No more subgoals but non-instantiated existential " ++ + str "variables:" ++ fnl () ++ (hov 0 pei) + ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++ + 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 @@ -637,8 +640,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = with None -> str"" | Some s -> fnl () ++ str s) ++ fnl () in - msg_info end_cmd; - pr_subgoals ~pr_first:false None 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 end -- cgit v1.2.3