1.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Oct 20 15:22:56 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Oct 20 15:23:55 1999 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4    val undo: Toplevel.transition -> Toplevel.transition
     1.5    val use: string -> Toplevel.transition -> Toplevel.transition
     1.6    val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition
     1.7 -  val use_mltext: string -> Toplevel.transition -> Toplevel.transition
     1.8 +  val use_mltext: bool -> string -> Toplevel.transition -> Toplevel.transition
     1.9    val use_commit: Toplevel.transition -> Toplevel.transition
    1.10    val cd: string -> Toplevel.transition -> Toplevel.transition
    1.11    val pwd: Toplevel.transition -> Toplevel.transition
    1.12 @@ -100,11 +100,11 @@
    1.13  val use_mltext_theory = Toplevel.theory' o IsarThy.use_mltext_theory;
    1.14  
    1.15  (*ignore result theory context*)
    1.16 -fun use_mltext txt = Toplevel.keep' (fn verb => fn state =>
    1.17 -  (IsarThy.use_mltext txt verb (try Toplevel.theory_of state)));
    1.18 +fun use_mltext v txt = Toplevel.keep' (fn verb => fn state =>
    1.19 +  (IsarThy.use_mltext txt (v andalso verb) (try Toplevel.theory_of state)));
    1.20  
    1.21  (*Note: commit is dynamically bound*)
    1.22 -val use_commit = use_mltext "commit();";
    1.23 +val use_commit = use_mltext false "commit();";
    1.24  
    1.25  
    1.26  (* current working directory *)

     2.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Oct 20 15:22:56 1999 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Oct 20 15:23:55 1999 +0200
     2.3 @@ -207,7 +207,11 @@
     2.4  
     2.5  val mlP =
     2.6    OuterSyntax.command "ML" "eval ML text (diagnostic)" K.diag
     2.7 -    (P.text >> IsarCmd.use_mltext)
     2.8 +    (P.text >> IsarCmd.use_mltext true);
     2.9 +
    2.10 +val ml_commandP =
    2.11 +  OuterSyntax.command "ML_command" "eval ML text" K.diag
    2.12 +    (P.text >> IsarCmd.use_mltext false);
    2.13  
    2.14  val ml_setupP =
    2.15    OuterSyntax.command "ML_setup" "eval ML text (may change theory)" K.thy_decl
    2.16 @@ -612,8 +616,8 @@
    2.17    classesP, classrelP, defaultsortP, typedeclP, typeabbrP, nontermP,
    2.18    aritiesP, constsP, syntaxP, translationsP, axiomsP, defsP,
    2.19    constdefsP, theoremsP, lemmasP, globalP, localP, useP, mlP,
    2.20 -  ml_setupP, setupP, parse_ast_translationP, parse_translationP,
    2.21 -  print_translationP, typed_print_translationP,
    2.22 +  ml_commandP, ml_setupP, setupP, parse_ast_translationP,
    2.23 +  parse_translationP, print_translationP, typed_print_translationP,
    2.24    print_ast_translationP, token_translationP, oracleP,
    2.25    (*proof commands*)
    2.26    theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,