src/Pure/Isar/isar_syn.ML
changeset 26490 87d27e426f14
parent 26435 bdce320cd426
child 26516 1bf210ac0a90
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Mar 29 19:14:11 2008 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Mar 29 19:14:12 2008 +0100
     1.3 @@ -302,24 +302,21 @@
     1.4  (* use ML text *)
     1.5  
     1.6  val _ =
     1.7 -  OuterSyntax.command "use" "eval ML text from file" (K.tag_ml K.diag)
     1.8 -    (P.path >> (Toplevel.no_timing oo IsarCmd.use));
     1.9 +  OuterSyntax.command "use" "eval ML text from file" (K.tag_ml K.thy_decl)
    1.10 +    (P.path >> (Toplevel.generic_theory o ThyInfo.exec_file false));
    1.11  
    1.12  val _ =
    1.13 -  OuterSyntax.command "ML" "eval ML text (diagnostic)" (K.tag_ml K.diag)
    1.14 -    (P.position P.text >> IsarCmd.use_mltext true);
    1.15 +  OuterSyntax.command "ML" "eval ML text (diagnostic)" (K.tag_ml K.thy_decl)
    1.16 +    (P.position P.text >> (fn (txt, pos) =>
    1.17 +      Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt))));
    1.18  
    1.19  val _ =
    1.20    OuterSyntax.command "ML_val" "eval ML text (diagnostic)" (K.tag_ml K.diag)
    1.21 -    (P.position P.text >> IsarCmd.use_mltext true);
    1.22 +    (P.position P.text >> IsarCmd.ml_diag true);
    1.23  
    1.24  val _ =
    1.25    OuterSyntax.command "ML_command" "silently eval ML text (diagnostic)" (K.tag_ml K.diag)
    1.26 -    (P.position P.text >> (Toplevel.no_timing oo IsarCmd.use_mltext false));
    1.27 -
    1.28 -val _ =
    1.29 -  OuterSyntax.command "ML_setup" "eval ML text (may change theory)" (K.tag_ml K.thy_decl)
    1.30 -    (P.position P.text >> IsarCmd.use_mltext_theory);
    1.31 +    (P.position P.text >> (Toplevel.no_timing oo IsarCmd.ml_diag false));
    1.32  
    1.33  val _ =
    1.34    OuterSyntax.command "setup" "apply ML theory setup" (K.tag_ml K.thy_decl)
    1.35 @@ -991,7 +988,7 @@
    1.36  
    1.37  val _ =
    1.38    OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag
    1.39 -    (P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.use_commit));
    1.40 +    (P.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit));
    1.41  
    1.42  val _ =
    1.43    OuterSyntax.improper_command "quit" "quit Isabelle" K.control