echo prover input via raw_messages, for improved protocol tracing;
authorwenzelm
Sat Jul 09 21:53:27 2011 +0200 (2011-07-09 ago)
changeset 43721fad8634cee62
parent 43720 8dd722886c76
child 43722 9b5dadb0c28d
echo prover input via raw_messages, for improved protocol tracing;
src/Pure/General/markup.scala
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/General/markup.scala	Sat Jul 09 18:54:50 2011 +0200
     1.2 +++ b/src/Pure/General/markup.scala	Sat Jul 09 21:53:27 2011 +0200
     1.3 @@ -302,6 +302,12 @@
     1.4    val EDIT = "edit"
     1.5  
     1.6  
     1.7 +  /* prover process */
     1.8 +
     1.9 +  val PROVER_COMMAND = "prover_command"
    1.10 +  val PROVER_ARG = "prover_arg"
    1.11 +
    1.12 +
    1.13    /* messages */
    1.14  
    1.15    val Serial = new Long_Property("serial")
     2.1 --- a/src/Pure/System/isabelle_process.scala	Sat Jul 09 18:54:50 2011 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.scala	Sat Jul 09 21:53:27 2011 +0200
     2.3 @@ -32,7 +32,17 @@
     2.4        ('G' : Int) -> Markup.ERROR)
     2.5    }
     2.6  
     2.7 -  class Result(val message: XML.Elem)
     2.8 +  abstract class Message
     2.9 +
    2.10 +  class Input(name: String, args: List[String]) extends Message
    2.11 +  {
    2.12 +    override def toString: String =
    2.13 +      XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
    2.14 +        args.map(s =>
    2.15 +          List(XML.Text("\n"), XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
    2.16 +  }
    2.17 +
    2.18 +  class Result(val message: XML.Elem) extends Message
    2.19    {
    2.20      def kind = message.markup.name
    2.21      def properties = message.markup.properties
    2.22 @@ -377,7 +387,10 @@
    2.23      command_input._2 ! Input_Chunks(Standard_System.string_bytes(name) :: args.toList)
    2.24  
    2.25    def input(name: String, args: String*): Unit =
    2.26 +  {
    2.27 +    receiver ! new Input(name, args.toList)
    2.28      input_bytes(name, args.map(Standard_System.string_bytes): _*)
    2.29 +  }
    2.30  
    2.31    def close(): Unit = { close(command_input); close(standard_input) }
    2.32  }
     3.1 --- a/src/Pure/System/session.scala	Sat Jul 09 18:54:50 2011 +0200
     3.2 +++ b/src/Pure/System/session.scala	Sat Jul 09 21:53:27 2011 +0200
     3.3 @@ -58,7 +58,7 @@
     3.4    val assignments = new Event_Bus[Session.Assignment.type]
     3.5    val commands_changed = new Event_Bus[Session.Commands_Changed]
     3.6    val phase_changed = new Event_Bus[Session.Phase]
     3.7 -  val raw_messages = new Event_Bus[Isabelle_Process.Result]
     3.8 +  val raw_messages = new Event_Bus[Isabelle_Process.Message]
     3.9  
    3.10  
    3.11  
    3.12 @@ -276,8 +276,6 @@
    3.13            }
    3.14            else bad_result(result)
    3.15          }
    3.16 -
    3.17 -      raw_messages.event(result)
    3.18      }
    3.19      //}}}
    3.20  
    3.21 @@ -320,8 +318,12 @@
    3.22          case Change_Node(name, header, change) if prover.isDefined =>
    3.23            handle_change(name, header, change)
    3.24  
    3.25 +        case input: Isabelle_Process.Input =>
    3.26 +          raw_messages.event(input)
    3.27 +
    3.28          case result: Isabelle_Process.Result =>
    3.29            handle_result(result)
    3.30 +          raw_messages.event(result)
    3.31  
    3.32          case bad => System.err.println("session_actor: ignoring bad message " + bad)
    3.33        }
     4.1 --- a/src/Tools/jEdit/src/protocol_dockable.scala	Sat Jul 09 18:54:50 2011 +0200
     4.2 +++ b/src/Tools/jEdit/src/protocol_dockable.scala	Sat Jul 09 21:53:27 2011 +0200
     4.3 @@ -28,6 +28,9 @@
     4.4    private val main_actor = actor {
     4.5      loop {
     4.6        react {
     4.7 +        case input: Isabelle_Process.Input =>
     4.8 +          Swing_Thread.now { text_area.append(input.toString + "\n") }
     4.9 +
    4.10          case result: Isabelle_Process.Result =>
    4.11            Swing_Thread.now { text_area.append(result.message.toString + "\n") }
    4.12  
     5.1 --- a/src/Tools/jEdit/src/raw_output_dockable.scala	Sat Jul 09 18:54:50 2011 +0200
     5.2 +++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Sat Jul 09 21:53:27 2011 +0200
     5.3 @@ -30,6 +30,8 @@
     5.4    private val main_actor = actor {
     5.5      loop {
     5.6        react {
     5.7 +        case input: Isabelle_Process.Input =>
     5.8 +
     5.9          case result: Isabelle_Process.Result =>
    5.10            if (result.is_stdout)
    5.11              Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
     6.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Sat Jul 09 18:54:50 2011 +0200
     6.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Sat Jul 09 21:53:27 2011 +0200
     6.3 @@ -76,6 +76,8 @@
     6.4    private val main_actor = actor {
     6.5      loop {
     6.6        react {
     6.7 +        case input: Isabelle_Process.Input =>
     6.8 +
     6.9          case result: Isabelle_Process.Result =>
    6.10            if (result.is_syslog)
    6.11              Swing_Thread.now {