diff -r 2c94c065564e -r c26369c9eda6 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/System/session.scala	Sun Nov 25 19:49:24 2012 +0100
@@ -314,7 +314,7 @@
             case _: Document.State.Fail => bad_output(output)
           }
 
-        case Isabelle_Markup.Assign_Execs if output.is_protocol =>
+        case Markup.Assign_Execs if output.is_protocol =>
           XML.content(output.body) match {
             case Protocol.Assign(id, assign) =>
               try {
@@ -331,7 +331,7 @@
             prune_next = System.currentTimeMillis() + prune_delay.ms
           }
 
-        case Isabelle_Markup.Removed_Versions if output.is_protocol =>
+        case Markup.Removed_Versions if output.is_protocol =>
           XML.content(output.body) match {
             case Protocol.Removed(removed) =>
               try {
@@ -341,7 +341,7 @@
             case _ => bad_output(output)
           }
 
-        case Isabelle_Markup.Invoke_Scala(name, id) if output.is_protocol =>
+        case Markup.Invoke_Scala(name, id) if output.is_protocol =>
           futures += (id ->
             default_thread_pool.submit(() =>
               {
@@ -350,7 +350,7 @@
                 this_actor ! Finished_Scala(id, tag, result)
               }))
 
-        case Isabelle_Markup.Cancel_Scala(id) if output.is_protocol =>
+        case Markup.Cancel_Scala(id) if output.is_protocol =>
           futures.get(id) match {
             case Some(future) =>
               future.cancel(true)
@@ -361,7 +361,7 @@
         case _ if output.is_init =>
             phase = Session.Ready
 
-        case Isabelle_Markup.Return_Code(rc) if output.is_exit =>
+        case Markup.Return_Code(rc) if output.is_exit =>
           if (rc == 0) phase = Session.Inactive
           else phase = Session.Failed