# HG changeset patch
# User wenzelm
# Date 1278403344 -7200
# Node ID 8244558af8a55148b3c3ce8f0067795024110fa8
# Parent  17b05b104390b990450def62e1e8fe6e17227b7f# Parent  c82cf6e1166966c3b81c81e0e481f0e16baf0f23
merged

diff -r 17b05b104390 -r 8244558af8a5 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Jul 06 09:27:49 2010 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Jul 06 10:02:24 2010 +0200
@@ -240,7 +240,10 @@
     val _ = List.app Thy_Syntax.report_token toks;
   in
     (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
-      [tr] => (tr, true)
+      [tr] =>
+        if Keyword.is_control (Toplevel.name_of tr) then
+          (Toplevel.malformed range_pos "Illegal control command", true)
+        else (tr, true)
     | [] => (Toplevel.ignored range_pos, false)
     | _ => (Toplevel.malformed range_pos not_singleton, true))
     handle ERROR msg => (Toplevel.malformed range_pos msg, true)
diff -r 17b05b104390 -r 8244558af8a5 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Jul 06 09:27:49 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Jul 06 10:02:24 2010 +0200
@@ -563,8 +563,10 @@
 
 fun async_state (tr as Transition {print, ...}) st =
   if print then
-    ignore (Future.fork_group (Task_Queue.new_group (Future.worker_group ()))
-      (fn () => Future.report (setmp_thread_position tr (fn () => print_state false st))))
+    ignore
+      (Future.fork_group (Task_Queue.new_group (Future.worker_group ()))
+        (fn () =>
+          setmp_thread_position tr (fn () => Future.report (fn () => print_state false st)) ()))
   else ();
 
 fun error_msg tr exn_info =
diff -r 17b05b104390 -r 8244558af8a5 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Tue Jul 06 09:27:49 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Tue Jul 06 10:02:24 2010 +0200
@@ -157,9 +157,12 @@
     output_sync("Isabelle.command " + Isabelle_Syntax.encode_properties(props) + " " +
       Isabelle_Syntax.encode_string(text))
 
-  def ML(text: String) =
+  def ML_val(text: String) =
     output_sync("ML_val " + Isabelle_Syntax.encode_string(text))
 
+  def ML_command(text: String) =
+    output_sync("ML_command " + Isabelle_Syntax.encode_string(text))
+
   def close() = synchronized {    // FIXME watchdog/timeout
     output_raw("\u0000")
     closing = true