src/Pure/System/isabelle_process.scala
changeset 43721 fad8634cee62
parent 43695 5130dfe1b7be
child 43745 562e35bc351e
     1.1 --- a/src/Pure/System/isabelle_process.scala	Sat Jul 09 18:54:50 2011 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Sat Jul 09 21:53:27 2011 +0200
     1.3 @@ -32,7 +32,17 @@
     1.4        ('G' : Int) -> Markup.ERROR)
     1.5    }
     1.6  
     1.7 -  class Result(val message: XML.Elem)
     1.8 +  abstract class Message
     1.9 +
    1.10 +  class Input(name: String, args: List[String]) extends Message
    1.11 +  {
    1.12 +    override def toString: String =
    1.13 +      XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
    1.14 +        args.map(s =>
    1.15 +          List(XML.Text("\n"), XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
    1.16 +  }
    1.17 +
    1.18 +  class Result(val message: XML.Elem) extends Message
    1.19    {
    1.20      def kind = message.markup.name
    1.21      def properties = message.markup.properties
    1.22 @@ -377,7 +387,10 @@
    1.23      command_input._2 ! Input_Chunks(Standard_System.string_bytes(name) :: args.toList)
    1.24  
    1.25    def input(name: String, args: String*): Unit =
    1.26 +  {
    1.27 +    receiver ! new Input(name, args.toList)
    1.28      input_bytes(name, args.map(Standard_System.string_bytes): _*)
    1.29 +  }
    1.30  
    1.31    def close(): Unit = { close(command_input); close(standard_input) }
    1.32  }