# HG changeset patch
# User wenzelm
# Date 940425835 -7200
# Node ID c77ad0c3c92f728a158715bdabb25e9a467a220e
# Parent  0aa16bc2abdb1b58aaa3e6e99dc608b217b79d3c
use_mltext: better control of verbosity;

diff -r 0aa16bc2abdb -r c77ad0c3c92f src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Oct 20 15:22:56 1999 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Oct 20 15:23:55 1999 +0200
@@ -23,7 +23,7 @@
   val undo: Toplevel.transition -> Toplevel.transition
   val use: string -> Toplevel.transition -> Toplevel.transition
   val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition
-  val use_mltext: string -> Toplevel.transition -> Toplevel.transition
+  val use_mltext: bool -> string -> Toplevel.transition -> Toplevel.transition
   val use_commit: Toplevel.transition -> Toplevel.transition
   val cd: string -> Toplevel.transition -> Toplevel.transition
   val pwd: Toplevel.transition -> Toplevel.transition
@@ -100,11 +100,11 @@
 val use_mltext_theory = Toplevel.theory' o IsarThy.use_mltext_theory;
 
 (*ignore result theory context*)
-fun use_mltext txt = Toplevel.keep' (fn verb => fn state =>
-  (IsarThy.use_mltext txt verb (try Toplevel.theory_of state)));
+fun use_mltext v txt = Toplevel.keep' (fn verb => fn state =>
+  (IsarThy.use_mltext txt (v andalso verb) (try Toplevel.theory_of state)));
 
 (*Note: commit is dynamically bound*)
-val use_commit = use_mltext "commit();";
+val use_commit = use_mltext false "commit();";
 
 
 (* current working directory *)
diff -r 0aa16bc2abdb -r c77ad0c3c92f src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Oct 20 15:22:56 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Oct 20 15:23:55 1999 +0200
@@ -207,7 +207,11 @@
 
 val mlP =
   OuterSyntax.command "ML" "eval ML text (diagnostic)" K.diag
-    (P.text >> IsarCmd.use_mltext)
+    (P.text >> IsarCmd.use_mltext true);
+
+val ml_commandP =
+  OuterSyntax.command "ML_command" "eval ML text" K.diag
+    (P.text >> IsarCmd.use_mltext false);
 
 val ml_setupP =
   OuterSyntax.command "ML_setup" "eval ML text (may change theory)" K.thy_decl
@@ -612,8 +616,8 @@
   classesP, classrelP, defaultsortP, typedeclP, typeabbrP, nontermP,
   aritiesP, constsP, syntaxP, translationsP, axiomsP, defsP,
   constdefsP, theoremsP, lemmasP, globalP, localP, useP, mlP,
-  ml_setupP, setupP, parse_ast_translationP, parse_translationP,
-  print_translationP, typed_print_translationP,
+  ml_commandP, ml_setupP, setupP, parse_ast_translationP,
+  parse_translationP, print_translationP, typed_print_translationP,
   print_ast_translationP, token_translationP, oracleP,
   (*proof commands*)
   theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,