re-init ml_prompts after loop termination;
authorwenzelm
Tue, 17 May 2005 18:10:42 +0200
changeset 15989 80dd2f5780df
parent 15988 181bbcee76f5
child 15990 4ef32dcbb44f
re-init ml_prompts after loop termination;
src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue May 17 18:10:41 2005 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue May 17 18:10:42 2005 +0200
@@ -372,7 +372,8 @@
 
 fun gen_loop term no_pos =
  (Context.reset_context ();
-  Toplevel.loop (isar term no_pos));
+  Toplevel.loop (isar term no_pos);
+  ml_prompts "ML> " "ML# ");
 
 fun gen_main term no_pos =
  (Toplevel.set_state Toplevel.toplevel;