1.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Jul 06 09:27:49 2010 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Jul 06 10:02:24 2010 +0200
     1.3 @@ -240,7 +240,10 @@
     1.4      val _ = List.app Thy_Syntax.report_token toks;
     1.5    in
     1.6      (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
     1.7 -      [tr] => (tr, true)
     1.8 +      [tr] =>
     1.9 +        if Keyword.is_control (Toplevel.name_of tr) then
    1.10 +          (Toplevel.malformed range_pos "Illegal control command", true)
    1.11 +        else (tr, true)
    1.12      | [] => (Toplevel.ignored range_pos, false)
    1.13      | _ => (Toplevel.malformed range_pos not_singleton, true))
    1.14      handle ERROR msg => (Toplevel.malformed range_pos msg, true)

     2.1 --- a/src/Pure/Isar/toplevel.ML	Tue Jul 06 09:27:49 2010 +0200
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Jul 06 10:02:24 2010 +0200
     2.3 @@ -563,8 +563,10 @@
     2.4  
     2.5  fun async_state (tr as Transition {print, ...}) st =
     2.6    if print then
     2.7 -    ignore (Future.fork_group (Task_Queue.new_group (Future.worker_group ()))
     2.8 -      (fn () => Future.report (setmp_thread_position tr (fn () => print_state false st))))
     2.9 +    ignore
    2.10 +      (Future.fork_group (Task_Queue.new_group (Future.worker_group ()))
    2.11 +        (fn () =>
    2.12 +          setmp_thread_position tr (fn () => Future.report (fn () => print_state false st)) ()))
    2.13    else ();
    2.14  
    2.15  fun error_msg tr exn_info =

     3.1 --- a/src/Pure/System/isabelle_process.scala	Tue Jul 06 09:27:49 2010 +0200
     3.2 +++ b/src/Pure/System/isabelle_process.scala	Tue Jul 06 10:02:24 2010 +0200
     3.3 @@ -157,9 +157,12 @@
     3.4      output_sync("Isabelle.command " + Isabelle_Syntax.encode_properties(props) + " " +
     3.5        Isabelle_Syntax.encode_string(text))
     3.6  
     3.7 -  def ML(text: String) =
     3.8 +  def ML_val(text: String) =
     3.9      output_sync("ML_val " + Isabelle_Syntax.encode_string(text))
    3.10  
    3.11 +  def ML_command(text: String) =
    3.12 +    output_sync("ML_command " + Isabelle_Syntax.encode_string(text))
    3.13 +
    3.14    def close() = synchronized {    // FIXME watchdog/timeout
    3.15      output_raw("\u0000")
    3.16      closing = true