# HG changeset patch
# User wenzelm
# Date 1310241207 -7200
# Node ID fad8634cee6257822b55b59c61d04bf49b58d980
# Parent  8dd722886c76ab0277a5e8e958a0da759477f7b1
echo prover input via raw_messages, for improved protocol tracing;

diff -r 8dd722886c76 -r fad8634cee62 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Sat Jul 09 18:54:50 2011 +0200
+++ b/src/Pure/General/markup.scala	Sat Jul 09 21:53:27 2011 +0200
@@ -302,6 +302,12 @@
   val EDIT = "edit"
 
 
+  /* prover process */
+
+  val PROVER_COMMAND = "prover_command"
+  val PROVER_ARG = "prover_arg"
+
+
   /* messages */
 
   val Serial = new Long_Property("serial")
diff -r 8dd722886c76 -r fad8634cee62 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Sat Jul 09 18:54:50 2011 +0200
+++ b/src/Pure/System/isabelle_process.scala	Sat Jul 09 21:53:27 2011 +0200
@@ -32,7 +32,17 @@
       ('G' : Int) -> Markup.ERROR)
   }
 
-  class Result(val message: XML.Elem)
+  abstract class Message
+
+  class Input(name: String, args: List[String]) extends Message
+  {
+    override def toString: String =
+      XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
+        args.map(s =>
+          List(XML.Text("\n"), XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
+  }
+
+  class Result(val message: XML.Elem) extends Message
   {
     def kind = message.markup.name
     def properties = message.markup.properties
@@ -377,7 +387,10 @@
     command_input._2 ! Input_Chunks(Standard_System.string_bytes(name) :: args.toList)
 
   def input(name: String, args: String*): Unit =
+  {
+    receiver ! new Input(name, args.toList)
     input_bytes(name, args.map(Standard_System.string_bytes): _*)
+  }
 
   def close(): Unit = { close(command_input); close(standard_input) }
 }
diff -r 8dd722886c76 -r fad8634cee62 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sat Jul 09 18:54:50 2011 +0200
+++ b/src/Pure/System/session.scala	Sat Jul 09 21:53:27 2011 +0200
@@ -58,7 +58,7 @@
   val assignments = new Event_Bus[Session.Assignment.type]
   val commands_changed = new Event_Bus[Session.Commands_Changed]
   val phase_changed = new Event_Bus[Session.Phase]
-  val raw_messages = new Event_Bus[Isabelle_Process.Result]
+  val raw_messages = new Event_Bus[Isabelle_Process.Message]
 
 
 
@@ -276,8 +276,6 @@
           }
           else bad_result(result)
         }
-
-      raw_messages.event(result)
     }
     //}}}
 
@@ -320,8 +318,12 @@
         case Change_Node(name, header, change) if prover.isDefined =>
           handle_change(name, header, change)
 
+        case input: Isabelle_Process.Input =>
+          raw_messages.event(input)
+
         case result: Isabelle_Process.Result =>
           handle_result(result)
+          raw_messages.event(result)
 
         case bad => System.err.println("session_actor: ignoring bad message " + bad)
       }
diff -r 8dd722886c76 -r fad8634cee62 src/Tools/jEdit/src/protocol_dockable.scala
--- a/src/Tools/jEdit/src/protocol_dockable.scala	Sat Jul 09 18:54:50 2011 +0200
+++ b/src/Tools/jEdit/src/protocol_dockable.scala	Sat Jul 09 21:53:27 2011 +0200
@@ -28,6 +28,9 @@
   private val main_actor = actor {
     loop {
       react {
+        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") }
 
diff -r 8dd722886c76 -r fad8634cee62 src/Tools/jEdit/src/raw_output_dockable.scala
--- a/src/Tools/jEdit/src/raw_output_dockable.scala	Sat Jul 09 18:54:50 2011 +0200
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Sat Jul 09 21:53:27 2011 +0200
@@ -30,6 +30,8 @@
   private val main_actor = actor {
     loop {
       react {
+        case input: Isabelle_Process.Input =>
+
         case result: Isabelle_Process.Result =>
           if (result.is_stdout)
             Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
diff -r 8dd722886c76 -r fad8634cee62 src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Sat Jul 09 18:54:50 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Sat Jul 09 21:53:27 2011 +0200
@@ -76,6 +76,8 @@
   private val main_actor = actor {
     loop {
       react {
+        case input: Isabelle_Process.Input =>
+
         case result: Isabelle_Process.Result =>
           if (result.is_syslog)
             Swing_Thread.now {