src/Pure/System/session.scala

--- a/src/Pure/System/session.scala	Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/System/session.scala	Mon Nov 28 22:05:32 2011 +0100
@@ -363,7 +363,7 @@
           catch {
             case _: Document.State.Fail => bad_result(result)
           }
-        case Markup.Assign_Execs if result.is_raw =>
+        case Isabelle_Markup.Assign_Execs if result.is_raw =>
           XML.content(result.body).mkString match {
             case Isar_Document.Assign(id, assign) =>
               try { handle_assign(id, assign) }
@@ -376,20 +376,20 @@
             if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
             prune_next = System.currentTimeMillis() + prune_delay.ms
           }
-        case Markup.Removed_Versions if result.is_raw =>
+        case Isabelle_Markup.Removed_Versions if result.is_raw =>
           XML.content(result.body).mkString match {
             case Isar_Document.Removed(removed) =>
               try { handle_removed(removed) }
               catch { case _: Document.State.Fail => bad_result(result) }
             case _ => bad_result(result)
           }
-        case Markup.Invoke_Scala(name, id) if result.is_raw =>
+        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 Markup.Cancel_Scala(id) =>
+        case Isabelle_Markup.Cancel_Scala(id) =>
           System.err.println("cancel_scala " + id)  // FIXME cancel JVM task
         case _ =>
           if (result.is_syslog) {