# HG changeset patch
# User wenzelm
# Date 1165683944 -3600
# Node ID ec2014c93d7f1d3cc1bfa48b36bfa15acc8a5b56
# Parent  04b4ed5e3033695fae342fd83abf55df7c8579ef
added print_abbrevs;
exit: less verbosity;

diff -r 04b4ed5e3033 -r ec2014c93d7f src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sat Dec 09 18:05:43 2006 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Dec 09 18:05:44 2006 +0100
@@ -70,6 +70,7 @@
   val print_context: Toplevel.transition -> Toplevel.transition
   val print_theory: bool -> Toplevel.transition -> Toplevel.transition
   val print_syntax: Toplevel.transition -> Toplevel.transition
+  val print_abbrevs: Toplevel.transition -> Toplevel.transition
   val print_facts: Toplevel.transition -> Toplevel.transition
   val print_theorems: Toplevel.transition -> Toplevel.transition
   val print_locales: Toplevel.transition -> Toplevel.transition
@@ -215,9 +216,7 @@
 val welcome = Toplevel.imperative (writeln o Session.welcome);
 
 val exit = Toplevel.keep (fn state =>
-  (Context.set_context (try Toplevel.theory_of state);
-    writeln "Leaving the Isar loop.  Invoke 'Isar.loop();' to continue.";
-    raise Toplevel.TERMINATE));
+  (Context.set_context (try Toplevel.theory_of state); raise Toplevel.TERMINATE));
 
 val quit = Toplevel.imperative quit;
 
@@ -337,6 +336,9 @@
 val print_syntax = Toplevel.unknown_context o
   Toplevel.keep (ProofContext.print_syntax o Toplevel.context_of);
 
+val print_abbrevs = Toplevel.unknown_context o
+  Toplevel.keep (ProofContext.print_abbrevs o Toplevel.context_of);
+
 val print_facts = Toplevel.unknown_context o Toplevel.keep (fn state =>
   ProofContext.setmp_verbose
     ProofContext.print_lthms (Toplevel.context_of state));