src/Pure/Isar/proof.ML
changeset 6529 0f4c2ebc5018
parent 6404 2daaf2943c79
child 6683 b7293047b0f4
     1.1 --- a/src/Pure/Isar/proof.ML	Tue Apr 27 15:13:18 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Tue Apr 27 15:13:35 1999 +0200
     1.3 @@ -28,6 +28,7 @@
     1.4    val reset_facts: state -> state
     1.5    val assert_backward: state -> state
     1.6    val enter_forward: state -> state
     1.7 +  val verbose: bool ref
     1.8    val print_state: state -> unit
     1.9    type method
    1.10    val method: (thm list -> thm ->
    1.11 @@ -59,7 +60,7 @@
    1.12    val at_bottom: state -> bool
    1.13    val local_qed: (state -> state Seq.seq) -> state -> state Seq.seq
    1.14    val global_qed: (state -> state Seq.seq) -> bstring option
    1.15 -    -> theory attribute list option -> state -> theory * (string * string * thm)
    1.16 +    -> theory attribute list option -> state -> theory * {kind: string, name: string, thm: thm}
    1.17  end;
    1.18  
    1.19  signature PROOF_PRIVATE =
    1.20 @@ -265,6 +266,8 @@
    1.21  
    1.22  (** print_state **)
    1.23  
    1.24 +val verbose = ProofContext.verbose;
    1.25 +
    1.26  fun print_state (state as State ({context, facts, mode, goal = _}, nodes)) =
    1.27    let
    1.28      val ref (_, _, begin_goal) = Goals.current_goals_markers;
    1.29 @@ -282,12 +285,15 @@
    1.30    in
    1.31      writeln ("Nesting level: " ^ string_of_int (length nodes div 2));
    1.32      writeln "";
    1.33 -    writeln (mode_name mode ^ " mode");
    1.34 +    writeln (enclose "`" "'" (mode_name mode) ^ " mode");
    1.35      writeln "";
    1.36 -    ProofContext.print_context context;
    1.37 -    writeln "";
    1.38 -    print_facts facts;
    1.39 -    print_goal (find_goal 0 state)
    1.40 +    if ! verbose orelse mode = Forward then
    1.41 +      (ProofContext.print_context context;
    1.42 +        writeln "";
    1.43 +        print_facts facts;
    1.44 +        print_goal (find_goal 0 state))
    1.45 +    else if mode = ForwardChain then print_facts facts
    1.46 +    else print_goal (find_goal 0 state)
    1.47    end;
    1.48  
    1.49  
    1.50 @@ -639,7 +645,7 @@
    1.51        | _ => raise STATE ("No global goal!", state));
    1.52  
    1.53      val (thy', result') = PureThy.store_thm ((name, result), atts) (theory_of state);
    1.54 -  in (thy', (kind_name kind, name, result')) end;
    1.55 +  in (thy', {kind = kind_name kind, name = name, thm = result'}) end;
    1.56  
    1.57  fun global_qed finalize alt_name alt_atts state =
    1.58    state