Toplevel.init_state;
authorwenzelm
Sat Dec 30 12:33:27 2006 +0100 (2006-12-30)
changeset 219574e44e74dc7e7
parent 21956 2cbee05b18a1
child 21958 9dfd1ca4c0a0
Toplevel.init_state;
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/session.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Sat Dec 30 12:33:26 2006 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sat Dec 30 12:33:27 2006 +0100
     1.3 @@ -318,7 +318,7 @@
     1.4    ml_prompts "ML> " "ML# ");
     1.5  
     1.6  fun gen_main term no_pos =
     1.7 - (Toplevel.set_state Toplevel.toplevel;
     1.8 + (Toplevel.init_state ();
     1.9    writeln (Session.welcome ());
    1.10    gen_loop term no_pos);
    1.11  
     2.1 --- a/src/Pure/Isar/session.ML	Sat Dec 30 12:33:26 2006 +0100
     2.2 +++ b/src/Pure/Isar/session.ML	Sat Dec 30 12:33:27 2006 +0100
     2.3 @@ -61,6 +61,7 @@
     2.4    (Output.accumulated_time ();
     2.5      ThyInfo.finish ();
     2.6      Present.finish ();
     2.7 +    Toplevel.init_state ();
     2.8      session_finished := true);
     2.9  
    2.10