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) }
 }