src/Pure/System/session.scala

--- a/src/Pure/System/session.scala	Thu Jan 05 14:15:37 2012 +0100
+++ b/src/Pure/System/session.scala	Thu Jan 05 14:34:18 2012 +0100
@@ -355,6 +355,7 @@
       }
 
       result.properties match {
+
         case Position.Id(state_id) if !result.is_raw =>
           try {
             val st = global_state.change_yield(_.accumulate(state_id, result.message))
@@ -363,6 +364,7 @@
           catch {
             case _: Document.State.Fail => bad_result(result)
           }
+
         case Isabelle_Markup.Assign_Execs if result.is_raw =>
           XML.content(result.body).mkString match {
             case Protocol.Assign(id, assign) =>
@@ -376,6 +378,7 @@
             if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
             prune_next = System.currentTimeMillis() + prune_delay.ms
           }
+
         case Isabelle_Markup.Removed_Versions if result.is_raw =>
           XML.content(result.body).mkString match {
             case Protocol.Removed(removed) =>
@@ -383,19 +386,26 @@
               catch { case _: Document.State.Fail => bad_result(result) }
             case _ => bad_result(result)
           }
+
         case Isabelle_Markup.Invoke_Scala(name, id) if result.is_raw =>
           Future.fork {
             val arg = XML.content(result.body).mkString
             val (tag, res) = Invoke_Scala.method(name, arg)
             prover.get.invoke_scala(id, tag, res)
           }
+
         case Isabelle_Markup.Cancel_Scala(id) if result.is_raw =>
           System.err.println("cancel_scala " + id)  // FIXME actually cancel JVM task
+
         case Isabelle_Markup.Ready if result.is_raw =>
             // FIXME move to ML side (!?)
             syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have")
             syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show")
             phase = Session.Ready
+
+        case Isabelle_Markup.Loaded_Theory(name) if result.is_raw =>
+          thy_load.register_thy(name)
+
         case _ =>
           if (result.is_syslog) {
             reverse_syslog ::= result.message
@@ -407,7 +417,6 @@
             result.body match {
               case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
               case List(Keyword.Keyword_Decl(name)) => syntax += name
-              case List(Thy_Info.Loaded_Theory(name)) => thy_load.register_thy(name)
               case _ => bad_result(result)
             }
           }