src/Pure/System/session.scala
changeset 39525 72e949a0425b
parent 39524 59ebce09ce6e
child 39528 c01d89d18ff0
--- a/src/Pure/System/session.scala	Sat Sep 18 21:33:56 2010 +0200
+++ b/src/Pure/System/session.scala	Sun Sep 19 17:12:34 2010 +0200
@@ -200,8 +200,8 @@
               case _ => if (!result.is_ready) bad_result(result)
             }
           }
-          else if (result.kind == Markup.EXIT) prover = null
-          else if (result.is_raw) raw_output.event(result)
+          else if (result.is_exit) prover = null  // FIXME ??
+          else if (result.is_stdout) raw_output.event(result)
           else if (!result.is_system) bad_result(result)  // FIXME syslog for system messages (!?)
         }
     }
@@ -216,7 +216,7 @@
       while (
         receiveWithin(0) {
           case result: Isabelle_Process.Result =>
-            if (result.is_raw) {
+            if (result.is_stdout) {
               for (text <- XML.content(result.message))
                 buf.append(text)
             }
@@ -229,16 +229,14 @@
     def prover_startup(timeout: Int): Option[String] =
     {
       receiveWithin(timeout) {
-        case result: Isabelle_Process.Result
-          if result.kind == Markup.INIT =>
+        case result: Isabelle_Process.Result if result.is_init =>
           while (receive {
             case result: Isabelle_Process.Result =>
               handle_result(result); !result.is_ready
             }) {}
           None
 
-        case result: Isabelle_Process.Result
-          if result.kind == Markup.EXIT =>
+        case result: Isabelle_Process.Result if result.is_exit =>
           Some(startup_error())
 
         case TIMEOUT =>  // FIXME clarify