src/Pure/System/session.scala
changeset 37689 628eabe2213a
parent 37132 10ef4da1c314
child 37849 4f9de312cc23
     1.1 --- a/src/Pure/System/session.scala	Sat Jul 03 23:24:36 2010 +0200
     1.2 +++ b/src/Pure/System/session.scala	Sun Jul 04 00:05:32 2010 +0200
     1.3 @@ -110,14 +110,14 @@
     1.4      {
     1.5        raw_results.event(result)
     1.6  
     1.7 -      val target_id: Option[Session.Entity_ID] = Position.get_id(result.props)
     1.8 +      val target_id: Option[Session.Entity_ID] = Position.get_id(result.message.attributes)
     1.9        val target: Option[Session.Entity] =
    1.10          target_id match {
    1.11            case None => None
    1.12            case Some(id) => lookup_entity(id)
    1.13          }
    1.14        if (target.isDefined) target.get.consume(result.message, indicate_command_change)
    1.15 -      else if (result.kind == Isabelle_Process.Kind.STATUS) {
    1.16 +      else if (result.is_status) {
    1.17          // global status message
    1.18          result.body match {
    1.19  
    1.20 @@ -145,7 +145,7 @@
    1.21            case _ => if (!result.is_ready) bad_result(result)
    1.22          }
    1.23        }
    1.24 -      else if (result.kind == Isabelle_Process.Kind.EXIT)
    1.25 +      else if (result.kind == Markup.EXIT)
    1.26          prover = null
    1.27        else if (result.is_raw)
    1.28          raw_output.event(result)
    1.29 @@ -176,7 +176,7 @@
    1.30      {
    1.31        receiveWithin(timeout) {
    1.32          case result: Isabelle_Process.Result
    1.33 -          if result.kind == Isabelle_Process.Kind.INIT =>
    1.34 +          if result.kind == Markup.INIT =>
    1.35            while (receive {
    1.36              case result: Isabelle_Process.Result =>
    1.37                handle_result(result); !result.is_ready
    1.38 @@ -184,7 +184,7 @@
    1.39            None
    1.40  
    1.41          case result: Isabelle_Process.Result
    1.42 -          if result.kind == Isabelle_Process.Kind.EXIT =>
    1.43 +          if result.kind == Markup.EXIT =>
    1.44            Some(startup_error())
    1.45  
    1.46          case TIMEOUT =>  // FIXME clarify