merged

--- 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)

--- 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 =

--- 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