src/Pure/System/isabelle_process.scala
changeset 39525 72e949a0425b
parent 39524 59ebce09ce6e
child 39526 f1296795a8dc
     1.1 --- a/src/Pure/System/isabelle_process.scala	Sat Sep 18 21:33:56 2010 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Sun Sep 19 17:12:34 2010 +0200
     1.3 @@ -19,9 +19,9 @@
     1.4  {
     1.5    /* results */
     1.6  
     1.7 -  object Kind {
     1.8 -    // message markup
     1.9 -    val markup = Map(
    1.10 +  object Kind
    1.11 +  {
    1.12 +    val message_markup = Map(
    1.13        ('A' : Int) -> Markup.INIT,
    1.14        ('B' : Int) -> Markup.STATUS,
    1.15        ('C' : Int) -> Markup.REPORT,
    1.16 @@ -29,19 +29,6 @@
    1.17        ('E' : Int) -> Markup.TRACING,
    1.18        ('F' : Int) -> Markup.WARNING,
    1.19        ('G' : Int) -> Markup.ERROR)
    1.20 -    def is_raw(kind: String) =
    1.21 -      kind == Markup.STDOUT
    1.22 -    def is_control(kind: String) =
    1.23 -      kind == Markup.SYSTEM ||
    1.24 -      kind == Markup.SIGNAL ||
    1.25 -      kind == Markup.EXIT
    1.26 -    def is_system(kind: String) =
    1.27 -      kind == Markup.SYSTEM ||
    1.28 -      kind == Markup.INPUT ||
    1.29 -      kind == Markup.STDIN ||
    1.30 -      kind == Markup.SIGNAL ||
    1.31 -      kind == Markup.EXIT ||
    1.32 -      kind == Markup.STATUS
    1.33    }
    1.34  
    1.35    class Result(val message: XML.Elem)
    1.36 @@ -50,9 +37,10 @@
    1.37      def properties = message.markup.properties
    1.38      def body = message.body
    1.39  
    1.40 -    def is_raw = Kind.is_raw(kind)
    1.41 -    def is_control = Kind.is_control(kind)
    1.42 -    def is_system = Kind.is_system(kind)
    1.43 +    def is_init = kind == Markup.INIT
    1.44 +    def is_exit = kind == Markup.EXIT
    1.45 +    def is_stdout = kind == Markup.STDOUT
    1.46 +    def is_system = kind == Markup.SYSTEM
    1.47      def is_status = kind == Markup.STATUS
    1.48      def is_report = kind == Markup.REPORT
    1.49      def is_ready = is_status && body == List(XML.Elem(Markup.Ready, Nil))
    1.50 @@ -92,12 +80,22 @@
    1.51  
    1.52    /* results */
    1.53  
    1.54 +  private def system_result(text: String)
    1.55 +  {
    1.56 +    receiver ! new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))
    1.57 +  }
    1.58 +
    1.59 +
    1.60    private val xml_cache = new XML.Cache(131071)
    1.61  
    1.62    private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
    1.63    {
    1.64 -    if (pid.isEmpty && kind == Markup.INIT)
    1.65 -      pid = props.find(_._1 == Markup.PID).map(_._1)
    1.66 +    if (pid.isEmpty && kind == Markup.INIT) {
    1.67 +      props.find(_._1 == Markup.PID).map(_._1) match {
    1.68 +        case None => system_result("Bad Isabelle process initialization: missing pid")
    1.69 +        case p => pid = p
    1.70 +      }
    1.71 +    }
    1.72  
    1.73      val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
    1.74      xml_cache.cache_tree(msg)((message: XML.Tree) =>
    1.75 @@ -114,16 +112,16 @@
    1.76  
    1.77    def interrupt()
    1.78    {
    1.79 -    if (proc.isEmpty) put_result(Markup.SYSTEM, "Cannot interrupt Isabelle: no process")
    1.80 +    if (proc.isEmpty) system_result("Cannot interrupt Isabelle: no process")
    1.81      else
    1.82        pid match {
    1.83 -        case None => put_result(Markup.SYSTEM, "Cannot interrupt Isabelle: unknowd pid")
    1.84 +        case None => system_result("Cannot interrupt Isabelle: unknowd pid")
    1.85          case Some(i) =>
    1.86            try {
    1.87              if (system.execute(true, "kill", "-INT", i).waitFor == 0)
    1.88 -              put_result(Markup.SIGNAL, "INT")
    1.89 +              system_result("Interrupt Isabelle")
    1.90              else
    1.91 -              put_result(Markup.SYSTEM, "Cannot interrupt Isabelle: kill command failed")
    1.92 +              system_result("Cannot interrupt Isabelle: kill command failed")
    1.93            }
    1.94            catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
    1.95        }
    1.96 @@ -132,11 +130,11 @@
    1.97    def kill()
    1.98    {
    1.99      proc match {
   1.100 -      case None => put_result(Markup.SYSTEM, "Cannot kill Isabelle: no process")
   1.101 +      case None => system_result("Cannot kill Isabelle: no process")
   1.102        case Some(p) =>
   1.103          close()
   1.104          Thread.sleep(500)  // FIXME !?
   1.105 -        put_result(Markup.SIGNAL, "KILL")
   1.106 +        system_result("Kill Isabelle")
   1.107          p.destroy
   1.108          proc = None
   1.109          pid = None
   1.110 @@ -172,11 +170,9 @@
   1.111            }
   1.112            //}}}
   1.113          }
   1.114 -        catch {
   1.115 -          case e: IOException => put_result(Markup.SYSTEM, name + ": " + e.getMessage)
   1.116 -        }
   1.117 +        catch { case e: IOException => system_result(name + ": " + e.getMessage) }
   1.118        }
   1.119 -      put_result(Markup.SYSTEM, name + " terminated")
   1.120 +      system_result(name + " terminated")
   1.121      }
   1.122  
   1.123  
   1.124 @@ -209,11 +205,9 @@
   1.125            }
   1.126            //}}}
   1.127          }
   1.128 -        catch {
   1.129 -          case e: IOException => put_result(Markup.SYSTEM, name + ": " + e.getMessage)
   1.130 -        }
   1.131 +        catch { case e: IOException => system_result(name + ": " + e.getMessage) }
   1.132        }
   1.133 -      put_result(Markup.SYSTEM, name + " terminated")
   1.134 +      system_result(name + " terminated")
   1.135      }
   1.136  
   1.137  
   1.138 @@ -239,11 +233,9 @@
   1.139            }
   1.140            //}}}
   1.141          }
   1.142 -        catch {
   1.143 -          case e: IOException => put_result(Markup.SYSTEM, name + ": " + e.getMessage)
   1.144 -        }
   1.145 +        catch { case e: IOException => system_result(name + ": " + e.getMessage) }
   1.146        }
   1.147 -      put_result(Markup.SYSTEM, name + " terminated")
   1.148 +      system_result(name + " terminated")
   1.149      }
   1.150  
   1.151  
   1.152 @@ -293,22 +285,20 @@
   1.153            val body = read_chunk()
   1.154            header match {
   1.155              case List(XML.Elem(Markup(name, props), Nil))
   1.156 -                if name.size == 1 && Kind.markup.isDefinedAt(name(0)) =>
   1.157 -              put_result(Kind.markup(name(0)), props, body)
   1.158 +                if name.size == 1 && Kind.message_markup.isDefinedAt(name(0)) =>
   1.159 +              put_result(Kind.message_markup(name(0)), props, body)
   1.160              case _ => throw new Protocol_Error("bad header: " + header.toString)
   1.161            }
   1.162          }
   1.163          catch {
   1.164 -          case e: IOException =>
   1.165 -            put_result(Markup.SYSTEM, "Cannot read message:\n" + e.getMessage)
   1.166 -          case e: Protocol_Error =>
   1.167 -            put_result(Markup.SYSTEM, "Malformed message:\n" + e.getMessage)
   1.168 +          case e: IOException => system_result("Cannot read message:\n" + e.getMessage)
   1.169 +          case e: Protocol_Error => system_result("Malformed message:\n" + e.getMessage)
   1.170          }
   1.171        } while (c != -1)
   1.172        stream.close
   1.173        close()
   1.174  
   1.175 -      put_result(Markup.SYSTEM, name + " terminated")
   1.176 +      system_result(name + " terminated")
   1.177      }
   1.178  
   1.179  
   1.180 @@ -346,7 +336,7 @@
   1.181        case Some(p) =>
   1.182          val rc = p.waitFor()
   1.183          Thread.sleep(300)  // FIXME property!?
   1.184 -        put_result(Markup.SYSTEM, "Isabelle process terminated")
   1.185 +        system_result("Isabelle process terminated")
   1.186          put_result(Markup.EXIT, rc.toString)
   1.187      }
   1.188      rm_fifos()