src/Pure/System/session.scala
changeset 39525 72e949a0425b
parent 39524 59ebce09ce6e
child 39528 c01d89d18ff0
     1.1 --- a/src/Pure/System/session.scala	Sat Sep 18 21:33:56 2010 +0200
     1.2 +++ b/src/Pure/System/session.scala	Sun Sep 19 17:12:34 2010 +0200
     1.3 @@ -200,8 +200,8 @@
     1.4                case _ => if (!result.is_ready) bad_result(result)
     1.5              }
     1.6            }
     1.7 -          else if (result.kind == Markup.EXIT) prover = null
     1.8 -          else if (result.is_raw) raw_output.event(result)
     1.9 +          else if (result.is_exit) prover = null  // FIXME ??
    1.10 +          else if (result.is_stdout) raw_output.event(result)
    1.11            else if (!result.is_system) bad_result(result)  // FIXME syslog for system messages (!?)
    1.12          }
    1.13      }
    1.14 @@ -216,7 +216,7 @@
    1.15        while (
    1.16          receiveWithin(0) {
    1.17            case result: Isabelle_Process.Result =>
    1.18 -            if (result.is_raw) {
    1.19 +            if (result.is_stdout) {
    1.20                for (text <- XML.content(result.message))
    1.21                  buf.append(text)
    1.22              }
    1.23 @@ -229,16 +229,14 @@
    1.24      def prover_startup(timeout: Int): Option[String] =
    1.25      {
    1.26        receiveWithin(timeout) {
    1.27 -        case result: Isabelle_Process.Result
    1.28 -          if result.kind == Markup.INIT =>
    1.29 +        case result: Isabelle_Process.Result if result.is_init =>
    1.30            while (receive {
    1.31              case result: Isabelle_Process.Result =>
    1.32                handle_result(result); !result.is_ready
    1.33              }) {}
    1.34            None
    1.35  
    1.36 -        case result: Isabelle_Process.Result
    1.37 -          if result.kind == Markup.EXIT =>
    1.38 +        case result: Isabelle_Process.Result if result.is_exit =>
    1.39            Some(startup_error())
    1.40  
    1.41          case TIMEOUT =>  // FIXME clarify