# HG changeset patch
# User wenzelm
# Date 1330792214 -3600
# Node ID be21f050eda4d8cbc12dbca29e6dd925ba0141fa
# Parent  06a9b24c4a36e3f0bbb95678bbbe3244b681c374
tuned signature -- emphasize Isabelle_Process Input vs. Output;

diff -r 06a9b24c4a36 -r be21f050eda4 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Sat Mar 03 16:59:30 2012 +0100
+++ b/src/Pure/System/isabelle_process.scala	Sat Mar 03 17:30:14 2012 +0100
@@ -18,7 +18,7 @@
 
 object Isabelle_Process
 {
-  /* results */
+  /* messages */
 
   object Kind
   {
@@ -44,7 +44,7 @@
             XML.elem(Isabelle_Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
   }
 
-  class Result(val message: XML.Elem) extends Message
+  class Output(val message: XML.Elem) extends Message
   {
     def kind: String = message.markup.name
     def properties: Properties.T = message.markup.properties
@@ -84,29 +84,29 @@
   import Isabelle_Process._
 
 
-  /* results */
+  /* output */
 
-  private def system_result(text: String)
+  private def system_output(text: String)
   {
-    receiver(new Result(XML.Elem(Markup(Isabelle_Markup.SYSTEM, Nil), List(XML.Text(text)))))
+    receiver(new Output(XML.Elem(Markup(Isabelle_Markup.SYSTEM, Nil), List(XML.Text(text)))))
   }
 
   private val xml_cache = new XML.Cache()
 
-  private def put_result(kind: String, props: Properties.T, body: XML.Body)
+  private def output_message(kind: String, props: Properties.T, body: XML.Body)
   {
     if (kind == Isabelle_Markup.INIT) system_channel.accepted()
     if (kind == Isabelle_Markup.RAW)
-      receiver(new Result(XML.Elem(Markup(kind, props), body)))
+      receiver(new Output(XML.Elem(Markup(kind, props), body)))
     else {
       val msg = XML.Elem(Markup(kind, props), Protocol.clean_message(body))
-      receiver(new Result(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem]))
+      receiver(new Output(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem]))
     }
   }
 
-  private def put_result(kind: String, text: String)
+  private def output_message(kind: String, text: String)
   {
-    put_result(kind, Nil, List(XML.Text(Symbol.decode(text))))
+    output_message(kind, Nil, List(XML.Text(Symbol.decode(text))))
   }
 
 
@@ -147,7 +147,7 @@
   private def terminate_process()
   {
     try { process.terminate }
-    catch { case e: IOException => system_result("Failed to terminate Isabelle: " + e.getMessage) }
+    catch { case e: IOException => system_output("Failed to terminate Isabelle: " + e.getMessage) }
   }
 
   private val process_manager = Simple_Thread.fork("process_manager")
@@ -169,10 +169,10 @@
       }
       (finished.isEmpty || !finished.get, result.toString.trim)
     }
-    if (startup_errors != "") system_result(startup_errors)
+    if (startup_errors != "") system_output(startup_errors)
 
     if (startup_failed) {
-      put_result(Isabelle_Markup.EXIT, "Return code: 127")
+      output_message(Isabelle_Markup.EXIT, "Return code: 127")
       process.stdin.close
       Thread.sleep(300)
       terminate_process()
@@ -188,11 +188,11 @@
       val message = message_actor(message_stream)
 
       val rc = process_result.join
-      system_result("process terminated")
+      system_output("process terminated")
       for ((thread, _) <- List(standard_input, stdout, stderr, command_input, message))
         thread.join
-      system_result("process_manager terminated")
-      put_result(Isabelle_Markup.EXIT, "Return code: " + rc.toString)
+      system_output("process_manager terminated")
+      output_message(Isabelle_Markup.EXIT, "Return code: " + rc.toString)
     }
     system_channel.accepted()
   }
@@ -205,7 +205,7 @@
   def terminate()
   {
     close()
-    system_result("Terminating Isabelle process")
+    system_output("Terminating Isabelle process")
     terminate_process()
   }
 
@@ -235,8 +235,8 @@
           //}}}
         }
       }
-      catch { case e: IOException => system_result(name + ": " + e.getMessage) }
-      system_result(name + " terminated")
+      catch { case e: IOException => system_output(name + ": " + e.getMessage) }
+      system_output(name + " terminated")
     }
   }
 
@@ -263,7 +263,7 @@
             else done = true
           }
           if (result.length > 0) {
-            put_result(markup, result.toString)
+            output_message(markup, result.toString)
             result.length = 0
           }
           else {
@@ -273,8 +273,8 @@
           //}}}
         }
       }
-      catch { case e: IOException => system_result(name + ": " + e.getMessage) }
-      system_result(name + " terminated")
+      catch { case e: IOException => system_output(name + ": " + e.getMessage) }
+      system_output(name + " terminated")
     }
   }
 
@@ -304,8 +304,8 @@
           //}}}
         }
       }
