# HG changeset patch
# User wenzelm
# Date 1116346242 -7200
# Node ID 80dd2f5780df8ccc9590d6b3819582184ec487d7
# Parent  181bbcee76f5137d612e95cd487ff503648427ad
re-init ml_prompts after loop termination;

diff -r 181bbcee76f5 -r 80dd2f5780df 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;