src/Pure/System/isabelle_process.scala
changeset 45666 d83797ef0d2d
parent 45633 2cb7e34f6096
child 45672 a497c5d4a523
     1.1 --- a/src/Pure/System/isabelle_process.scala	Mon Nov 28 20:39:08 2011 +0100
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Mon Nov 28 22:05:32 2011 +0100
     1.3 @@ -23,14 +23,14 @@
     1.4    object Kind
     1.5    {
     1.6      val message_markup = Map(
     1.7 -      ('A' : Int) -> Markup.INIT,
     1.8 -      ('B' : Int) -> Markup.STATUS,
     1.9 -      ('C' : Int) -> Markup.REPORT,
    1.10 -      ('D' : Int) -> Markup.WRITELN,
    1.11 -      ('E' : Int) -> Markup.TRACING,
    1.12 -      ('F' : Int) -> Markup.WARNING,
    1.13 -      ('G' : Int) -> Markup.ERROR,
    1.14 -      ('H' : Int) -> Markup.RAW)
    1.15 +      ('A' : Int) -> Isabelle_Markup.INIT,
    1.16 +      ('B' : Int) -> Isabelle_Markup.STATUS,
    1.17 +      ('C' : Int) -> Isabelle_Markup.REPORT,
    1.18 +      ('D' : Int) -> Isabelle_Markup.WRITELN,
    1.19 +      ('E' : Int) -> Isabelle_Markup.TRACING,
    1.20 +      ('F' : Int) -> Isabelle_Markup.WARNING,
    1.21 +      ('G' : Int) -> Isabelle_Markup.ERROR,
    1.22 +      ('H' : Int) -> Isabelle_Markup.RAW)
    1.23    }
    1.24  
    1.25    sealed abstract class Message
    1.26 @@ -38,9 +38,10 @@
    1.27    class Input(name: String, args: List[String]) extends Message
    1.28    {
    1.29      override def toString: String =
    1.30 -      XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
    1.31 +      XML.Elem(Markup(Isabelle_Markup.PROVER_COMMAND, List((Markup.NAME, name))),
    1.32          args.map(s =>
    1.33 -          List(XML.Text("\n"), XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
    1.34 +          List(XML.Text("\n"),
    1.35 +            XML.elem(Isabelle_Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
    1.36    }
    1.37  
    1.38    class Result(val message: XML.Elem) extends Message
    1.39 @@ -49,14 +50,14 @@
    1.40      def properties: Properties.T = message.markup.properties
    1.41      def body: XML.Body = message.body
    1.42  
    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_stderr = kind == Markup.STDERR
    1.47 -    def is_system = kind == Markup.SYSTEM
    1.48 -    def is_status = kind == Markup.STATUS
    1.49 -    def is_report = kind == Markup.REPORT
    1.50 -    def is_raw = kind == Markup.RAW
    1.51 +    def is_init = kind == Isabelle_Markup.INIT
    1.52 +    def is_exit = kind == Isabelle_Markup.EXIT
    1.53 +    def is_stdout = kind == Isabelle_Markup.STDOUT
    1.54 +    def is_stderr = kind == Isabelle_Markup.STDERR
    1.55 +    def is_system = kind == Isabelle_Markup.SYSTEM
    1.56 +    def is_status = kind == Isabelle_Markup.STATUS
    1.57 +    def is_report = kind == Isabelle_Markup.REPORT
    1.58 +    def is_raw = kind == Isabelle_Markup.RAW
    1.59      def is_ready = Isar_Document.is_ready(message)
    1.60      def is_syslog = is_init || is_exit || is_system || is_ready || is_stderr
    1.61  
    1.62 @@ -88,15 +89,15 @@
    1.63  
    1.64    private def system_result(text: String)
    1.65    {
    1.66 -    receiver(new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
    1.67 +    receiver(new Result(XML.Elem(Markup(Isabelle_Markup.SYSTEM, Nil), List(XML.Text(text)))))
    1.68    }
    1.69  
    1.70    private val xml_cache = new XML.Cache()
    1.71  
    1.72    private def put_result(kind: String, props: Properties.T, body: XML.Body)
    1.73    {
    1.74 -    if (kind == Markup.INIT) system_channel.accepted()
    1.75 -    if (kind == Markup.RAW)
    1.76 +    if (kind == Isabelle_Markup.INIT) system_channel.accepted()
    1.77 +    if (kind == Isabelle_Markup.RAW)
    1.78        receiver(new Result(XML.Elem(Markup(kind, props), body)))
    1.79      else {
    1.80        val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
    1.81 @@ -172,7 +173,7 @@
    1.82      system_result(startup_output)
    1.83  
    1.84      if (startup_failed) {
    1.85 -      put_result(Markup.EXIT, "Return code: 127")
    1.86 +      put_result(Isabelle_Markup.EXIT, "Return code: 127")
    1.87        process.stdin.close
    1.88        Thread.sleep(300)
    1.89        terminate_process()
    1.90 @@ -192,7 +193,7 @@
    1.91        for ((thread, _) <- List(standard_input, stdout, stderr, command_input, message))
    1.92          thread.join
    1.93        system_result("process_manager terminated")
    1.94 -      put_result(Markup.EXIT, "Return code: " + rc.toString)
    1.95 +      put_result(Isabelle_Markup.EXIT, "Return code: " + rc.toString)
    1.96      }
    1.97      system_channel.accepted()
    1.98    }
    1.99 @@ -246,8 +247,8 @@
   1.100    private def raw_output_actor(err: Boolean): (Thread, Actor) =
   1.101    {
   1.102      val (name, reader, markup) =
   1.103 -      if (err) ("standard_error", process.stderr, Markup.STDERR)
   1.104 -      else ("standard_output", process.stdout, Markup.STDOUT)
   1.105 +      if (err) ("standard_error", process.stderr, Isabelle_Markup.STDERR)
   1.106 +      else ("standard_output", process.stdout, Isabelle_Markup.STDOUT)
   1.107  
   1.108      Simple_Thread.actor(name) {
   1.109        var result = new StringBuilder(100)
   1.110 @@ -363,7 +364,7 @@
   1.111              case List(XML.Elem(Markup(name, props), Nil))
   1.112                  if name.size == 1 && Kind.message_markup.isDefinedAt(name(0)) =>
   1.113                val kind = Kind.message_markup(name(0))
   1.114 -              val body = read_chunk(kind != Markup.RAW)
   1.115 +              val body = read_chunk(kind != Isabelle_Markup.RAW)
   1.116                put_result(kind, props, body)
   1.117              case _ =>
   1.118                read_chunk(false)