# HG changeset patch
# User wenzelm
# Date 1121263657 -7200
# Node ID 13d20ed9086cbdc545799830e7644d5e7fd47d51
# Parent  b829a6c9a87addb3d5a5a5412885709941285fac
added print_state_hook;
renamed proof'' to actual_proof;
tuned;

diff -r b829a6c9a87a -r 13d20ed9086c src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Jul 13 16:07:36 2005 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Jul 13 16:07:37 2005 +0200
@@ -7,17 +7,11 @@
 
 signature TOPLEVEL =
 sig
-  datatype node = Theory of theory | Proof of ProofHistory.T | SkipProof of int History.T * theory
+  datatype node =
+    Theory of theory | Proof of ProofHistory.T | SkipProof of int History.T * theory
   type state
   val toplevel: state
   val is_toplevel: state -> bool
-  val prompt_state_default: state -> string
-  val prompt_state_fn: (state -> string) ref
-  val print_state_context: state -> unit
-  val print_state_default: bool -> state -> unit
-  val print_state_fn: (bool -> state -> unit) ref
-  val print_state: bool -> state -> unit
-  val pretty_state: bool -> state -> Pretty.T list
   exception UNDEF
   val node_history_of: state -> node History.T
   val node_of: state -> node
@@ -27,10 +21,19 @@
   val context_of: state -> Proof.context
   val proof_of: state -> Proof.state
   val enter_forward_proof: state -> Proof.state
+  val prompt_state_default: state -> string
+  val prompt_state_fn: (state -> string) ref
+  val print_state_context: state -> unit
+  val print_state_default: bool -> state -> unit
+  val print_state_hook: (bool -> state -> unit) -> unit
+  val print_state_fn: (bool -> state -> unit) ref
+  val print_state: bool -> state -> unit
+  val pretty_state: bool -> state -> Pretty.T list
   val quiet: bool ref
   val debug: bool ref
   val timing: bool ref
   val profiling: int ref
+  val skip_proofs: bool ref
   exception TERMINATE
   exception RESTART
   type transition
@@ -55,16 +58,15 @@
   val imperative: (unit -> unit) -> transition -> transition
   val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit)
     -> transition -> transition
-  val skip_proofs: bool ref
   val theory: (theory -> theory) -> transition -> transition
   val theory': (bool -> theory -> theory) -> transition -> transition
   val theory_to_proof: (bool -> theory -> ProofHistory.T) -> transition -> transition
   val proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition
   val proof': (bool -> ProofHistory.T -> ProofHistory.T) -> transition -> transition
-  val proof'': (ProofHistory.T -> ProofHistory.T) -> transition -> transition
+  val actual_proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition
+  val skip_proof: (int History.T -> int History.T) -> transition -> transition
   val proof_to_theory: (ProofHistory.T -> theory) -> transition -> transition
   val proof_to_theory': (bool -> ProofHistory.T -> theory) -> transition -> transition
-  val skip_proof: (int History.T -> int History.T) -> transition -> transition
   val skip_proof_to_theory: (int History.T -> bool) -> transition -> transition
   val unknown_theory: transition -> transition
   val unknown_proof: transition -> transition
@@ -88,32 +90,12 @@
 
 (** toplevel state **)
 
-(* datatype node *)
+(* datatype state *)
 
 datatype node =
   Theory of theory |
-  Proof of ProofHistory.T |
-  SkipProof of int History.T * theory;
-
-fun str_of_node (Theory _) = "in theory mode"
-  | str_of_node _ = "in proof mode";
-
-fun pretty_context thy = [Pretty.block
-  [Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name thy),
-    Pretty.str " =", Pretty.brk 1, ThyInfo.pretty_theory thy]];
-
-fun pretty_prf prf = Proof.pretty_state (ProofHistory.position prf) (ProofHistory.current prf);
-
-fun pretty_node_context (Theory thy) = pretty_context thy
-  | pretty_node_context (Proof prf) = pretty_context (Proof.theory_of (ProofHistory.current prf))
-  | pretty_node_context _ = [];
-
-fun pretty_node prf_only (Theory thy) = if prf_only then [] else pretty_context thy
-  | pretty_node _ (Proof prf) = pretty_prf prf
-  | pretty_node _ _ = [];
-
-
-(* datatype state *)
+  Proof of ProofHistory.T |              (*history of proof states*)
+  SkipProof of int History.T * theory;   (*history of proof depths*)
 
 datatype state = State of (node History.T * ((node -> unit) * (node -> unit))) option;
 
@@ -123,36 +105,11 @@
   | is_toplevel _ = false;
 
 fun str_of_state (State NONE) = "at top level"
