simplified Isabelle_Process message kinds;
authorwenzelm
Sun Sep 19 17:12:34 2010 +0200 (2010-09-19 ago)
changeset 3952572e949a0425b
parent 39524 59ebce09ce6e
child 39526 f1296795a8dc
simplified Isabelle_Process message kinds;
misc tuning and simplification;
src/Pure/General/markup.scala
src/Pure/System/isabelle_process.scala
src/Pure/System/session.scala
     1.1 --- a/src/Pure/General/markup.scala	Sat Sep 18 21:33:56 2010 +0200
     1.2 +++ b/src/Pure/General/markup.scala	Sun Sep 19 17:12:34 2010 +0200
     1.3 @@ -235,18 +235,15 @@
     1.4  
     1.5    val INIT = "init"
     1.6    val STATUS = "status"
     1.7 +  val REPORT = "report"
     1.8    val WRITELN = "writeln"
     1.9    val TRACING = "tracing"
    1.10    val WARNING = "warning"
    1.11    val ERROR = "error"
    1.12    val SYSTEM = "system"
    1.13 -  val INPUT = "input"
    1.14 -  val STDIN = "stdin"
    1.15    val STDOUT = "stdout"
    1.16 -  val SIGNAL = "signal"
    1.17    val EXIT = "exit"
    1.18  
    1.19 -  val REPORT = "report"
    1.20    val NO_REPORT = "no_report"
    1.21  
    1.22    val BAD = "bad"
     2.1 --- a/src/Pure/System/isabelle_process.scala	Sat Sep 18 21:33:56 2010 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.scala	Sun Sep 19 17:12:34 2010 +0200
     2.3 @@ -19,9 +19,9 @@
     2.4  {
     2.5    /* results */
     2.6  
     2.7 -  object Kind {
     2.8 -    // message markup
     2.9 -    val markup = Map(
    2.10 +  object Kind
    2.11 +  {
    2.12 +    val message_markup = Map(
    2.13        ('A' : Int) -> Markup.INIT,
    2.14        ('B' : Int) -> Markup.STATUS,
    2.15        ('C' : Int) -> Markup.REPORT,
    2.16 @@ -29,19 +29,6 @@
    2.17        ('E' : Int) -> Markup.TRACING,
    2.18        ('F' : Int) -> Markup.WARNING,
    2.19        ('G' : Int) -> Markup.ERROR)
    2.20 -    def is_raw(kind: String) =
    2.21 -      kind == Markup.STDOUT
    2.22 -    def is_control(kind: String) =
    2.23 -      kind == Markup.SYSTEM ||
    2.24 -      kind == Markup.SIGNAL ||
    2.25 -      kind == Markup.EXIT
    2.26 -    def is_system(kind: String) =
    2.27 -      kind == Markup.SYSTEM ||
    2.28 -      kind == Markup.INPUT ||
    2.29 -      kind == Markup.STDIN ||
    2.30 -      kind == Markup.SIGNAL ||
    2.31 -      kind == Markup.EXIT ||
    2.32 -      kind == Markup.STATUS
    2.33    }
    2.34  
    2.35    class Result(val message: XML.Elem)
    2.36 @@ -50,9 +37,10 @@
    2.37      def properties = message.markup.properties
    2.38      def body = message.body
    2.39  
    2.40 -    def is_raw = Kind.is_raw(kind)
    2.41 -    def is_control = Kind.is_control(kind)
    2.42 -    def is_system = Kind.is_system(kind)
    2.43 +    def is_init = kind == Markup.INIT
    2.44 +    def is_exit = kind == Markup.EXIT
    2.45 +    def is_stdout = kind == Markup.STDOUT
    2.46 +    def is_system = kind == Markup.SYSTEM
    2.47      def is_status = kind == Markup.STATUS
    2.48      def is_report = kind == Markup.REPORT
    2.49      def is_ready = is_status && body == List(XML.Elem(Markup.Ready, Nil))
    2.50 @@ -92,12 +80,22 @@
    2.51  
    2.52    /* results */
    2.53  
    2.54 +  private def system_result(text: String)
    2.55 +  {
    2.56 +    receiver ! new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))
    2.57 +  }
    2.58 +
    2.59 +
    2.60    private val xml_cache = new XML.Cache(131071)
    2.61  
    2.62    private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
    2.63    {
    2.64 -    if (pid.isEmpty && kind == Markup.INIT)
    2.65 -      pid = props.find(_._1 == Markup.PID).map(_._1)
    2.66 +    if (pid.isEmpty && kind == Markup.INIT) {
    2.67 +      props.find(_._1 == Markup.PID).map(_._1) match {
    2.68 +        case None => system_result("Bad Isabelle process initialization: missing pid")
    2.69 +        case p => pid = p
    2.70 +      }
    2.71 +    }
    2.72  
    2.73      val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
    2.74      xml_cache.cache_tree(msg)((message: XML.Tree) =>
    2.75 @@ -114,16 +112,16 @@
    2.76  
    2.77    def interrupt()
    2.78    {
    2.79 -    if (proc.isEmpty) put_result(Markup.SYSTEM, "Cannot interrupt Isabelle: no process")
    2.80 +    if (proc.isEmpty) system_result("Cannot interrupt Isabelle: no process")
    2.81      else
    2.82        pid match {
    2.83 -        case None => put_result(Markup.SYSTEM, "Cannot interrupt Isabelle: unknowd pid")
    2.84 +        case None => system_result("Cannot interrupt Isabelle: unknowd pid")
    2.85          case Some(i) =>
    2.86            try {
    2.87              if (system.execute(true, "kill", "-INT", i).waitFor == 0)
    2.88 -              put_result(Markup.SIGNAL, "INT")
    2.89 +              system_result("Interrupt Isabelle")
    2.90              else
    2.91 -              put_result(Markup.SYSTEM, "Cannot interrupt Isabelle: kill command failed")
    2.92 +              system_result("Cannot interrupt Isabelle: kill command failed")
    2.93            }
    2.94            catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
    2.95        }
    2.96 @@ -132,11 +130,11 @@
    2.97    def kill()
    2.98    {
    2.99      proc match {
   2.100 -      case None => put_result(Markup.SYSTEM, "Cannot kill Isabelle: no process")
   2.101 +      case None => system_result("Cannot kill Isabelle: no process")
   2.102        case Some(p) =>
   2.103          close()
   2.104          Thread.sleep(500)  // FIXME !?
   2.105 -        put_result(Markup.SIGNAL, "KILL")
   2.106 +        system_result("Kill Isabelle")
   2.107          p.destroy
   2.108          proc = None
   2.109          pid = None
   2.110 @@ -172,11 +170,9 @@
   2.111            }
   2.112            //}}}
   2.113          }
   2.114 -        catch {
   2.115 -          case e: IOException => put_result(Markup.SYSTEM, name + ": " + e.getMessage)
   2.116 -        }
   2.117 +        catch { case e: IOException => system_result(name + ": " + e.getMessage) }
   2.118        }
   2.119 -      put_result(Markup.SYSTEM, name + " terminated")
   2.120 +      system_result(name + " terminated")
   2.121      }
   2.122  
   2.123  
   2.124 @@ -209,11 +205,9 @@
   2.125            }
   2.126            //}}}
   2.127          }
   2.128 -        catch {
   2.129 -          case e: IOException => put_result(Markup.SYSTEM, name + ": " + e.getMessage)
   2.130 -        }
   2.131 +        catch { case e: IOException => system_result(name + ": " + e.getMessage) }
   2.132        }
   2.133 -      put_result(Markup.SYSTEM, name + " terminated")
   2.134 +      system_result(name + " terminated")
   2.135      }
   2.136  
   2.137  
   2.138 @@ -239,11 +233,9 @@
   2.139            }
   2.140            //}}}
   2.141          }
   2.142 -        catch {
   2.143 -          case e: IOException => put_result(Markup.SYSTEM, name + ": " + e.getMessage)
   2.144 -        }
   2.145 +        catch { case e: IOException => system_result(name + ": " + e.getMessage) }
   2.146        }
   2.147 -      put_result(Markup.SYSTEM, name + " terminated")
   2.148 +      system_result(name + " terminated")
   2.149      }
   2.150  
   2.151  
   2.152 @@ -293,22 +285,20 @@
   2.153            val body = read_chunk()
   2.154            header match {
   2.155              case List(XML.Elem(Markup(name, props), Nil))
   2.156 -                if name.size == 1 && Kind.markup.isDefinedAt(name(0)) =>
   2.157 -              put_result(Kind.markup(name(0)), props, body)
   2.158 +                if name.size == 1 && Kind.message_markup.isDefinedAt(name(0)) =>
   2.159 +              put_result(Kind.message_markup(name(0)), props, body)
   2.160              case _ => throw new Protocol_Error("bad header: " + header.toString)
   2.161            }
   2.162          }
   2.163          catch {
   2.164 -          case e: IOException =>
   2.165 -            put_result(Markup.SYSTEM, "Cannot read message:\n" + e.getMessage)
   2.166 -          case e: Protocol_Error =>
   2.167 -            put_result(Markup.SYSTEM, "Malformed message:\n" + e.getMessage)
   2.168 +          case e: IOException => system_result("Cannot read message:\n" + e.getMessage)
   2.169 +          case e: Protocol_Error => system_result("Malformed message:\n" + e.getMessage)
   2.170          }
   2.171        } while (c != -1)
   2.172        stream.close
   2.173        close()
   2.174  
   2.175 -      put_result(Markup.SYSTEM, name + " terminated")
   2.176 +      system_result(name + " terminated")
   2.177      }
   2.178  
   2.179  
   2.180 @@ -346,7 +336,7 @@
   2.181        case Some(p) =>
   2.182          val rc = p.waitFor()
   2.183          Thread.sleep(300)  // FIXME property!?
   2.184 -        put_result(Markup.SYSTEM, "Isabelle process terminated")
   2.185 +        system_result("Isabelle process terminated")
   2.186          put_result(Markup.EXIT, rc.toString)
   2.187      }
   2.188      rm_fifos()
     3.1 --- a/src/Pure/System/session.scala	Sat Sep 18 21:33:56 2010 +0200
     3.2 +++ b/src/Pure/System/session.scala	Sun Sep 19 17:12:34 2010 +0200
     3.3 @@ -200,8 +200,8 @@
     3.4                case _ => if (!result.is_ready) bad_result(result)
     3.5              }
     3.6            }
     3.7 -          else if (result.kind == Markup.EXIT) prover = null
     3.8 -          else if (result.is_raw) raw_output.event(result)
     3.9 +          else if (result.is_exit) prover = null  // FIXME ??
    3.10 +          else if (result.is_stdout) raw_output.event(result)
    3.11            else if (!result.is_system) bad_result(result)  // FIXME syslog for system messages (!?)
    3.12          }
    3.13      }
    3.14 @@ -216,7 +216,7 @@
    3.15        while (
    3.16          receiveWithin(0) {
    3.17            case result: Isabelle_Process.Result =>
    3.18 -            if (result.is_raw) {
    3.19 +            if (result.is_stdout) {
    3.20                for (text <- XML.content(result.message))
    3.21                  buf.append(text)
    3.22              }
    3.23 @@ -229,16 +229,14 @@
    3.24      def prover_startup(timeout: Int): Option[String] =
    3.25      {
    3.26        receiveWithin(timeout) {
    3.27 -        case result: Isabelle_Process.Result
    3.28 -          if result.kind == Markup.INIT =>
    3.29 +        case result: Isabelle_Process.Result if result.is_init =>
    3.30            while (receive {
    3.31              case result: Isabelle_Process.Result =>
    3.32                handle_result(result); !result.is_ready
    3.33              }) {}
    3.34            None
    3.35  
    3.36 -        case result: Isabelle_Process.Result
    3.37 -          if result.kind == Markup.EXIT =>
    3.38 +        case result: Isabelle_Process.Result if result.is_exit =>
    3.39            Some(startup_error())
    3.40  
    3.41          case TIMEOUT =>  // FIXME clarify