# HG changeset patch
# User wenzelm
# Date 933105563 -7200
# Node ID dcd7ac72f1e7dda7ee253caaf4ef40d79bdb6cf2
# Parent  247e4247b64e4138423f347966ee1013ec7dab65
init / init_theory: pass int flag;

diff -r 247e4247b64e -r dcd7ac72f1e7 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Jul 27 21:58:59 1999 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Jul 27 21:59:23 1999 +0200
@@ -32,13 +32,13 @@
   val interactive: bool -> transition -> transition
   val print: transition -> transition
   val reset: transition -> transition
-  val init: (state -> node) -> (node -> unit) -> (node -> unit) -> transition -> transition
+  val init: (bool -> state -> node) -> (node -> unit) -> (node -> unit) -> transition -> transition
   val exit: transition -> transition
   val kill: transition -> transition
   val keep: (state -> unit) -> transition -> transition
   val history: (node History.T -> node History.T) -> transition -> transition
   val imperative: (unit -> unit) -> transition -> transition
-  val init_theory: (unit -> theory) -> (theory -> unit) -> (theory -> unit)
+  val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit)
     -> transition -> transition
   val theory: (theory -> theory) -> transition -> transition
   val theory_to_proof: (bool -> theory -> ProofHistory.T) -> transition -> transition
@@ -205,7 +205,7 @@
 
 datatype trans =
   Reset |                                       (*empty toplevel*)
-  Init of (state -> node) * ((node -> unit) * (node -> unit)) |
+  Init of (bool -> state -> node) * ((node -> unit) * (node -> unit)) |
     (*push node; provide exit/kill operation*)
   Exit |                                        (*pop node*)
   Kill |                                        (*abort node*)
@@ -220,7 +220,7 @@
 
 fun apply_tr _ Reset _ = toplevel
   | apply_tr int (Init (f, term)) (state as State nodes) =
-      State ((History.init (undo_limit int) (f state), term) :: nodes)
+      State ((History.init (undo_limit int) (f int state), term) :: nodes)
   | apply_tr _ Exit (State []) = raise UNDEF
   | apply_tr _ Exit (State ((node, (exit, _)):: nodes)) =
       (exit (History.current node); State nodes)
@@ -310,7 +310,7 @@
 fun imperative f = keep (fn _ => f ());
 
 fun init_theory f exit kill =
-  init (fn _ => Theory (f ()))
+  init (fn int => fn _ => Theory (f int))
     (fn Theory thy => exit thy | _ => raise UNDEF)
     (fn Theory thy => kill thy | _ => raise UNDEF);