-  | str_of_state (State (SOME (node, _))) = str_of_node (History.current node);
-
-
-(* prompt_state hook *)
-
-fun prompt_state_default (State _) = Source.default_prompt;
-
-val prompt_state_fn = ref prompt_state_default;
-fun prompt_state state = ! prompt_state_fn state;
-
-
-(* print state *)
-
-fun pretty_current_node _ (State NONE) = []
-  | pretty_current_node prt (State (SOME (node, _))) = prt (History.current node);
-
-val print_state_context =
-  Pretty.writeln o Pretty.chunks o pretty_current_node pretty_node_context;
-
-fun pretty_state prf_only state =
-  let val ref (begin_state, end_state, _) = Display.current_goals_markers in
-    (case pretty_current_node (pretty_node prf_only) state of [] => []
-    | prts =>
-        (if begin_state = "" then [] else [Pretty.str begin_state]) @ prts @
-        (if end_state = "" then [] else [Pretty.str end_state]))
-  end;
-
-fun print_state_default prf_only state = Pretty.writelns (pretty_state prf_only state);
-val print_state_fn = ref print_state_default;
-fun print_state state = ! print_state_fn state;
+  | str_of_state (State (SOME (node, _))) =
+      (case History.current node of
+        Theory _ => "in theory mode"
+      | Proof _ => "in proof mode"
+      | SkipProof _ => "in skipped proof mode");
 
 
 (* top node *)
@@ -167,8 +124,8 @@
 fun node_case f g state =
   (case node_of state of
     Theory thy => f thy
-  | SkipProof (i, thy) => f thy
-  | Proof prf => g (ProofHistory.current prf));
+  | Proof prf => g (ProofHistory.current prf)
+  | SkipProof (_, thy) => f thy);
 
 val theory_of = node_case I Proof.theory_of;
 val sign_of = theory_of;
@@ -178,6 +135,51 @@
 val enter_forward_proof = node_case Proof.init_state Proof.enter_forward;
 
 
+(* prompt state *)
+
+fun prompt_state_default (State _) = Source.default_prompt;
+
+val prompt_state_fn = ref prompt_state_default;
+fun prompt_state state = ! prompt_state_fn state;
+
+
+(* print state *)
+
+fun pretty_context thy = [Pretty.block
+  [Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name thy),
+    Pretty.str " =", Pretty.brk 1, ThyInfo.pretty_theory thy]];
+
+fun pretty_state_context state =
+  (case try theory_of state of NONE => []
+  | SOME thy => pretty_context thy);
+
+fun pretty_node prf_only (Theory thy) = if prf_only then [] else pretty_context thy
+  | pretty_node _ (Proof prf) =
+      Proof.pretty_state (ProofHistory.position prf) (ProofHistory.current prf)
+  | pretty_node _ (SkipProof (h, _)) =
+      [Pretty.str ("skipped proof: depth " ^ string_of_int (History.current h))];
+
+fun pretty_state prf_only state =
+  let val ref (begin_state, end_state, _) = Display.current_goals_markers in
+    (case try node_of state of NONE => []
+    | SOME node =>
+        (if begin_state = "" then [] else [Pretty.str begin_state]) @
+        pretty_node prf_only node @
+        (if end_state = "" then [] else [Pretty.str end_state]))
+  end;
+
+val print_state_context = Pretty.writelns o pretty_state_context;
+fun print_state_default prf_only state = Pretty.writelns (pretty_state prf_only state);
+
+val print_state_hooks = ref ([]: (bool -> state -> unit) list);
+fun print_state_hook f = change print_state_hooks (cons f);
+val print_state_fn = ref print_state_default;
+
+fun print_state prf_only state =
+ (List.app (fn f => (try (fn () => f prf_only state) (); ())) (! print_state_hooks);
+  ! print_state_fn prf_only state);
+
+
 
 (** toplevel transitions **)
 
@@ -185,6 +187,7 @@
 val debug = ref false;
 val timing = Output.timing;
 val profiling = ref 0;
+val skip_proofs = ref false;
 
 exception TERMINATE;
 exception RESTART;
@@ -192,31 +195,29 @@
 exception FAILURE of state * exn;
 
 
-(* recovery from stale theories *)
+(* node transactions and recovery from stale theories *)
 
-(*note: proof commands should be non-destructive!*)
+(*NB: proof commands should be non-destructive!*)
 
 local
 
 fun is_stale state = Context.is_stale (theory_of state) handle UNDEF => false;
 
+val stale_theory = ERROR_MESSAGE "Stale theory encountered after succesful execution!";
+
 fun checkpoint_node true (Theory thy) = Theory (Theory.checkpoint thy)
   | checkpoint_node _ node = node;
 
 fun copy_node true (Theory thy) = Theory (Theory.copy thy)
   | copy_node _ node = node;
 
-val stale_theory = ERROR_MESSAGE "Stale theory encountered after succesful execution!";
-
 fun return (result, NONE) = result
   | return (result, SOME exn) = raise FAILURE (result, exn);
 
 fun debug_trans f x =
   if ! debug then
-    let val y = ref x in
-      setmp Output.transform_exceptions false
-        exception_trace (fn () => y := f x); ! y
-    end
+    setmp Output.transform_exceptions false
+      exception_trace (fn () => f x)
   else f x;
 
 fun interruptible f x =
@@ -225,8 +226,8 @@
 
 in
 
