more abstract view on prover output messages;
authorwenzelm
Fri May 21 14:53:19 2010 +0200 (2010-05-21)
changeset 370381ce1b19f78f4
parent 37037 35d45feccbc6
child 37039 d01da9438170
more abstract view on prover output messages;
src/Pure/General/output.scala
src/Pure/System/isabelle_process.scala
src/Pure/build-jars
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/General/output.scala	Fri May 21 14:53:19 2010 +0200
     1.3 @@ -0,0 +1,24 @@
     1.4 +/*  Title:      Pure/General/output.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Prover output messages.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +object Output
    1.14 +{
    1.15 +  object Message
    1.16 +  {
    1.17 +    def apply(name: String, atts: XML.Attributes, body: List[XML.Tree]): XML.Tree =
    1.18 +      XML.Elem(Markup.MESSAGE, (Markup.CLASS, name) :: atts, body)
    1.19 +
    1.20 +    def unapply(tree: XML.Tree): Option[(String, XML.Attributes, List[XML.Tree])] =
    1.21 +      tree match {
    1.22 +        case XML.Elem(Markup.MESSAGE, (Markup.CLASS, name) :: atts, body) =>
    1.23 +          Some(name, atts, body)
    1.24 +        case _ => None
    1.25 +      }
    1.26 +  }
    1.27 +}
     2.1 --- a/src/Pure/System/isabelle_process.scala	Fri May 21 12:59:44 2010 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.scala	Fri May 21 14:53:19 2010 +0200
     2.3 @@ -84,7 +84,7 @@
     2.4  
     2.5    class Result(val kind: Kind.Value, val props: List[(String, String)], val body: List[XML.Tree])
     2.6    {
     2.7 -    def message = XML.Elem(Markup.MESSAGE, (Markup.CLASS, Kind.markup(kind)) :: props, body)
     2.8 +    def message = Output.Message(Kind.markup(kind), props, body)
     2.9  
    2.10      override def toString: String =
    2.11      {
     3.1 --- a/src/Pure/build-jars	Fri May 21 12:59:44 2010 +0200
     3.2 +++ b/src/Pure/build-jars	Fri May 21 14:53:19 2010 +0200
     3.3 @@ -26,6 +26,7 @@
     3.4    General/exn.scala
     3.5    General/linear_set.scala
     3.6    General/markup.scala
     3.7 +  General/output.scala
     3.8    General/position.scala
     3.9    General/pretty.scala
    3.10    General/scan.scala