src/Pure/Isar/proof.ML
changeset 8462 7f4e4e875c13
parent 8450 dc44d6533f0f
child 8494 21074180a6f2
     1.1 --- a/src/Pure/Isar/proof.ML	Wed Mar 15 18:25:42 2000 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Mar 15 18:26:53 2000 +0100
     1.3 @@ -304,9 +304,9 @@
     1.4  
     1.5  val verbose = ProofContext.verbose;
     1.6  
     1.7 -fun print_facts _ None = ()
     1.8 -  | print_facts s (Some ths) =
     1.9 -     (Pretty.writeln (Pretty.big_list (s ^ "this:") (map pretty_thm ths)); writeln "");
    1.10 +fun pretty_facts _ None = []
    1.11 +  | pretty_facts s (Some ths) =
    1.12 +      [Pretty.big_list (s ^ "this:") (map pretty_thm ths), Pretty.str ""];
    1.13  
    1.14  fun print_state nr (state as State (Node {context, facts, mode, goal = _}, nodes)) =
    1.15    let
    1.16 @@ -316,27 +316,27 @@
    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 -          (if mode <> Backward orelse null goal_facts then None else Some goal_facts);
    1.23 -        writeln ("goal (" ^ kind_name kind ^ (if name = "" then "" else " " ^ name) ^
    1.24 -          levels_up (i div 2) ^ "):");
    1.25 -        Locale.print_goals_marker begin_goal (! goals_limit) thm);
    1.26 +    fun pretty_goal (_, (i, (((kind, name, _), (goal_facts, thm)), _))) =
    1.27 +      pretty_facts "using "
    1.28 +        (if mode <> Backward orelse null goal_facts then None else Some goal_facts) @
    1.29 +      [Pretty.str ("goal (" ^ kind_name kind ^ (if name = "" then "" else " " ^ name) ^
    1.30 +        levels_up (i div 2) ^ "):")] @
    1.31 +      Locale.pretty_goals_marker begin_goal (! goals_limit) thm;
    1.32  
    1.33 -    val ctxt_strings =
    1.34 -      if ! verbose orelse mode = Forward then ProofContext.strings_of_context context
    1.35 -      else if mode = Backward then ProofContext.strings_of_prems context
    1.36 +    val ctxt_prts =
    1.37 +      if ! verbose orelse mode = Forward then ProofContext.pretty_context context
    1.38 +      else if mode = Backward then ProofContext.pretty_prems context
    1.39        else [];
    1.40 -  in
    1.41 -    writeln ("Proof(" ^ mode_name mode ^ "): step " ^ string_of_int nr ^
    1.42 -      ", depth " ^ string_of_int (length nodes div 2));
    1.43 -    writeln "";
    1.44 -    if null ctxt_strings then () else (seq writeln ctxt_strings; writeln "");
    1.45 -    if ! verbose orelse mode = Forward then
    1.46 -      (print_facts "" facts; print_goal (find_goal 0 state))
    1.47 -    else if mode = ForwardChain then print_facts "picking " facts
    1.48 -    else print_goal (find_goal 0 state)
    1.49 -  end;
    1.50 +
    1.51 +    val prts =
    1.52 +     [Pretty.str ("Proof(" ^ mode_name mode ^ "): step " ^ string_of_int nr ^
    1.53 +        ", depth " ^ string_of_int (length nodes div 2)), Pretty.str ""] @
    1.54 +     (if null ctxt_prts then [] else ctxt_prts @ [Pretty.str ""]) @
    1.55 +     (if ! verbose orelse mode = Forward then
    1.56 +       (pretty_facts "" facts @ pretty_goal (find_goal 0 state))
    1.57 +      else if mode = ForwardChain then pretty_facts "picking " facts
    1.58 +      else pretty_goal (find_goal 0 state))
    1.59 +  in Pretty.writeln (Pretty.chunks prts) end;
    1.60  
    1.61  
    1.62