src/Pure/Isar/proof.ML
changeset 7575 e1e2d07287d8
parent 7556 f3e78ebcf6ba
child 7580 536499cf71af
     1.1 --- a/src/Pure/Isar/proof.ML	Wed Sep 22 20:59:22 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Sep 22 21:02:32 1999 +0200
     1.3 @@ -289,32 +289,35 @@
     1.4  
     1.5  fun print_facts _ None = ()
     1.6    | print_facts s (Some ths) =
     1.7 -      Pretty.writeln (Pretty.big_list (s ^ " facts:") (map pretty_thm ths));
     1.8 +     (Pretty.writeln (Pretty.big_list (s ^ "this:") (map pretty_thm ths)); writeln "");
     1.9  
    1.10  fun print_state nr (state as State (Node {context, facts, mode, goal = _}, nodes)) =
    1.11    let
    1.12      val ref (_, _, begin_goal) = Goals.current_goals_markers;
    1.13  
    1.14      fun levels_up 0 = ""
    1.15 -      | levels_up 1 = " (1 level up)"
    1.16 -      | levels_up i = " (" ^ string_of_int i ^ " levels up)";
    1.17 +      | levels_up 1 = ", 1 level up"
    1.18 +      | levels_up i = ", " ^ string_of_int i ^ " levels up";
    1.19  
    1.20      fun print_goal (_, (i, (((kind, name, _), (goal_facts, thm)), _))) =
    1.21 -      (print_facts "Using"
    1.22 +      (print_facts "using "
    1.23            (if mode <> Backward orelse null goal_facts then None else Some goal_facts);
    1.24 -        writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 2) ^ ":");
    1.25 +        writeln ("goal (" ^ kind_name kind ^ (if name = "" then "" else " " ^ name) ^
    1.26 +          levels_up (i div 2) ^ "):");
    1.27          Locale.print_goals_marker begin_goal (! goals_limit) thm);
    1.28  
    1.29 -    val ctxt_strings = ProofContext.strings_of_context context;
    1.30 +    val ctxt_strings =
    1.31 +      if ! verbose orelse mode = Forward then ProofContext.strings_of_context context
    1.32 +      else if mode = Backward then ProofContext.strings_of_prems context
    1.33 +      else [];
    1.34    in
    1.35      writeln ("Proof(" ^ mode_name mode ^ "): step " ^ string_of_int nr ^
    1.36        ", depth " ^ string_of_int (length nodes div 2));
    1.37      writeln "";
    1.38 +    if null ctxt_strings then () else (seq writeln ctxt_strings; writeln "");
    1.39      if ! verbose orelse mode = Forward then
    1.40 -      (if null ctxt_strings then () else (seq writeln ctxt_strings; writeln "");
    1.41 -        print_facts "Current" facts;
    1.42 -        print_goal (find_goal 0 state))
    1.43 -    else if mode = ForwardChain then print_facts "Picking" facts
    1.44 +      (print_facts "" facts; print_goal (find_goal 0 state))
    1.45 +    else if mode = ForwardChain then print_facts "picking " facts
    1.46      else print_goal (find_goal 0 state)
    1.47    end;
    1.48