simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
authorwenzelm
Sat Aug 07 22:09:52 2010 +0200 (2010-08-07 ago)
changeset 38230ed147003de4b
parent 38229 61d0fe8b96ac
child 38231 968844caaff9
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
XML.cache_tree: actually store XML.Text as well;
added Isabelle_Process.Result.properties;
src/Pure/General/markup.scala
src/Pure/General/pretty.scala
src/Pure/General/xml.scala
src/Pure/General/yxml.scala
src/Pure/Isar/isar_document.scala
src/Pure/Isar/keyword.scala
src/Pure/PIDE/state.scala
src/Pure/System/isabelle_process.scala
src/Pure/System/session.scala
src/Pure/Thy/html.scala
src/Tools/jEdit/src/jedit/output_dockable.scala
     1.1 --- a/src/Pure/General/markup.scala	Sat Aug 07 21:22:39 2010 +0200
     1.2 +++ b/src/Pure/General/markup.scala	Sat Aug 07 22:09:52 2010 +0200
     1.3 @@ -214,3 +214,5 @@
     1.4  
     1.5    val DATA = "data"
     1.6  }
     1.7 +
     1.8 +sealed case class Markup(name: String, properties: List[(String, String)])
     2.1 --- a/src/Pure/General/pretty.scala	Sat Aug 07 21:22:39 2010 +0200
     2.2 +++ b/src/Pure/General/pretty.scala	Sat Aug 07 22:09:52 2010 +0200
     2.3 @@ -17,11 +17,11 @@
     2.4    object Block
     2.5    {
     2.6      def apply(indent: Int, body: List[XML.Tree]): XML.Tree =
     2.7 -      XML.Elem(Markup.BLOCK, List((Markup.INDENT, indent.toString)), body)
     2.8 +      XML.Elem(Markup(Markup.BLOCK, List((Markup.INDENT, indent.toString))), body)
     2.9  
    2.10      def unapply(tree: XML.Tree): Option[(Int, List[XML.Tree])] =
    2.11        tree match {
    2.12 -        case XML.Elem(Markup.BLOCK, List((Markup.INDENT, indent)), body) =>
    2.13 +        case XML.Elem(Markup(Markup.BLOCK, List((Markup.INDENT, indent))), body) =>
    2.14            Markup.parse_int(indent) match {
    2.15              case Some(i) => Some((i, body))
    2.16              case None => None
    2.17 @@ -33,12 +33,12 @@
    2.18    object Break
    2.19    {
    2.20      def apply(width: Int): XML.Tree =
    2.21 -      XML.Elem(Markup.BREAK, List((Markup.WIDTH, width.toString)),
    2.22 +      XML.Elem(Markup(Markup.BREAK, List((Markup.WIDTH, width.toString))),
    2.23          List(XML.Text(Symbol.spaces(width))))
    2.24  
    2.25      def unapply(tree: XML.Tree): Option[Int] =
    2.26        tree match {
    2.27 -        case XML.Elem(Markup.BREAK, List((Markup.WIDTH, width)), _) => Markup.parse_int(width)
    2.28 +        case XML.Elem(Markup(Markup.BREAK, List((Markup.WIDTH, width))), _) => Markup.parse_int(width)
    2.29          case _ => None
    2.30        }
    2.31    }
    2.32 @@ -50,7 +50,7 @@
    2.33  
    2.34    private def standard_format(tree: XML.Tree): List[XML.Tree] =
    2.35      tree match {
    2.36 -      case XML.Elem(name, atts, body) => List(XML.Elem(name, atts, body.flatMap(standard_format)))
    2.37 +      case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(standard_format)))
    2.38        case XML.Text(text) =>
    2.39          Library.separate(FBreak,
    2.40            Library.chunks(text).toList.map((s: CharSequence) => XML.Text(s.toString)))
    2.41 @@ -82,7 +82,7 @@
    2.42  
    2.43      def content_length(tree: XML.Tree): Double =
    2.44        tree match {
    2.45 -        case XML.Elem(_, _, body) => (0.0 /: body)(_ + content_length(_))
    2.46 +        case XML.Elem(_, body) => (0.0 /: body)(_ + content_length(_))
    2.47          case XML.Text(s) => metric(s)
    2.48        }
    2.49  
    2.50 @@ -122,10 +122,10 @@
    2.51            else format(ts, blockin, after, text.newline.blanks(blockin.toInt))
    2.52          case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin.toInt))
    2.53  
    2.54 -        case XML.Elem(name, atts, body) :: ts =>
    2.55 +        case XML.Elem(markup, body) :: ts =>
    2.56            val btext = format(body, blockin, breakdist(ts, after), text.copy(tx = Nil))
    2.57            val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
    2.58 -          val btext1 = btext.copy(tx = XML.Elem(name, atts, btext.content) :: text.tx)
    2.59 +          val btext1 = btext.copy(tx = XML.Elem(markup, btext.content) :: text.tx)
    2.60            format(ts1, blockin, after, btext1)
    2.61          case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s, metric(s)))
    2.62        }
    2.63 @@ -146,7 +146,7 @@
    2.64          case Block(_, body) => body.flatMap(fmt)
    2.65          case Break(wd) => List(XML.Text(Symbol.spaces(wd)))
    2.66          case FBreak => List(XML.Text(Symbol.space))
    2.67 -        case XML.Elem(name, atts, body) => List(XML.Elem(name, atts, body.flatMap(fmt)))
    2.68 +        case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt)))
    2.69          case XML.Text(_) => List(tree)
    2.70        }
    2.71      input.flatMap(standard_format).flatMap(fmt)
     3.1 --- a/src/Pure/General/xml.scala	Sat Aug 07 21:22:39 2010 +0200
     3.2 +++ b/src/Pure/General/xml.scala	Sat Aug 07 22:09:52 2010 +0200
     3.3 @@ -24,11 +24,11 @@
     3.4        s.toString
     3.5      }
     3.6    }
     3.7 -  case class Elem(name: String, attributes: Attributes, body: List[Tree]) extends Tree
     3.8 +  case class Elem(markup: Markup, body: List[Tree]) extends Tree
     3.9    case class Text(content: String) extends Tree
    3.10  
    3.11 -  def elem(name: String, body: List[Tree]) = Elem(name, Nil, body)
    3.12 -  def elem(name: String) = Elem(name, Nil, Nil)
    3.13 +  def elem(name: String, body: List[Tree]) = Elem(Markup(name, Nil), body)
    3.14 +  def elem(name: String) = Elem(Markup(name, Nil), Nil)
    3.15  
    3.16  
    3.17    /* string representation */
    3.18 @@ -56,9 +56,9 @@
    3.19  
    3.20    private def append_tree(tree: Tree, s: StringBuilder) {
    3.21      tree match {
    3.22 -      case Elem(name, atts, Nil) =>
    3.23 +      case Elem(Markup(name, atts), Nil) =>
    3.24          s ++= "<"; append_elem(name, atts, s); s ++= "/>"
    3.25 -      case Elem(name, atts, ts) =>
    3.26 +      case Elem(Markup(name, atts), ts) =>
    3.27          s ++= "<"; append_elem(name, atts, s); s ++= ">"
    3.28          for (t <- ts) append_tree(t, s)
    3.29          s ++= "</"; s ++= name; s ++= ">"
    3.30 @@ -72,7 +72,7 @@
    3.31    private type State = Option[(String, List[Tree])]
    3.32  
    3.33    private def get_next(tree: Tree): State = tree match {
    3.34 -    case Elem(_, _, body) => get_nexts(body)
    3.35 +    case Elem(_, body) => get_nexts(body)
    3.36      case Text(content) => Some(content, Nil)
    3.37    }
    3.38    private def get_nexts(trees: List[Tree]): State = trees match {
    3.39 @@ -127,14 +127,23 @@
    3.40            case Some(y) => y
    3.41            case None => store(x.map(p => (cache_string(p._1), cache_string(p._2))))
    3.42          }
    3.43 +    def cache_markup(x: Markup): Markup =
    3.44 +      lookup(x) match {
    3.45 +        case Some(y) => y
    3.46 +        case None =>
    3.47 +          x match {
    3.48 +            case Markup(name, props) =>
    3.49 +              store(Markup(cache_string(name), cache_props(props)))
    3.50 +          }
    3.51 +      }
    3.52      def cache_tree(x: XML.Tree): XML.Tree =
    3.53        lookup(x) match {
    3.54          case Some(y) => y
    3.55          case None =>
    3.56            x match {
    3.57 -            case XML.Elem(name, props, body) =>
    3.58 -              store(XML.Elem(cache_string(name), cache_props(props), cache_trees(body)))
    3.59 -            case XML.Text(text) => XML.Text(cache_string(text))
    3.60 +            case XML.Elem(markup, body) =>
    3.61 +              store(XML.Elem(cache_markup(markup), cache_trees(body)))
    3.62 +            case XML.Text(text) => store(XML.Text(cache_string(text)))
    3.63            }
    3.64        }
    3.65      def cache_trees(x: List[XML.Tree]): List[XML.Tree] =
    3.66 @@ -158,11 +167,11 @@
    3.67    def document_node(doc: org.w3c.dom.Document, tree: Tree): org.w3c.dom.Node =
    3.68    {
    3.69      def DOM(tr: Tree): org.w3c.dom.Node = tr match {
    3.70 -      case Elem(Markup.DATA, Nil, List(data, t)) =>
    3.71 +      case Elem(Markup(Markup.DATA, Nil), List(data, t)) =>
    3.72          val node = DOM(t)
    3.73          node.setUserData(Markup.DATA, data, null)
    3.74          node
    3.75 -      case Elem(name, atts, ts) =>
    3.76 +      case Elem(Markup(name, atts), ts) =>
    3.77          if (name == Markup.DATA)
    3.78            error("Malformed data element: " + tr.toString)
    3.79          val node = doc.createElement(name)
     4.1 --- a/src/Pure/General/yxml.scala	Sat Aug 07 21:22:39 2010 +0200
     4.2 +++ b/src/Pure/General/yxml.scala	Sat Aug 07 22:09:52 2010 +0200
     4.3 @@ -64,7 +64,7 @@
     4.4      /* stack operations */
     4.5  
     4.6      def buffer(): ListBuffer[XML.Tree] = new ListBuffer[XML.Tree]
     4.7 -    var stack: List[((String, XML.Attributes), ListBuffer[XML.Tree])] = List((("", Nil), buffer()))
     4.8 +    var stack: List[(Markup, ListBuffer[XML.Tree])] = List((Markup("", Nil), buffer()))
     4.9  
    4.10      def add(x: XML.Tree)
    4.11      {
    4.12 @@ -74,15 +74,16 @@
    4.13      def push(name: String, atts: XML.Attributes)
    4.14      {
    4.15        if (name == "") err_element()
    4.16 -      else stack = ((name, atts), buffer()) :: stack
    4.17 +      else stack = (Markup(name, atts), buffer()) :: stack
    4.18      }
    4.19  
    4.20      def pop()
    4.21      {
    4.22        (stack: @unchecked) match {
    4.23 -        case ((("", _), _) :: _) => err_unbalanced("")
    4.24 -        case (((name, atts), body) :: pending) =>
    4.25 -          stack = pending; add(XML.Elem(name, atts, body.toList))
    4.26 +        case ((Markup("", _), _) :: _) => err_unbalanced("")
    4.27 +        case ((markup, body) :: pending) =>
    4.28 +          stack = pending
    4.29 +          add(XML.Elem(markup, body.toList))
    4.30        }
    4.31      }
    4.32  
    4.33 @@ -100,8 +101,8 @@
    4.34        }
    4.35      }
    4.36      stack match {
    4.37 -      case List((("", _), body)) => body.toList
    4.38 -      case ((name, _), _) :: _ => err_unbalanced(name)
    4.39 +      case List((Markup("", _), body)) => body.toList
    4.40 +      case (Markup(name, _), _) :: _ => err_unbalanced(name)
    4.41      }
    4.42    }
    4.43  
    4.44 @@ -116,7 +117,7 @@
    4.45    /* failsafe parsing */
    4.46  
    4.47    private def markup_failsafe(source: CharSequence) =
    4.48 -    XML.Elem (Markup.MALFORMED, Nil,
    4.49 +    XML.Elem (Markup(Markup.MALFORMED, Nil),
    4.50        List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
    4.51  
    4.52    def parse_body_failsafe(source: CharSequence): List[XML.Tree] =
     5.1 --- a/src/Pure/Isar/isar_document.scala	Sat Aug 07 21:22:39 2010 +0200
     5.2 +++ b/src/Pure/Isar/isar_document.scala	Sat Aug 07 22:09:52 2010 +0200
     5.3 @@ -14,7 +14,7 @@
     5.4    object Assign {
     5.5      def unapply(msg: XML.Tree): Option[List[XML.Tree]] =
     5.6        msg match {
     5.7 -        case XML.Elem(Markup.ASSIGN, Nil, edits) => Some(edits)
     5.8 +        case XML.Elem(Markup(Markup.ASSIGN, Nil), edits) => Some(edits)
     5.9          case _ => None
    5.10        }
    5.11    }
    5.12 @@ -22,7 +22,7 @@
    5.13    object Edit {
    5.14      def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.State_ID)] =
    5.15        msg match {
    5.16 -        case XML.Elem(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id)), Nil) =>
    5.17 +        case XML.Elem(Markup(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id))), Nil) =>
    5.18            Some(cmd_id, state_id)
    5.19          case _ => None
    5.20        }
     6.1 --- a/src/Pure/Isar/keyword.scala	Sat Aug 07 21:22:39 2010 +0200
     6.2 +++ b/src/Pure/Isar/keyword.scala	Sat Aug 07 22:09:52 2010 +0200
     6.3 @@ -55,7 +55,7 @@
     6.4    object Keyword_Decl {
     6.5      def unapply(msg: XML.Tree): Option[String] =
     6.6        msg match {
     6.7 -        case XML.Elem(Markup.KEYWORD_DECL, List((Markup.NAME, name)), _) => Some(name)
     6.8 +        case XML.Elem(Markup(Markup.KEYWORD_DECL, List((Markup.NAME, name))), _) => Some(name)
     6.9          case _ => None
    6.10        }
    6.11    }
    6.12 @@ -63,7 +63,7 @@
    6.13    object Command_Decl {
    6.14      def unapply(msg: XML.Tree): Option[(String, String)] =
    6.15        msg match {
    6.16 -        case XML.Elem(Markup.COMMAND_DECL, List((Markup.NAME, name), (Markup.KIND, kind)), _) =>
    6.17 +        case XML.Elem(Markup(Markup.COMMAND_DECL, List((Markup.NAME, name), (Markup.KIND, kind))), _) =>
    6.18            Some((name, kind))
    6.19          case _ => None
    6.20        }
     7.1 --- a/src/Pure/PIDE/state.scala	Sat Aug 07 21:22:39 2010 +0200
     7.2 +++ b/src/Pure/PIDE/state.scala	Sat Aug 07 22:09:52 2010 +0200
     7.3 @@ -76,15 +76,15 @@
     7.4  
     7.5    def accumulate(message: XML.Tree): State =
     7.6      message match {
     7.7 -      case XML.Elem(Markup.STATUS, _, elems) =>
     7.8 +      case XML.Elem(Markup(Markup.STATUS, _), elems) =>
     7.9          (this /: elems)((state, elem) =>
    7.10            elem match {
    7.11 -            case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
    7.12 -            case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
    7.13 -            case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
    7.14 -            case XML.Elem(Markup.FORKED, _, _) => state.add_forks(1)
    7.15 -            case XML.Elem(Markup.JOINED, _, _) => state.add_forks(-1)
    7.16 -            case XML.Elem(kind, atts, body) if Position.get_id(atts) == Some(command.id) =>
    7.17 +            case XML.Elem(Markup(Markup.UNPROCESSED, _), _) => state.set_status(Command.Status.UNPROCESSED)
    7.18 +            case XML.Elem(Markup(Markup.FINISHED, _), _) => state.set_status(Command.Status.FINISHED)
    7.19 +            case XML.Elem(Markup(Markup.FAILED, _), _) => state.set_status(Command.Status.FAILED)
    7.20 +            case XML.Elem(Markup(Markup.FORKED, _), _) => state.add_forks(1)
    7.21 +            case XML.Elem(Markup(Markup.JOINED, _), _) => state.add_forks(-1)
    7.22 +            case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) =>
    7.23                atts match {
    7.24                  case Position.Range(begin, end) =>
    7.25                    if (kind == Markup.ML_TYPING) {
    7.26 @@ -94,7 +94,7 @@
    7.27                    }
    7.28                    else if (kind == Markup.ML_REF) {
    7.29                      body match {
    7.30 -                      case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
    7.31 +                      case List(XML.Elem(Markup(Markup.ML_DEF, atts), _)) =>
    7.32                          state.add_markup(command.markup_node(
    7.33                            begin - 1, end - 1,
    7.34                            Command.RefInfo(
     8.1 --- a/src/Pure/System/isabelle_process.scala	Sat Aug 07 21:22:39 2010 +0200
     8.2 +++ b/src/Pure/System/isabelle_process.scala	Sat Aug 07 22:09:52 2010 +0200
     8.3 @@ -45,26 +45,26 @@
     8.4  
     8.5    class Result(val message: XML.Elem)
     8.6    {
     8.7 -    def kind = message.name
     8.8 +    def kind = message.markup.name
     8.9 +    def properties = message.markup.properties
    8.10      def body = message.body
    8.11  
    8.12      def is_raw = Kind.is_raw(kind)
    8.13      def is_control = Kind.is_control(kind)
    8.14      def is_system = Kind.is_system(kind)
    8.15      def is_status = kind == Markup.STATUS
    8.16 -    def is_ready = is_status && body == List(XML.Elem(Markup.READY, Nil, Nil))
    8.17 +    def is_ready = is_status && body == List(XML.Elem(Markup(Markup.READY, Nil), Nil))
    8.18  
    8.19      override def toString: String =
    8.20      {
    8.21        val res =
    8.22          if (is_status) message.body.map(_.toString).mkString
    8.23          else Pretty.string_of(message.body)
    8.24 -      val props = message.attributes
    8.25 -      if (props.isEmpty)
    8.26 +      if (properties.isEmpty)
    8.27          kind.toString + " [[" + res + "]]"
    8.28        else
    8.29          kind.toString + " " +
    8.30 -          (for ((x, y) <- props) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
    8.31 +          (for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
    8.32      }
    8.33  
    8.34      def cache(c: XML.Cache): Result = new Result(c.cache_tree(message).asInstanceOf[XML.Elem])
    8.35 @@ -98,7 +98,7 @@
    8.36      if (kind == Markup.INIT) {
    8.37        for ((Markup.PID, p) <- props) pid = p
    8.38      }
    8.39 -    receiver ! new Result(XML.Elem(kind, props, body))
    8.40 +    receiver ! new Result(XML.Elem(Markup(kind, props), body))
    8.41    }
    8.42  
    8.43    private def put_result(kind: String, text: String)
    8.44 @@ -300,7 +300,7 @@
    8.45              val header = read_chunk()
    8.46              val body = read_chunk()
    8.47              header match {
    8.48 -              case List(XML.Elem(name, props, Nil))
    8.49 +              case List(XML.Elem(Markup(name, props), Nil))
    8.50                    if name.size == 1 && Kind.markup.isDefinedAt(name(0)) =>
    8.51                  put_result(Kind.markup(name(0)), props, body)
    8.52                case _ => throw new Protocol_Error("bad header: " + header.toString)
     9.1 --- a/src/Pure/System/session.scala	Sat Aug 07 21:22:39 2010 +0200
     9.2 +++ b/src/Pure/System/session.scala	Sat Aug 07 22:09:52 2010 +0200
     9.3 @@ -138,7 +138,7 @@
     9.4      {
     9.5        raw_results.event(result)
     9.6  
     9.7 -      val target_id: Option[Session.Entity_ID] = Position.get_id(result.message.attributes)
     9.8 +      val target_id: Option[Session.Entity_ID] = Position.get_id(result.properties)
     9.9        val target: Option[Session.Entity] =
    9.10          target_id match {
    9.11            case None => None
    10.1 --- a/src/Pure/Thy/html.scala	Sat Aug 07 21:22:39 2010 +0200
    10.2 +++ b/src/Pure/Thy/html.scala	Sat Aug 07 22:09:52 2010 +0200
    10.3 @@ -42,7 +42,7 @@
    10.4    // document markup
    10.5  
    10.6    def span(cls: String, body: List[XML.Tree]): XML.Elem =
    10.7 -    XML.Elem(SPAN, List((CLASS, cls)), body)
    10.8 +    XML.Elem(Markup(SPAN, List((CLASS, cls))), body)
    10.9  
   10.10    def hidden(txt: String): XML.Elem =
   10.11      span(Markup.HIDDEN, List(XML.Text(txt)))
   10.12 @@ -52,7 +52,7 @@
   10.13  
   10.14    def spans(tree: XML.Tree): List[XML.Tree] =
   10.15      tree match {
   10.16 -      case XML.Elem(name, _, ts) =>
   10.17 +      case XML.Elem(Markup(name, _), ts) =>
   10.18          List(XML.elem(Markup.DATA, List(tree, span(name, ts.flatMap(spans)))))
   10.19        case XML.Text(txt) =>
   10.20          val ts = new ListBuffer[XML.Tree]
    11.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Sat Aug 07 21:22:39 2010 +0200
    11.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Sat Aug 07 22:09:52 2010 +0200
    11.3 @@ -68,8 +68,8 @@
    11.4                val snapshot = doc_view.model.snapshot()
    11.5                val filtered_results =
    11.6                  snapshot.document.current_state(cmd).results filter {
    11.7 -                  case XML.Elem(Markup.TRACING, _, _) => show_tracing
    11.8 -                  case XML.Elem(Markup.DEBUG, _, _) => show_debug
    11.9 +                  case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing
   11.10 +                  case XML.Elem(Markup(Markup.DEBUG, _), _) => show_debug
   11.11                    case _ => true
   11.12                  }
   11.13                html_panel.render(filtered_results)