-fun node_trans _ _ _ (State NONE) = raise UNDEF
-  | node_trans int hist f (State (SOME (node, term))) =
+fun transaction _ _ _ (State NONE) = raise UNDEF
+  | transaction int hist f (State (SOME (node, term))) =
       let
         val cont_node = History.map (checkpoint_node int) node;
         val back_node = History.map (copy_node int) cont_node;
@@ -254,12 +255,11 @@
 
 (* primitive transitions *)
 
-(*Important note: recovery from stale theories is provided only for
-  theory-level operations via MapCurrent and AppCurrent.  Other node
-  or state operations should not touch theories at all.
+(*NB: recovery from stale theories is provided only for theory-level
+  operations via MapCurrent and AppCurrent.  Other node or state
+  operations should not touch theories at all.
 
-  Also note that interrupts are enabled for Keep, MapCurrent, and
-  AppCurrent only.*)
+  Interrupts are enabled only for Keep, MapCurrent, and AppCurrent.*)
 
 datatype trans =
   Reset |                                       (*empty toplevel*)
@@ -289,8 +289,8 @@
   | apply_tr int (Keep f) state = (raise_interrupt (f int) state; state)
   | apply_tr _ (History _) (State NONE) = raise UNDEF
   | apply_tr _ (History f) (State (SOME (node, term))) = State (SOME (f node, term))
-  | apply_tr int (MapCurrent f) state = node_trans int false f state
-  | apply_tr int (AppCurrent f) state = node_trans int true f state;
+  | apply_tr int (MapCurrent f) state = transaction int false f state
+  | apply_tr int (AppCurrent f) state = transaction int true f state;
 
 fun apply_union _ [] state = raise FAILURE (state, UNDEF)
   | apply_union int (tr :: trs) state =
@@ -311,13 +311,13 @@
 (* datatype transition *)
 
 datatype transition = Transition of
- {name: string,
-  pos: Position.T,
-  source: OuterLex.token list option,
-  int_only: bool,
-  print: string list,
-  no_timing: bool,
-  trans: trans list};
+ {name: string,                        (*command name*)
+  pos: Position.T,                     (*source position*)
+  source: OuterLex.token list option,  (*source text*)
+  int_only: bool,                      (*interactive-only*)
+  print: string list,                  (*print modes (union)*)
+  no_timing: bool,                     (*suppress timing*)
+  trans: trans list};                  (*primitive transitions (union)*)
 
 fun make_transition (name, pos, source, int_only, print, no_timing, trans) =
   Transition {name = name, pos = pos, source = source,
@@ -391,14 +391,6 @@
 
 (* typed transitions *)
 
-(*The skip_proofs flag allows proof scripts to be skipped during
-  interactive proof in order to speed up processing of large
-  theories. While in skipping mode, states are represented as
-  SkipProof (h, thy), where h contains a counter for the number of
-  open proof blocks.*)
-
-val skip_proofs = ref false;
-
 fun theory f = app_current (fn _ => (fn Theory thy => Theory (f thy) | _ => raise UNDEF));
 fun theory' f = app_current (fn int => (fn Theory thy => Theory (f int thy) | _ => raise UNDEF));
 
@@ -409,13 +401,18 @@
         else Proof (f int thy)
     | _ => raise UNDEF));
 
-fun proof''' b f = map_current (fn int => (fn Proof prf => Proof (f int prf)
-  | SkipProof (h, thy) => if b then SkipProof (History.apply I h, thy) else raise UNDEF
-  | _ => raise UNDEF));
+fun proof' f = map_current (fn int =>
+  (fn Proof prf => Proof (f int prf)
+    | SkipProof (h, thy) => SkipProof (History.apply I h, thy)   (*approximate f*)
+    | _ => raise UNDEF));
 
-val proof' = proof''' true;
 val proof = proof' o K;
-val proof'' = proof''' false o K;
+
+fun actual_proof f = map_current (fn _ =>
+  (fn Proof prf => Proof (f prf) | _ => raise UNDEF));
+
+fun skip_proof f = map_current (fn _ =>
+  (fn SkipProof (h, thy) => SkipProof (f h, thy) | _ => raise UNDEF));
 
 fun proof_to_theory' f =
   map_current (fn int => (fn Proof prf => Theory (f int prf)
@@ -424,10 +421,7 @@
 
 val proof_to_theory = proof_to_theory' o K;
 
-fun skip_proof f = map_current (fn int =>
-  (fn SkipProof (h, thy) => SkipProof (f h, thy) | _ => raise UNDEF));
-
-fun skip_proof_to_theory p = map_current (fn int =>
+fun skip_proof_to_theory p = map_current (fn _ =>
   (fn SkipProof (h, thy) => if p h then Theory thy else raise UNDEF | _ => raise UNDEF));
 
 val unknown_theory = imperative (fn () => warning "Unknown theory context");
@@ -500,8 +494,6 @@
 
 (* apply transitions *)
 
-val quiet = ref false;
-
 local
 
 fun app int (tr as Transition {trans, int_only, print, no_timing, ...}) state =