1.1 --- a/src/Pure/System/isabelle_process.scala	Sat Jul 03 23:24:36 2010 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Sun Jul 04 00:05:32 2010 +0200
     1.3 @@ -19,89 +19,55 @@
     1.4  {
     1.5    /* results */
     1.6  
     1.7 -  object Kind extends Enumeration {
     1.8 -    //{{{ values and codes
     1.9 -    // internal system notification
    1.10 -    val SYSTEM = Value("SYSTEM")
    1.11 -    // Posix channels/events
    1.12 -    val STDIN = Value("STDIN")
    1.13 -    val STDOUT = Value("STDOUT")
    1.14 -    val SIGNAL = Value("SIGNAL")
    1.15 -    val EXIT = Value("EXIT")
    1.16 -    // Isabelle messages
    1.17 -    val INIT = Value("INIT")
    1.18 -    val STATUS = Value("STATUS")
    1.19 -    val WRITELN = Value("WRITELN")
    1.20 -    val TRACING = Value("TRACING")
    1.21 -    val WARNING = Value("WARNING")
    1.22 -    val ERROR = Value("ERROR")
    1.23 -    val DEBUG = Value("DEBUG")
    1.24 -    // messages codes
    1.25 -    val code = Map(
    1.26 -      ('A' : Int) -> Kind.INIT,
    1.27 -      ('B' : Int) -> Kind.STATUS,
    1.28 -      ('C' : Int) -> Kind.WRITELN,
    1.29 -      ('D' : Int) -> Kind.TRACING,
    1.30 -      ('E' : Int) -> Kind.WARNING,
    1.31 -      ('F' : Int) -> Kind.ERROR,
    1.32 -      ('G' : Int) -> Kind.DEBUG,
    1.33 -      ('0' : Int) -> Kind.SYSTEM,
    1.34 -      ('1' : Int) -> Kind.STDIN,
    1.35 -      ('2' : Int) -> Kind.STDOUT,
    1.36 -      ('3' : Int) -> Kind.SIGNAL,
    1.37 -      ('4' : Int) -> Kind.EXIT)
    1.38 +  object Kind {
    1.39      // message markup
    1.40      val markup = Map(
    1.41 -      Kind.INIT -> Markup.INIT,
    1.42 -      Kind.STATUS -> Markup.STATUS,
    1.43 -      Kind.WRITELN -> Markup.WRITELN,
    1.44 -      Kind.TRACING -> Markup.TRACING,
    1.45 -      Kind.WARNING -> Markup.WARNING,
    1.46 -      Kind.ERROR -> Markup.ERROR,
    1.47 -      Kind.DEBUG -> Markup.DEBUG,
    1.48 -      Kind.SYSTEM -> Markup.SYSTEM,
    1.49 -      Kind.STDIN -> Markup.STDIN,
    1.50 -      Kind.STDOUT -> Markup.STDOUT,
    1.51 -      Kind.SIGNAL -> Markup.SIGNAL,
    1.52 -      Kind.EXIT -> Markup.EXIT)
    1.53 -    //}}}
    1.54 -    def is_raw(kind: Value) =
    1.55 -      kind == STDOUT
    1.56 -    def is_control(kind: Value) =
    1.57 -      kind == SYSTEM ||
    1.58 -      kind == SIGNAL ||
    1.59 -      kind == EXIT
    1.60 -    def is_system(kind: Value) =
    1.61 -      kind == SYSTEM ||
    1.62 -      kind == STDIN ||
    1.63 -      kind == SIGNAL ||
    1.64 -      kind == EXIT ||
    1.65 -      kind == STATUS
    1.66 +      ('A' : Int) -> Markup.INIT,
    1.67 +      ('B' : Int) -> Markup.STATUS,
    1.68 +      ('C' : Int) -> Markup.WRITELN,
    1.69 +      ('D' : Int) -> Markup.TRACING,
    1.70 +      ('E' : Int) -> Markup.WARNING,
    1.71 +      ('F' : Int) -> Markup.ERROR,
    1.72 +      ('G' : Int) -> Markup.DEBUG)
    1.73 +    def is_raw(kind: String) =
    1.74 +      kind == Markup.STDOUT
    1.75 +    def is_control(kind: String) =
    1.76 +      kind == Markup.SYSTEM ||
    1.77 +      kind == Markup.SIGNAL ||
    1.78 +      kind == Markup.EXIT
    1.79 +    def is_system(kind: String) =
    1.80 +      kind == Markup.SYSTEM ||
    1.81 +      kind == Markup.STDIN ||
    1.82 +      kind == Markup.SIGNAL ||
    1.83 +      kind == Markup.EXIT ||
    1.84 +      kind == Markup.STATUS
    1.85    }
    1.86  
    1.87 -  class Result(val kind: Kind.Value, val props: List[(String, String)], val body: List[XML.Tree])
    1.88 +  class Result(val message: XML.Elem)
    1.89    {
    1.90 -    def message = XML.Elem(Kind.markup(kind), props, body)
    1.91 +    def kind = message.name
    1.92 +    def body = message.body
    1.93 +
    1.94 +    def is_raw = Kind.is_raw(kind)
    1.95 +    def is_control = Kind.is_control(kind)
    1.96 +    def is_system = Kind.is_system(kind)
    1.97 +    def is_status = kind == Markup.STATUS
    1.98 +    def is_ready = is_status && body == List(XML.Elem(Markup.READY, Nil, Nil))
    1.99  
   1.100      override def toString: String =
   1.101      {
   1.102        val res =
   1.103 -        if (kind == Kind.STATUS) body.map(_.toString).mkString
   1.104 -        else Pretty.string_of(body)
   1.105 +        if (is_status) message.body.map(_.toString).mkString
   1.106 +        else Pretty.string_of(message.body)
   1.107 +      val props = message.attributes
   1.108        if (props.isEmpty)
   1.109          kind.toString + " [[" + res + "]]"
   1.110        else
   1.111          kind.toString + " " +
   1.112            (for ((x, y) <- props) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
   1.113      }
   1.114 -    def is_raw = Kind.is_raw(kind)
   1.115 -    def is_control = Kind.is_control(kind)
   1.116 -    def is_system = Kind.is_system(kind)
   1.117  
   1.118 -    def is_ready = kind == Kind.STATUS && body == List(XML.Elem(Markup.READY, Nil, Nil))
   1.119 -
   1.120 -    def cache(c: XML.Cache): Result =
   1.121 -      new Result(kind, c.cache_props(props), c.cache_trees(body))
   1.122 +    def cache(c: XML.Cache): Result = new Result(c.cache_tree(message).asInstanceOf[XML.Elem])
   1.123    }
   1.124  }
   1.125  
   1.126 @@ -127,15 +93,15 @@
   1.127  
   1.128    /* results */
   1.129  
   1.130 -  private def put_result(kind: Kind.Value, props: List[(String, String)], body: List[XML.Tree])
   1.131 +  private def put_result(kind: String, props: List[(String, String)], body: List[XML.Tree])
   1.132    {
   1.133 -    if (kind == Kind.INIT) {
   1.134 +    if (kind == Markup.INIT) {
   1.135        for ((Markup.PID, p) <- props) pid = p
   1.136      }
   1.137 -    receiver ! new Result(kind, props, body)
   1.138 +    receiver ! new Result(XML.Elem(kind, props, body))
   1.139    }
   1.140  
   1.141 -  private def put_result(kind: Kind.Value, text: String)
   1.142 +  private def put_result(kind: String, text: String)
   1.143    {
   1.144      put_result(kind, Nil, List(XML.Text(system.symbols.decode(text))))
   1.145    }
   1.146 @@ -145,13 +111,13 @@
   1.147  
   1.148    def interrupt() = synchronized {
   1.149      if (proc == null) error("Cannot interrupt Isabelle: no process")
   1.150 -    if (pid == null) put_result(Kind.SYSTEM, "Cannot interrupt: unknown pid")
   1.151 +    if (pid == null) put_result(Markup.SYSTEM, "Cannot interrupt: unknown pid")
   1.152      else {
   1.153        try {
   1.154          if (system.execute(true, "kill", "-INT", pid).waitFor == 0)
   1.155 -          put_result(Kind.SIGNAL, "INT")
   1.156 +          put_result(Markup.SIGNAL, "INT")
   1.157          else
   1.158 -          put_result(Kind.SYSTEM, "Cannot interrupt: kill command failed")
   1.159 +          put_result(Markup.SYSTEM, "Cannot interrupt: kill command failed")
   1.160        }
   1.161        catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
   1.162      }
   1.163 @@ -162,7 +128,7 @@
   1.164      else {
   1.165        try_close()
   1.166        Thread.sleep(500)  // FIXME property!?
   1.167 -      put_result(Kind.SIGNAL, "KILL")
   1.168 +      put_result(Markup.SIGNAL, "KILL")
   1.169        proc.destroy
   1.170        proc = null
   1.171        pid = null
   1.172 @@ -222,17 +188,17 @@
   1.173              finished = true
   1.174            }
   1.175            else {
   1.176 -            put_result(Kind.STDIN, s)
   1.177 +            put_result(Markup.STDIN, s)
   1.178              writer.write(s)
   1.179              writer.flush
   1.180            }
   1.181            //}}}
   1.182          }
   1.183          catch {
   1.184 -          case e: IOException => put_result(Kind.SYSTEM, "Stdin thread: " + e.getMessage)
   1.185 +          case e: IOException => put_result(Markup.SYSTEM, "Stdin thread: " + e.getMessage)
   1.186          }
   1.187        }
   1.188 -      put_result(Kind.SYSTEM, "Stdin thread terminated")
   1.189 +      put_result(Markup.SYSTEM, "Stdin thread terminated")
   1.190      }
   1.191    }
   1.192  
   1.193 @@ -256,7 +222,7 @@
   1.194              else done = true
   1.195            }
   1.196            if (result.length > 0) {
   1.197 -            put_result(Kind.STDOUT, result.toString)
   1.198 +            put_result(Markup.STDOUT, result.toString)
   1.199              result.length = 0
   1.200            }
   1.201            else {
   1.202 @@ -267,10 +233,10 @@
   1.203            //}}}
   1.204          }
   1.205          catch {
   1.206 -          case e: IOException => put_result(Kind.SYSTEM, "Stdout thread: " + e.getMessage)
   1.207 +          case e: IOException => put_result(Markup.SYSTEM, "Stdout thread: " + e.getMessage)
   1.208          }
   1.209        }
   1.210 -      put_result(Kind.SYSTEM, "Stdout thread terminated")
   1.211 +      put_result(Markup.SYSTEM, "Stdout thread terminated")
   1.212      }
   1.213    }
   1.214  
   1.215 @@ -332,8 +298,8 @@
   1.216              val body = read_chunk()
   1.217              header match {
   1.218                case List(XML.Elem(name, props, Nil))
   1.219 -                  if name.size == 1 && Kind.code.isDefinedAt(name(0)) =>
   1.220 -                put_result(Kind.code(name(0)), props, body)
   1.221 +                  if name.size == 1 && Kind.markup.isDefinedAt(name(0)) =>
   1.222 +                put_result(Kind.markup(name(0)), props, body)
   1.223                case _ => throw new Protocol_Error("bad header: " + header.toString)
   1.224              }
   1.225            }
   1.226 @@ -341,15 +307,15 @@
   1.227          }
   1.228          catch {
   1.229            case e: IOException =>
   1.230 -            put_result(Kind.SYSTEM, "Cannot read message:\n" + e.getMessage)
   1.231 +            put_result(Markup.SYSTEM, "Cannot read message:\n" + e.getMessage)
   1.232            case e: Protocol_Error =>
   1.233 -            put_result(Kind.SYSTEM, "Malformed message:\n" + e.getMessage)
   1.234 +            put_result(Markup.SYSTEM, "Malformed message:\n" + e.getMessage)
   1.235          }
   1.236        } while (c != -1)
   1.237        stream.close
   1.238        try_close()
   1.239  
   1.240 -      put_result(Kind.SYSTEM, "Message thread terminated")
   1.241 +      put_result(Markup.SYSTEM, "Message thread terminated")
   1.242      }
   1.243    }
   1.244  
   1.245 @@ -392,8 +358,8 @@
   1.246        override def run() = {
   1.247          val rc = proc.waitFor()
   1.248          Thread.sleep(300)  // FIXME property!?
   1.249 -        put_result(Kind.SYSTEM, "Exit thread terminated")
   1.250 -        put_result(Kind.EXIT, rc.toString)
   1.251 +        put_result(Markup.SYSTEM, "Exit thread terminated")
   1.252 +        put_result(Markup.EXIT, rc.toString)
   1.253          rm_fifo()
   1.254        }
   1.255      }.start

     2.1 --- a/src/Pure/System/session.scala	Sat Jul 03 23:24:36 2010 +0200
     2.2 +++ b/src/Pure/System/session.scala	Sun Jul 04 00:05:32 2010 +0200
     2.3 @@ -110,14 +110,14 @@
     2.4      {
     2.5        raw_results.event(result)
     2.6  
     2.7 -      val target_id: Option[Session.Entity_ID] = Position.get_id(result.props)
     2.8 +      val target_id: Option[Session.Entity_ID] = Position.get_id(result.message.attributes)
     2.9        val target: Option[Session.Entity] =
    2.10          target_id match {
    2.11            case None => None
    2.12            case Some(id) => lookup_entity(id)
    2.13          }
    2.14        if (target.isDefined) target.get.consume(result.message, indicate_command_change)
    2.15 -      else if (result.kind == Isabelle_Process.Kind.STATUS) {
    2.16 +      else if (result.is_status) {
    2.17          // global status message
    2.18          result.body match {
    2.19  
    2.20 @@ -145,7 +145,7 @@
    2.21            case _ => if (!result.is_ready) bad_result(result)
    2.22          }
    2.23        }
    2.24 -      else if (result.kind == Isabelle_Process.Kind.EXIT)
    2.25 +      else if (result.kind == Markup.EXIT)
    2.26          prover = null
    2.27        else if (result.is_raw)
    2.28          raw_output.event(result)
    2.29 @@ -176,7 +176,7 @@
    2.30      {
    2.31        receiveWithin(timeout) {
    2.32          case result: Isabelle_Process.Result
    2.33 -          if result.kind == Isabelle_Process.Kind.INIT =>
    2.34 +          if result.kind == Markup.INIT =>
    2.35            while (receive {
    2.36              case result: Isabelle_Process.Result =>
    2.37                handle_result(result); !result.is_ready
    2.38 @@ -184,7 +184,7 @@
    2.39            None
    2.40  
    2.41          case result: Isabelle_Process.Result
    2.42 -          if result.kind == Isabelle_Process.Kind.EXIT =>
    2.43 +          if result.kind == Markup.EXIT =>
    2.44            Some(startup_error())
    2.45  
    2.46          case TIMEOUT =>  // FIXME clarify