-      catch { case e: IOException => system_result(name + ": " + e.getMessage) }
-      system_result(name + " terminated")
+      catch { case e: IOException => system_output(name + ": " + e.getMessage) }
+      system_output(name + " terminated")
     }
   }
 
@@ -365,7 +365,7 @@
                   if name.size == 1 && Kind.message_markup.isDefinedAt(name(0)) =>
                 val kind = Kind.message_markup(name(0))
                 val body = read_chunk(kind != Isabelle_Markup.RAW)
-                put_result(kind, props, body)
+                output_message(kind, props, body)
               case _ =>
                 read_chunk(false)
                 throw new Protocol_Error("bad header: " + header.toString)
@@ -376,12 +376,12 @@
         } while (c != -1)
       }
       catch {
-        case e: IOException => system_result("Cannot read message:\n" + e.getMessage)
-        case e: Protocol_Error => system_result("Malformed message:\n" + e.getMessage)
+        case e: IOException => system_output("Cannot read message:\n" + e.getMessage)
+        case e: Protocol_Error => system_output("Malformed message:\n" + e.getMessage)
       }
       stream.close
 
-      system_result(name + " terminated")
+      system_output(name + " terminated")
     }
   }
 
diff -r 06a9b24c4a36 -r be21f050eda4 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sat Mar 03 16:59:30 2012 +0100
+++ b/src/Pure/System/session.scala	Sat Mar 03 17:30:14 2012 +0100
@@ -56,8 +56,8 @@
   val caret_focus = new Event_Bus[Session.Caret_Focus.type]
   val commands_changed = new Event_Bus[Session.Commands_Changed]
   val phase_changed = new Event_Bus[Session.Phase]
-  val syslog_messages = new Event_Bus[Isabelle_Process.Result]
-  val raw_output_messages = new Event_Bus[Isabelle_Process.Result]
+  val syslog_messages = new Event_Bus[Isabelle_Process.Output]
+  val raw_output_messages = new Event_Bus[Isabelle_Process.Output]
   val protocol_messages = new Event_Bus[Isabelle_Process.Message]  // potential bottle-neck
 
 
@@ -193,14 +193,14 @@
       def invoke(msg: Isabelle_Process.Message): Unit = synchronized {
         buffer += msg
         msg match {
-          case result: Isabelle_Process.Result =>
-            if (result.is_syslog)
+          case output: Isabelle_Process.Output =>
+            if (output.is_syslog)
               syslog >> (queue =>
                 {
-                  val queue1 = queue.enqueue(result.message)
+                  val queue1 = queue.enqueue(output.message)
                   if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
                 })
-            if (result.is_raw) flush()
+            if (output.is_raw) flush()
           case _ =>
         }
       }
@@ -343,34 +343,34 @@
     //}}}
 
 
-    /* prover results */
+    /* prover output */
 
