# 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;