tuned signature -- emphasize Isabelle_Process Input vs. Output;
authorwenzelm
Sat Mar 03 17:30:14 2012 +0100 (2012-03-03)
changeset 46772be21f050eda4
parent 46771 06a9b24c4a36
child 46773 94259b352ed3
tuned signature -- emphasize Isabelle_Process Input vs. Output;
src/Pure/System/isabelle_process.scala
src/Pure/System/session.scala
src/Tools/jEdit/src/protocol_dockable.scala
src/Tools/jEdit/src/raw_output_dockable.scala
src/Tools/jEdit/src/session_dockable.scala
     1.1 --- a/src/Pure/System/isabelle_process.scala	Sat Mar 03 16:59:30 2012 +0100
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Sat Mar 03 17:30:14 2012 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4  
     1.5  object Isabelle_Process
     1.6  {
     1.7 -  /* results */
     1.8 +  /* messages */
     1.9  
    1.10    object Kind
    1.11    {
    1.12 @@ -44,7 +44,7 @@
    1.13              XML.elem(Isabelle_Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
    1.14    }
    1.15  
    1.16 -  class Result(val message: XML.Elem) extends Message
    1.17 +  class Output(val message: XML.Elem) extends Message
    1.18    {
    1.19      def kind: String = message.markup.name
    1.20      def properties: Properties.T = message.markup.properties
    1.21 @@ -84,29 +84,29 @@
    1.22    import Isabelle_Process._
    1.23  
    1.24  
    1.25 -  /* results */
    1.26 +  /* output */
    1.27  
    1.28 -  private def system_result(text: String)
    1.29 +  private def system_output(text: String)
    1.30    {
    1.31 -    receiver(new Result(XML.Elem(Markup(Isabelle_Markup.SYSTEM, Nil), List(XML.Text(text)))))
    1.32 +    receiver(new Output(XML.Elem(Markup(Isabelle_Markup.SYSTEM, Nil), List(XML.Text(text)))))
    1.33    }
    1.34  
    1.35    private val xml_cache = new XML.Cache()
    1.36  
    1.37 -  private def put_result(kind: String, props: Properties.T, body: XML.Body)
    1.38 +  private def output_message(kind: String, props: Properties.T, body: XML.Body)
    1.39    {
    1.40      if (kind == Isabelle_Markup.INIT) system_channel.accepted()
    1.41      if (kind == Isabelle_Markup.RAW)
    1.42 -      receiver(new Result(XML.Elem(Markup(kind, props), body)))
    1.43 +      receiver(new Output(XML.Elem(Markup(kind, props), body)))
    1.44      else {
    1.45        val msg = XML.Elem(Markup(kind, props), Protocol.clean_message(body))
    1.46 -      receiver(new Result(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem]))
    1.47 +      receiver(new Output(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem]))
    1.48      }
    1.49    }
    1.50  
    1.51 -  private def put_result(kind: String, text: String)
    1.52 +  private def output_message(kind: String, text: String)
    1.53    {
    1.54 -    put_result(kind, Nil, List(XML.Text(Symbol.decode(text))))
    1.55 +    output_message(kind, Nil, List(XML.Text(Symbol.decode(text))))
    1.56    }
    1.57  
    1.58  
    1.59 @@ -147,7 +147,7 @@
    1.60    private def terminate_process()
    1.61    {
    1.62      try { process.terminate }
    1.63 -    catch { case e: IOException => system_result("Failed to terminate Isabelle: " + e.getMessage) }
    1.64 +    catch { case e: IOException => system_output("Failed to terminate Isabelle: " + e.getMessage) }
    1.65    }
    1.66  
    1.67    private val process_manager = Simple_Thread.fork("process_manager")
    1.68 @@ -169,10 +169,10 @@
    1.69        }
    1.70        (finished.isEmpty || !finished.get, result.toString.trim)
    1.71      }
    1.72 -    if (startup_errors != "") system_result(startup_errors)
    1.73 +    if (startup_errors != "") system_output(startup_errors)
    1.74  
    1.75      if (startup_failed) {
    1.76 -      put_result(Isabelle_Markup.EXIT, "Return code: 127")
    1.77 +      output_message(Isabelle_Markup.EXIT, "Return code: 127")
    1.78        process.stdin.close
    1.79        Thread.sleep(300)
    1.80        terminate_process()
    1.81 @@ -188,11 +188,11 @@
    1.82        val message = message_actor(message_stream)
    1.83  
    1.84        val rc = process_result.join
    1.85 -      system_result("process terminated")
    1.86 +      system_output("process terminated")
    1.87        for ((thread, _) <- List(standard_input, stdout, stderr, command_input, message))
    1.88          thread.join
    1.89 -      system_result("process_manager terminated")
    1.90 -      put_result(Isabelle_Markup.EXIT, "Return code: " + rc.toString)
    1.91 +      system_output("process_manager terminated")
    1.92 +      output_message(Isabelle_Markup.EXIT, "Return code: " + rc.toString)
    1.93      }
    1.94      system_channel.accepted()
    1.95    }
    1.96 @@ -205,7 +205,7 @@
    1.97    def terminate()
    1.98    {
    1.99      close()
   1.100 -    system_result("Terminating Isabelle process")
   1.101 +    system_output("Terminating Isabelle process")
   1.102      terminate_process()
   1.103    }
   1.104  
   1.105 @@ -235,8 +235,8 @@
   1.106            //}}}
   1.107          }
   1.108        }
   1.109 -      catch { case e: IOException => system_result(name + ": " + e.getMessage) }
   1.110 -      system_result(name + " terminated")
   1.111 +      catch { case e: IOException => system_output(name + ": " + e.getMessage) }
   1.112 +      system_output(name + " terminated")
   1.113      }
   1.114    }
   1.115  
   1.116 @@ -263,7 +263,7 @@
   1.117              else done = true
   1.118            }
   1.119            if (result.length > 0) {
   1.120 -            put_result(markup, result.toString)
   1.121 +            output_message(markup, result.toString)
   1.122              result.length = 0
   1.123            }
   1.124            else {
   1.125 @@ -273,8 +273,8 @@
   1.126            //}}}
   1.127          }
   1.128        }
   1.129 -      catch { case e: IOException => system_result(name + ": " + e.getMessage) }
   1.130 -      system_result(name + " terminated")
   1.131 +      catch { case e: IOException => system_output(name + ": " + e.getMessage) }
   1.132 +      system_output(name + " terminated")
   1.133      }
   1.134    }
   1.135  
   1.136 @@ -304,8 +304,8 @@
   1.137            //}}}
   1.138          }
   1.139        }
   1.140 -      catch { case e: IOException => system_result(name + ": " + e.getMessage) }
   1.141 -      system_result(name + " terminated")
   1.142 +      catch { case e: IOException => system_output(name + ": " + e.getMessage) }
   1.143 +      system_output(name + " terminated")
   1.144      }
   1.145    }
   1.146  
   1.147 @@ -365,7 +365,7 @@
   1.148                    if name.size == 1 && Kind.message_markup.isDefinedAt(name(0)) =>
   1.149                  val kind = Kind.message_markup(name(0))
   1.150                  val body = read_chunk(kind != Isabelle_Markup.RAW)
   1.151 -                put_result(kind, props, body)
   1.152 +                output_message(kind, props, body)
   1.153                case _ =>
   1.154                  read_chunk(false)
   1.155                  throw new Protocol_Error("bad header: " + header.toString)
   1.156 @@ -376,12 +376,12 @@
   1.157          } while (c != -1)
   1.158        }
   1.159        catch {
   1.160 -        case e: IOException => system_result("Cannot read message:\n" + e.getMessage)
   1.161 -        case e: Protocol_Error => system_result("Malformed message:\n" + e.getMessage)
   1.162 +        case e: IOException => system_output("Cannot read message:\n" + e.getMessage)
   1.163 +        case e: Protocol_Error => system_output("Malformed message:\n" + e.getMessage)
   1.164        }
   1.165        stream.close
   1.166  
   1.167 -      system_result(name + " terminated")
   1.168 +      system_output(name + " terminated")
   1.169      }
   1.170    }
   1.171  
     2.1 --- a/src/Pure/System/session.scala	Sat Mar 03 16:59:30 2012 +0100
     2.2 +++ b/src/Pure/System/session.scala	Sat Mar 03 17:30:14 2012 +0100
     2.3 @@ -56,8 +56,8 @@
     2.4    val caret_focus = new Event_Bus[Session.Caret_Focus.type]
     2.5    val commands_changed = new Event_Bus[Session.Commands_Changed]
     2.6    val phase_changed = new Event_Bus[Session.Phase]
     2.7 -  val syslog_messages = new Event_Bus[Isabelle_Process.Result]
     2.8 -  val raw_output_messages = new Event_Bus[Isabelle_Process.Result]
     2.9 +  val syslog_messages = new Event_Bus[Isabelle_Process.Output]
    2.10 +  val raw_output_messages = new Event_Bus[Isabelle_Process.Output]
    2.11    val protocol_messages = new Event_Bus[Isabelle_Process.Message]  // potential bottle-neck
    2.12  
    2.13  
    2.14 @@ -193,14 +193,14 @@
    2.15        def invoke(msg: Isabelle_Process.Message): Unit = synchronized {
    2.16          buffer += msg
    2.17          msg match {
    2.18 -          case result: Isabelle_Process.Result =>
    2.19 -            if (result.is_syslog)
    2.20 +          case output: Isabelle_Process.Output =>
    2.21 +            if (output.is_syslog)
    2.22                syslog >> (queue =>
    2.23                  {
    2.24 -                  val queue1 = queue.enqueue(result.message)
    2.25 +                  val queue1 = queue.enqueue(output.message)
    2.26                    if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
    2.27                  })
    2.28 -            if (result.is_raw) flush()
    2.29 +            if (output.is_raw) flush()
    2.30            case _ =>
    2.31          }
    2.32        }
    2.33 @@ -343,34 +343,34 @@
    2.34      //}}}
    2.35  
    2.36  
    2.37 -    /* prover results */
    2.38 +    /* prover output */
    2.39  
    2.40 -    def handle_result(result: Isabelle_Process.Result)
    2.41 +    def handle_output(output: Isabelle_Process.Output)
    2.42      //{{{
    2.43      {
    2.44 -      def bad_result(result: Isabelle_Process.Result)
    2.45 +      def bad_output(output: Isabelle_Process.Output)
    2.46        {
    2.47          if (verbose)
    2.48 -          System.err.println("Ignoring prover result: " + result.message.toString)
    2.49 +          System.err.println("Ignoring prover output: " + output.message.toString)
    2.50        }
    2.51  
    2.52 -      result.properties match {
    2.53 +      output.properties match {
    2.54  
    2.55 -        case Position.Id(state_id) if !result.is_raw =>
    2.56 +        case Position.Id(state_id) if !output.is_raw =>
    2.57            try {
    2.58 -            val st = global_state >>> (_.accumulate(state_id, result.message))
    2.59 +            val st = global_state >>> (_.accumulate(state_id, output.message))
    2.60              delay_commands_changed.invoke(st.command)
    2.61            }
    2.62            catch {
    2.63 -            case _: Document.State.Fail => bad_result(result)
    2.64 +            case _: Document.State.Fail => bad_output(output)
    2.65            }
    2.66  
    2.67 -        case Isabelle_Markup.Assign_Execs if result.is_raw =>
    2.68 -          XML.content(result.body).mkString match {
    2.69 +        case Isabelle_Markup.Assign_Execs if output.is_raw =>
    2.70 +          XML.content(output.body).mkString match {
    2.71              case Protocol.Assign(id, assign) =>
    2.72                try { handle_assign(id, assign) }
    2.73 -              catch { case _: Document.State.Fail => bad_result(result) }
    2.74 -            case _ => bad_result(result)
    2.75 +              catch { case _: Document.State.Fail => bad_output(output) }
    2.76 +            case _ => bad_output(output)
    2.77            }
    2.78            // FIXME separate timeout event/message!?
    2.79            if (prover.isDefined && System.currentTimeMillis() > prune_next) {
    2.80 @@ -379,44 +379,44 @@
    2.81              prune_next = System.currentTimeMillis() + prune_delay.ms
    2.82            }
    2.83  
    2.84 -        case Isabelle_Markup.Removed_Versions if result.is_raw =>
    2.85 -          XML.content(result.body).mkString match {
    2.86 +        case Isabelle_Markup.Removed_Versions if output.is_raw =>
    2.87 +          XML.content(output.body).mkString match {
    2.88              case Protocol.Removed(removed) =>
    2.89                try { handle_removed(removed) }
    2.90 -              catch { case _: Document.State.Fail => bad_result(result) }
    2.91 -            case _ => bad_result(result)
    2.92 +              catch { case _: Document.State.Fail => bad_output(output) }
    2.93 +            case _ => bad_output(output)
    2.94            }
    2.95  
    2.96 -        case Isabelle_Markup.Invoke_Scala(name, id) if result.is_raw =>
    2.97 +        case Isabelle_Markup.Invoke_Scala(name, id) if output.is_raw =>
    2.98            Future.fork {
    2.99 -            val arg = XML.content(result.body).mkString
   2.100 +            val arg = XML.content(output.body).mkString
   2.101              val (tag, res) = Invoke_Scala.method(name, arg)
   2.102              prover.get.invoke_scala(id, tag, res)
   2.103            }
   2.104  
   2.105 -        case Isabelle_Markup.Cancel_Scala(id) if result.is_raw =>
   2.106 +        case Isabelle_Markup.Cancel_Scala(id) if output.is_raw =>
   2.107            System.err.println("cancel_scala " + id)  // FIXME actually cancel JVM task
   2.108  
   2.109 -        case Isabelle_Markup.Ready if result.is_raw =>
   2.110 +        case Isabelle_Markup.Ready if output.is_raw =>
   2.111              // FIXME move to ML side (!?)
   2.112              syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have")
   2.113              syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show")
   2.114              phase = Session.Ready
   2.115  
   2.116 -        case Isabelle_Markup.Loaded_Theory(name) if result.is_raw =>
   2.117 +        case Isabelle_Markup.Loaded_Theory(name) if output.is_raw =>
   2.118            thy_load.register_thy(name)
   2.119  
   2.120 -        case Isabelle_Markup.Command_Decl(name, kind) if result.is_raw =>
   2.121 +        case Isabelle_Markup.Command_Decl(name, kind) if output.is_raw =>
   2.122            syntax += (name, kind)
   2.123  
   2.124 -        case Isabelle_Markup.Keyword_Decl(name) if result.is_raw =>
   2.125 +        case Isabelle_Markup.Keyword_Decl(name) if output.is_raw =>
   2.126            syntax += name
   2.127  
   2.128          case _ =>
   2.129 -          if (result.is_exit && phase == Session.Startup) phase = Session.Failed
   2.130 -          else if (result.is_exit) phase = Session.Inactive
   2.131 -          else if (result.is_stdout) { }
   2.132 -          else bad_result(result)
   2.133 +          if (output.is_exit && phase == Session.Startup) phase = Session.Failed
   2.134 +          else if (output.is_exit) phase = Session.Inactive
   2.135 +          else if (output.is_stdout) { }
   2.136 +          else bad_output(output)
   2.137        }
   2.138      }
   2.139      //}}}
   2.140 @@ -473,11 +473,11 @@
   2.141              case input: Isabelle_Process.Input =>
   2.142                protocol_messages.event(input)
   2.143  
   2.144 -            case result: Isabelle_Process.Result =>
   2.145 -              handle_result(result)
   2.146 -              if (result.is_syslog) syslog_messages.event(result)
   2.147 -              if (result.is_stdout || result.is_stderr) raw_output_messages.event(result)
   2.148 -              protocol_messages.event(result)
   2.149 +            case output: Isabelle_Process.Output =>
   2.150 +              handle_output(output)
   2.151 +              if (output.is_syslog) syslog_messages.event(output)
   2.152 +              if (output.is_stdout || output.is_stderr) raw_output_messages.event(output)
   2.153 +              protocol_messages.event(output)
   2.154            }
   2.155  
   2.156          case change: Change_Node
     3.1 --- a/src/Tools/jEdit/src/protocol_dockable.scala	Sat Mar 03 16:59:30 2012 +0100
     3.2 +++ b/src/Tools/jEdit/src/protocol_dockable.scala	Sat Mar 03 17:30:14 2012 +0100
     3.3 @@ -31,8 +31,8 @@
     3.4          case input: Isabelle_Process.Input =>
     3.5            Swing_Thread.now { text_area.append(input.toString + "\n") }
     3.6  
     3.7 -        case result: Isabelle_Process.Result =>
     3.8 -          Swing_Thread.now { text_area.append(result.message.toString + "\n") }
     3.9 +        case output: Isabelle_Process.Output =>
    3.10 +          Swing_Thread.now { text_area.append(output.message.toString + "\n") }
    3.11  
    3.12          case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
    3.13        }
     4.1 --- a/src/Tools/jEdit/src/raw_output_dockable.scala	Sat Mar 03 16:59:30 2012 +0100
     4.2 +++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Sat Mar 03 17:30:14 2012 +0100
     4.3 @@ -29,9 +29,9 @@
     4.4    private val main_actor = actor {
     4.5      loop {
     4.6        react {
     4.7 -        case result: Isabelle_Process.Result =>
     4.8 -          if (result.is_stdout || result.is_stderr)
     4.9 -            Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
    4.10 +        case output: Isabelle_Process.Output =>
    4.11 +          if (output.is_stdout || output.is_stderr)
    4.12 +            Swing_Thread.now { text_area.append(XML.content(output.message).mkString) }
    4.13  
    4.14          case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad)
    4.15        }
     5.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Sat Mar 03 16:59:30 2012 +0100
     5.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Sat Mar 03 17:30:14 2012 +0100
     5.3 @@ -173,8 +173,8 @@
     5.4    private val main_actor = actor {
     5.5      loop {
     5.6        react {
     5.7 -        case result: Isabelle_Process.Result =>
     5.8 -          if (result.is_syslog)
     5.9 +        case output: Isabelle_Process.Output =>
    5.10 +          if (output.is_syslog)
    5.11              Swing_Thread.now {
    5.12                val text = Isabelle.session.current_syslog()
    5.13                if (text != syslog.text) syslog.text = text