-    def handle_result(result: Isabelle_Process.Result)
+    def handle_output(output: Isabelle_Process.Output)
     //{{{
     {
-      def bad_result(result: Isabelle_Process.Result)
+      def bad_output(output: Isabelle_Process.Output)
       {
         if (verbose)
-          System.err.println("Ignoring prover result: " + result.message.toString)
+          System.err.println("Ignoring prover output: " + output.message.toString)
       }
 
-      result.properties match {
+      output.properties match {
 
-        case Position.Id(state_id) if !result.is_raw =>
+        case Position.Id(state_id) if !output.is_raw =>
           try {
-            val st = global_state >>> (_.accumulate(state_id, result.message))
+            val st = global_state >>> (_.accumulate(state_id, output.message))
             delay_commands_changed.invoke(st.command)
           }
           catch {
-            case _: Document.State.Fail => bad_result(result)
+            case _: Document.State.Fail => bad_output(output)
           }
 
-        case Isabelle_Markup.Assign_Execs if result.is_raw =>
-          XML.content(result.body).mkString match {
+        case Isabelle_Markup.Assign_Execs if output.is_raw =>
+          XML.content(output.body).mkString match {
             case Protocol.Assign(id, assign) =>
               try { handle_assign(id, assign) }
-              catch { case _: Document.State.Fail => bad_result(result) }
-            case _ => bad_result(result)
+              catch { case _: Document.State.Fail => bad_output(output) }
+            case _ => bad_output(output)
           }
           // FIXME separate timeout event/message!?
           if (prover.isDefined && System.currentTimeMillis() > prune_next) {
@@ -379,44 +379,44 @@
             prune_next = System.currentTimeMillis() + prune_delay.ms
           }
 
-        case Isabelle_Markup.Removed_Versions if result.is_raw =>
-          XML.content(result.body).mkString match {
+        case Isabelle_Markup.Removed_Versions if output.is_raw =>
+          XML.content(output.body).mkString match {
             case Protocol.Removed(removed) =>
               try { handle_removed(removed) }
-              catch { case _: Document.State.Fail => bad_result(result) }
-            case _ => bad_result(result)
+              catch { case _: Document.State.Fail => bad_output(output) }
+            case _ => bad_output(output)
           }
 
-        case Isabelle_Markup.Invoke_Scala(name, id) if result.is_raw =>
+        case Isabelle_Markup.Invoke_Scala(name, id) if output.is_raw =>
           Future.fork {
-            val arg = XML.content(result.body).mkString
+            val arg = XML.content(output.body).mkString
             val (tag, res) = Invoke_Scala.method(name, arg)
             prover.get.invoke_scala(id, tag, res)
           }
 
-        case Isabelle_Markup.Cancel_Scala(id) if result.is_raw =>
+        case Isabelle_Markup.Cancel_Scala(id) if output.is_raw =>
           System.err.println("cancel_scala " + id)  // FIXME actually cancel JVM task
 
-        case Isabelle_Markup.Ready if result.is_raw =>
+        case Isabelle_Markup.Ready if output.is_raw =>
             // FIXME move to ML side (!?)
             syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have")
             syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show")
             phase = Session.Ready
 
-        case Isabelle_Markup.Loaded_Theory(name) if result.is_raw =>
+        case Isabelle_Markup.Loaded_Theory(name) if output.is_raw =>
           thy_load.register_thy(name)
 
-        case Isabelle_Markup.Command_Decl(name, kind) if result.is_raw =>
+        case Isabelle_Markup.Command_Decl(name, kind) if output.is_raw =>
           syntax += (name, kind)
 
-        case Isabelle_Markup.Keyword_Decl(name) if result.is_raw =>
+        case Isabelle_Markup.Keyword_Decl(name) if output.is_raw =>
           syntax += name
 
         case _ =>
-          if (result.is_exit && phase == Session.Startup) phase = Session.Failed
-          else if (result.is_exit) phase = Session.Inactive
-          else if (result.is_stdout) { }
-          else bad_result(result)
+          if (output.is_exit && phase == Session.Startup) phase = Session.Failed
+          else if (output.is_exit) phase = Session.Inactive
+          else if (output.is_stdout) { }
+          else bad_output(output)
       }
     }
     //}}}
@@ -473,11 +473,11 @@
             case input: Isabelle_Process.Input =>
               protocol_messages.event(input)
 
-            case result: Isabelle_Process.Result =>
-              handle_result(result)
-              if (result.is_syslog) syslog_messages.event(result)
-              if (result.is_stdout || result.is_stderr) raw_output_messages.event(result)
-              protocol_messages.event(result)
+            case output: Isabelle_Process.Output =>
+              handle_output(output)
+              if (output.is_syslog) syslog_messages.event(output)
+              if (output.is_stdout || output.is_stderr) raw_output_messages.event(output)
+              protocol_messages.event(output)
           }
 
         case change: Change_Node
diff -r 06a9b24c4a36 -r be21f050eda4 src/Tools/jEdit/src/protocol_dockable.scala
--- a/src/Tools/jEdit/src/protocol_dockable.scala	Sat Mar 03 16:59:30 2012 +0100
+++ b/src/Tools/jEdit/src/protocol_dockable.scala	Sat Mar 03 17:30:14 2012 +0100
@@ -31,8 +31,8 @@
         case input: Isabelle_Process.Input =>
           Swing_Thread.now { text_area.append(input.toString + "\n") }
 
-        case result: Isabelle_Process.Result =>
-          Swing_Thread.now { text_area.append(result.message.toString + "\n") }
+        case output: Isabelle_Process.Output =>
+          Swing_Thread.now { text_area.append(output.message.toString + "\n") }
 
         case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
       }
diff -r 06a9b24c4a36 -r be21f050eda4 src/Tools/jEdit/src/raw_output_dockable.scala
--- a/src/Tools/jEdit/src/raw_output_dockable.scala	Sat Mar 03 16:59:30 2012 +0100
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Sat Mar 03 17:30:14 2012 +0100
@@ -29,9 +29,9 @@
   private val main_actor = actor {
     loop {
       react {
-        case result: Isabelle_Process.Result =>
-          if (result.is_stdout || result.is_stderr)
-            Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
+        case output: Isabelle_Process.Output =>
+          if (output.is_stdout || output.is_stderr)
+            Swing_Thread.now { text_area.append(XML.content(output.message).mkString) }
 
         case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad)
       }
diff -r 06a9b24c4a36 -r be21f050eda4 src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Sat Mar 03 16:59:30 2012 +0100
+++ b/src/Tools/jEdit/src/session_dockable.scala	Sat Mar 03 17:30:14 2012 +0100
@@ -173,8 +173,8 @@
   private val main_actor = actor {
     loop {
       react {
-        case result: Isabelle_Process.Result =>
-          if (result.is_syslog)
+        case output: Isabelle_Process.Output =>
+          if (output.is_syslog)
             Swing_Thread.now {
               val text = Isabelle.session.current_syslog()
               if (text != syslog.text) syslog.text = text