# HG changeset patch # User wenzelm # Date 1350388922 -7200 # Node ID 9a0fe50e4534532f5993a10a28f444151f54f88f # Parent 52da6a736c320251c1d47a950732863b0e044d6f further attempts to unify/simplify goal output; diff -r 52da6a736c32 -r 9a0fe50e4534 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Tue Oct 16 13:06:40 2012 +0200 +++ b/src/Pure/Isar/proof.ML Tue Oct 16 14:02:02 2012 +0200 @@ -333,32 +333,20 @@ fun pretty_facts _ _ NONE = [] | pretty_facts s ctxt (SOME ths) = - [Pretty.big_list (s ^ "this:") (map (Display.pretty_thm ctxt) ths), Pretty.str ""]; + [Pretty.chunks + (Pretty.block [Pretty.command s, Pretty.brk 1, Pretty.str "this:"] :: + map (Display.pretty_thm ctxt) ths), Pretty.str ""]; fun pretty_state nr state = let val {context = ctxt, facts, mode, goal = _} = top state; val verbose = Config.get ctxt Proof_Context.verbose; - fun levels_up 0 = "" - | levels_up 1 = "1 level up" - | levels_up i = string_of_int i ^ " levels up"; - - fun subgoals 0 = "" - | subgoals 1 = "1 subgoal" - | subgoals n = string_of_int n ^ " subgoals"; - - fun description strs = - (case filter_out (fn s => s = "") strs of [] => "" - | strs' => enclose " (" ")" (commas strs')); - - fun prt_goal (SOME (_, (i, + fun prt_goal (SOME (_, (_, {statement = ((_, pos), _, _), messages, using, goal, before_qed = _, after_qed = _}))) = pretty_facts "using " ctxt (if mode <> Backward orelse null using then NONE else SOME using) @ - [Pretty.str ("goal" ^ - description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @ - Goal_Display.pretty_goals ctxt goal @ + [Proof_Display.pretty_goal_header goal] @ Goal_Display.pretty_goals ctxt goal @ (map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages)) | prt_goal NONE = []; @@ -487,8 +475,7 @@ val string_of_term = Syntax.string_of_term ctxt; val string_of_thm = Display.string_of_thm ctxt; - val _ = Thm.no_prems goal orelse - error (Pretty.string_of (Goal_Display.pretty_goal {main = true, limit = false} ctxt goal)); + val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal); val extra_hyps = Assumption.extra_hyps ctxt goal; val _ = null extra_hyps orelse @@ -519,10 +506,7 @@ fun finished_goal state = let val (ctxt, (_, goal)) = get_goal state in if Thm.no_prems goal then Seq.Result state - else - Seq.Error (fn () => - finished_goal_error ^ ":\n" ^ - Pretty.string_of (Goal_Display.pretty_goal {main = true, limit = false} ctxt goal)) + else Seq.Error (fn () => finished_goal_error ^ ":\n" ^ Proof_Display.string_of_goal ctxt goal) end; @@ -980,29 +964,14 @@ (* concluding steps *) -fun method_error name state = Seq.Error (fn () => - let - val (ctxt, (facts, goal)) = get_goal state; - val pr_header = - "Failure of " ^ (if name = "" then "" else name ^ " ") ^ "proof method on goal state:\n"; - val pr_facts = - if null facts then "" - else Pretty.string_of (Pretty.big_list "facts:" (map (Display.pretty_thm ctxt) facts)) ^ "\n"; - val pr_goal = - "goal:\n" ^ Pretty.string_of (Goal_Display.pretty_goal {main = false, limit = false} ctxt goal); - in pr_header ^ pr_facts ^ pr_goal end); - -local - +fun method_error name state = Seq.single (Proof_Display.method_error name (raw_goal state)); val op APPEND = Seq.APPEND; fun terminal_proof qeds initial terminal = - ((proof (SOME initial) #> Seq.map Seq.Result) APPEND (Seq.single o method_error "initial")) - #> Seq.maps_results (qeds terminal APPEND (Seq.single o method_error "terminal")) + ((proof (SOME initial) #> Seq.map Seq.Result) APPEND method_error "initial") + #> Seq.maps_results (qeds terminal APPEND method_error "terminal") #> Seq.the_result ""; -in - fun local_terminal_proof (text, opt_text) = terminal_proof local_qeds text (opt_text, true); val local_default_proof = local_terminal_proof (Method.default_text, NONE); val local_immediate_proof = local_terminal_proof (Method.this_text, NONE); @@ -1015,8 +984,6 @@ fun global_skip_proof int = global_terminal_proof (Method.sorry_text int, NONE); val global_done_proof = terminal_proof global_qeds Method.done_text (NONE, false); -end; - (* common goal statements *) diff -r 52da6a736c32 -r 9a0fe50e4534 src/Pure/Isar/proof_display.ML --- a/src/Pure/Isar/proof_display.ML Tue Oct 16 13:06:40 2012 +0200 +++ b/src/Pure/Isar/proof_display.ML Tue Oct 16 14:02:02 2012 +0200 @@ -17,6 +17,9 @@ val pretty_full_theory: bool -> theory -> Pretty.T val print_theory: theory -> unit val string_of_rule: Proof.context -> string -> thm -> string + val pretty_goal_header: thm -> Pretty.T + val string_of_goal: Proof.context -> thm -> string + val method_error: string -> {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result val print_results: Markup.T -> bool -> Proof.context -> ((string * string) * (string * thm list) list) -> unit val print_consts: bool -> Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit @@ -86,6 +89,42 @@ val string_of_rule = Pretty.string_of ooo pretty_rule; +(* goals *) + +local + +fun subgoals 0 = [] + | subgoals 1 = [Pretty.brk 1, Pretty.str "(1 subgoal)"] + | subgoals n = [Pretty.brk 1, Pretty.str ("(" ^ string_of_int n ^ " subgoals)")]; + +in + +fun pretty_goal_header goal = + Pretty.block ([Pretty.command "goal"] @ subgoals (Thm.nprems_of goal) @ [Pretty.str ":"]); + +end; + +fun string_of_goal ctxt goal = + Pretty.string_of (Pretty.chunks + [pretty_goal_header goal, Goal_Display.pretty_goal {main = true, limit = false} ctxt goal]); + + +(* method_error *) + +fun method_error name {context = ctxt, facts, goal} = Seq.Error (fn () => + let + val pr_header = "Failure of " ^ (if name = "" then "" else name ^ " ") ^ "proof method:\n"; + val pr_facts = + if null facts then "" + else + Pretty.string_of + (Pretty.chunks + (Pretty.block [Pretty.command "using", Pretty.brk 1, Pretty.str "this:"] :: + map (Display.pretty_thm ctxt) facts)) ^ "\n"; + val pr_goal = string_of_goal ctxt goal; + in pr_header ^ pr_facts ^ pr_goal end); + + (* results *) local