343 |
343 |
344 fun description strs = |
344 fun description strs = |
345 (case filter_out (fn s => s = "") strs of [] => "" |
345 (case filter_out (fn s => s = "") strs of [] => "" |
346 | strs' => enclose " (" ")" (commas strs')); |
346 | strs' => enclose " (" ")" (commas strs')); |
347 |
347 |
348 fun prt_goal (SOME (ctxt, (i, {statement = ((_, pos), _, _), messages, using, goal, before_qed, after_qed}))) = |
348 fun prt_goal (SOME (ctxt, (i, |
|
349 {statement = ((_, pos), _, _), messages, using, goal, before_qed = _, after_qed = _}))) = |
349 pretty_facts "using " ctxt |
350 pretty_facts "using " ctxt |
350 (if mode <> Backward orelse null using then NONE else SOME using) @ |
351 (if mode <> Backward orelse null using then NONE else SOME using) @ |
351 [Pretty.str ("goal" ^ |
352 [Pretty.str ("goal" ^ |
352 description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @ |
353 description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @ |
353 pretty_goals_local ctxt Markup.subgoal |
354 pretty_goals_local ctxt Markup.subgoal |