# HG changeset patch
# User wenzelm
# Date 1206814452 -3600
# Node ID 87d27e426f14282273eb9c3852ca86985deb8162
# Parent  e83dc4bb9ab4541fcd33bf12bb89fa7dcd0f3823
commands 'use' and 'ML' now thy_decl;
removed obsolete 'ML_setup' -- superceded by 'ML';

diff -r e83dc4bb9ab4 -r 87d27e426f14 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Mar 29 19:14:11 2008 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sat Mar 29 19:14:12 2008 +0100
@@ -302,24 +302,21 @@
 (* use ML text *)
 
 val _ =
-  OuterSyntax.command "use" "eval ML text from file" (K.tag_ml K.diag)
-    (P.path >> (Toplevel.no_timing oo IsarCmd.use));
+  OuterSyntax.command "use" "eval ML text from file" (K.tag_ml K.thy_decl)
+    (P.path >> (Toplevel.generic_theory o ThyInfo.exec_file false));
 
 val _ =
-  OuterSyntax.command "ML" "eval ML text (diagnostic)" (K.tag_ml K.diag)
-    (P.position P.text >> IsarCmd.use_mltext true);
+  OuterSyntax.command "ML" "eval ML text (diagnostic)" (K.tag_ml K.thy_decl)
+    (P.position P.text >> (fn (txt, pos) =>
+      Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt))));
 
 val _ =
   OuterSyntax.command "ML_val" "eval ML text (diagnostic)" (K.tag_ml K.diag)
-    (P.position P.text >> IsarCmd.use_mltext true);
+    (P.position P.text >> IsarCmd.ml_diag true);
 
 val _ =
   OuterSyntax.command "ML_command" "silently eval ML text (diagnostic)" (K.tag_ml K.diag)
-    (P.position P.text >> (Toplevel.no_timing oo IsarCmd.use_mltext false));
-
-val _ =
-  OuterSyntax.command "ML_setup" "eval ML text (may change theory)" (K.tag_ml K.thy_decl)
-    (P.position P.text >> IsarCmd.use_mltext_theory);
+    (P.position P.text >> (Toplevel.no_timing oo IsarCmd.ml_diag false));
 
 val _ =
   OuterSyntax.command "setup" "apply ML theory setup" (K.tag_ml K.thy_decl)
@@ -991,7 +988,7 @@
 
 val _ =
   OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag
-    (P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.use_commit));
+    (P.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit));
 
 val _ =
   OuterSyntax.improper_command "quit" "quit Isabelle" K.control