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;
--- a/src/Pure/General/markup.scala Sat Aug 07 21:22:39 2010 +0200
+++ b/src/Pure/General/markup.scala Sat Aug 07 22:09:52 2010 +0200
@@ -214,3 +214,5 @@
val DATA = "data"
}
+
+sealed case class Markup(name: String, properties: List[(String, String)])
--- a/src/Pure/General/pretty.scala Sat Aug 07 21:22:39 2010 +0200
+++ b/src/Pure/General/pretty.scala Sat Aug 07 22:09:52 2010 +0200
@@ -17,11 +17,11 @@
object Block
{
def apply(indent: Int, body: List[XML.Tree]): XML.Tree =
- XML.Elem(Markup.BLOCK, List((Markup.INDENT, indent.toString)), body)
+ XML.Elem(Markup(Markup.BLOCK, List((Markup.INDENT, indent.toString))), body)
def unapply(tree: XML.Tree): Option[(Int, List[XML.Tree])] =
tree match {
- case XML.Elem(Markup.BLOCK, List((Markup.INDENT, indent)), body) =>
+ case XML.Elem(Markup(Markup.BLOCK, List((Markup.INDENT, indent))), body) =>
Markup.parse_int(indent) match {
case Some(i) => Some((i, body))
case None => None
@@ -33,12 +33,12 @@
object Break
{
def apply(width: Int): XML.Tree =
- XML.Elem(Markup.BREAK, List((Markup.WIDTH, width.toString)),
+ XML.Elem(Markup(Markup.BREAK, List((Markup.WIDTH, width.toString))),
List(XML.Text(Symbol.spaces(width))))
def unapply(tree: XML.Tree): Option[Int] =
tree match {
- case XML.Elem(Markup.BREAK, List((Markup.WIDTH, width)), _) => Markup.parse_int(width)
+ case XML.Elem(Markup(Markup.BREAK, List((Markup.WIDTH, width))), _) => Markup.parse_int(width)
case _ => None
}
}
@@ -50,7 +50,7 @@
private def standard_format(tree: XML.Tree): List[XML.Tree] =
tree match {
- case XML.Elem(name, atts, body) => List(XML.Elem(name, atts, body.flatMap(standard_format)))
+ case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(standard_format)))
case XML.Text(text) =>
Library.separate(FBreak,
Library.chunks(text).toList.map((s: CharSequence) => XML.Text(s.toString)))
@@ -82,7 +82,7 @@
def content_length(tree: XML.Tree): Double =
tree match {
- case XML.Elem(_, _, body) => (0.0 /: body)(_ + content_length(_))
+ case XML.Elem(_, body) => (0.0 /: body)(_ + content_length(_))
case XML.Text(s) => metric(s)
}
@@ -122,10 +122,10 @@
else format(ts, blockin, after, text.newline.blanks(blockin.toInt))
case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin.toInt))
- case XML.Elem(name, atts, body) :: ts =>
+ case XML.Elem(markup, body) :: ts =>
val btext = format(body, blockin, breakdist(ts, after), text.copy(tx = Nil))
val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
- val btext1 = btext.copy(tx = XML.Elem(name, atts, btext.content) :: text.tx)
+ val btext1 = btext.copy(tx = XML.Elem(markup, btext.content) :: text.tx)
format(ts1, blockin, after, btext1)
case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s, metric(s)))
}
@@ -146,7 +146,7 @@
case Block(_, body) => body.flatMap(fmt)
case Break(wd) => List(XML.Text(Symbol.spaces(wd)))
case FBreak => List(XML.Text(Symbol.space))
- case XML.Elem(name, atts, body) => List(XML.Elem(name, atts, body.flatMap(fmt)))
+ case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt)))
case XML.Text(_) => List(tree)
}
input.flatMap(standard_format).flatMap(fmt)
--- a/src/Pure/General/xml.scala Sat Aug 07 21:22:39 2010 +0200
+++ b/src/Pure/General/xml.scala Sat Aug 07 22:09:52 2010 +0200
@@ -24,11 +24,11 @@
s.toString
}
}
- case class Elem(name: String, attributes: Attributes, body: List[Tree]) extends Tree
+ case class Elem(markup: Markup, body: List[Tree]) extends Tree
case class Text(content: String) extends Tree
- def elem(name: String, body: List[Tree]) = Elem(name, Nil, body)
- def elem(name: String) = Elem(name, Nil, Nil)
+ def elem(name: String, body: List[Tree]) = Elem(Markup(name, Nil), body)
+ def elem(name: String) = Elem(Markup(name, Nil), Nil)
/* string representation */
@@ -56,9 +56,9 @@
private def append_tree(tree: Tree, s: StringBuilder) {
tree match {
- case Elem(name, atts, Nil) =>
+ case Elem(Markup(name, atts), Nil) =>
s ++= "<"; append_elem(name, atts, s); s ++= "/>"
- case Elem(name, atts, ts) =>
+ case Elem(Markup(name, atts), ts) =>
s ++= "<"; append_elem(name, atts, s); s ++= ">"
for (t <- ts) append_tree(t, s)
s ++= "</"; s ++= name; s ++= ">"
@@ -72,7 +72,7 @@
private type State = Option[(String, List[Tree])]
private def get_next(tree: Tree): State = tree match {
- case Elem(_, _, body) => get_nexts(body)
+ case Elem(_, body) => get_nexts(body)
case Text(content) => Some(content, Nil)
}
private def get_nexts(trees: List[Tree]): State = trees match {
@@ -127,14 +127,23 @@
case Some(y) => y
case None => store(x.map(p => (cache_string(p._1), cache_string(p._2))))
}
+ def cache_markup(x: Markup): Markup =
+ lookup(x) match {
+ case Some(y) => y
+ case None =>
+ x match {
+ case Markup(name, props) =>
+ store(Markup(cache_string(name), cache_props(props)))
+ }
+ }
def cache_tree(x: XML.Tree): XML.Tree =
lookup(x) match {
case Some(y) => y
case None =>
x match {
- case XML.Elem(name, props, body) =>
- store(XML.Elem(cache_string(name), cache_props(props), cache_trees(body)))
- case XML.Text(text) => XML.Text(cache_string(text))
+ case XML.Elem(markup, body) =>
+ store(XML.Elem(cache_markup(markup), cache_trees(body)))
+ case XML.Text(text) => store(XML.Text(cache_string(text)))
}
}
def cache_trees(x: List[XML.Tree]): List[XML.Tree] =
@@ -158,11 +167,11 @@
def document_node(doc: org.w3c.dom.Document, tree: Tree): org.w3c.dom.Node =
{
def DOM(tr: Tree): org.w3c.dom.Node = tr match {
- case Elem(Markup.DATA, Nil, List(data, t)) =>
+ case Elem(Markup(Markup.DATA, Nil), List(data, t)) =>
val node = DOM(t)
node.setUserData(Markup.DATA, data, null)
node
- case Elem(name, atts, ts) =>
+ case Elem(Markup(name, atts), ts) =>
if (name == Markup.DATA)
error("Malformed data element: " + tr.toString)
val node = doc.createElement(name)
--- a/src/Pure/General/yxml.scala Sat Aug 07 21:22:39 2010 +0200
+++ b/src/Pure/General/yxml.scala Sat Aug 07 22:09:52 2010 +0200
@@ -64,7 +64,7 @@
/* stack operations */
def buffer(): ListBuffer[XML.Tree] = new ListBuffer[XML.Tree]
- var stack: List[((String, XML.Attributes), ListBuffer[XML.Tree])] = List((("", Nil), buffer()))
+ var stack: List[(Markup, ListBuffer[XML.Tree])] = List((Markup("", Nil), buffer()))
def add(x: XML.Tree)
{
@@ -74,15 +74,16 @@
def push(name: String, atts: XML.Attributes)
{
if (name == "") err_element()
- else stack = ((name, atts), buffer()) :: stack
+ else stack = (Markup(name, atts), buffer()) :: stack
}
def pop()
{
(stack: @unchecked) match {
- case ((("", _), _) :: _) => err_unbalanced("")
- case (((name, atts), body) :: pending) =>
- stack = pending; add(XML.Elem(name, atts, body.toList))
+ case ((Markup("", _), _) :: _) => err_unbalanced("")
+ case ((markup, body) :: pending) =>
+ stack = pending
+ add(XML.Elem(markup, body.toList))
}
}
@@ -100,8 +101,8 @@
}
}
stack match {
- case List((("", _), body)) => body.toList
- case ((name, _), _) :: _ => err_unbalanced(name)
+ case List((Markup("", _), body)) => body.toList
+ case (Markup(name, _), _) :: _ => err_unbalanced(name)
}
}
@@ -116,7 +117,7 @@
/* failsafe parsing */
private def markup_failsafe(source: CharSequence) =
- XML.Elem (Markup.MALFORMED, Nil,
+ XML.Elem (Markup(Markup.MALFORMED, Nil),
List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
def parse_body_failsafe(source: CharSequence): List[XML.Tree] =
--- a/src/Pure/Isar/isar_document.scala Sat Aug 07 21:22:39 2010 +0200
+++ b/src/Pure/Isar/isar_document.scala Sat Aug 07 22:09:52 2010 +0200
@@ -14,7 +14,7 @@
object Assign {
def unapply(msg: XML.Tree): Option[List[XML.Tree]] =
msg match {
- case XML.Elem(Markup.ASSIGN, Nil, edits) => Some(edits)
+ case XML.Elem(Markup(Markup.ASSIGN, Nil), edits) => Some(edits)
case _ => None
}
}
@@ -22,7 +22,7 @@
object Edit {
def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.State_ID)] =
msg match {
- case XML.Elem(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id)), Nil) =>
+ case XML.Elem(Markup(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id))), Nil) =>
Some(cmd_id, state_id)
case _ => None
}
--- a/src/Pure/Isar/keyword.scala Sat Aug 07 21:22:39 2010 +0200
+++ b/src/Pure/Isar/keyword.scala Sat Aug 07 22:09:52 2010 +0200
@@ -55,7 +55,7 @@
object Keyword_Decl {
def unapply(msg: XML.Tree): Option[String] =
msg match {
- case XML.Elem(Markup.KEYWORD_DECL, List((Markup.NAME, name)), _) => Some(name)
+ case XML.Elem(Markup(Markup.KEYWORD_DECL, List((Markup.NAME, name))), _) => Some(name)
case _ => None
}
}
@@ -63,7 +63,7 @@
object Command_Decl {
def unapply(msg: XML.Tree): Option[(String, String)] =
msg match {
- case XML.Elem(Markup.COMMAND_DECL, List((Markup.NAME, name), (Markup.KIND, kind)), _) =>
+ case XML.Elem(Markup(Markup.COMMAND_DECL, List((Markup.NAME, name), (Markup.KIND, kind))), _) =>
Some((name, kind))
case _ => None
}
--- a/src/Pure/PIDE/state.scala Sat Aug 07 21:22:39 2010 +0200
+++ b/src/Pure/PIDE/state.scala Sat Aug 07 22:09:52 2010 +0200
@@ -76,15 +76,15 @@
def accumulate(message: XML.Tree): State =
message match {
- case XML.Elem(Markup.STATUS, _, elems) =>
+ case XML.Elem(Markup(Markup.STATUS, _), elems) =>
(this /: elems)((state, elem) =>
elem match {
- case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
- case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
- case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
- case XML.Elem(Markup.FORKED, _, _) => state.add_forks(1)
- case XML.Elem(Markup.JOINED, _, _) => state.add_forks(-1)
- case XML.Elem(kind, atts, body) if Position.get_id(atts) == Some(command.id) =>
+ case XML.Elem(Markup(Markup.UNPROCESSED, _), _) => state.set_status(Command.Status.UNPROCESSED)
+ case XML.Elem(Markup(Markup.FINISHED, _), _) => state.set_status(Command.Status.FINISHED)
+ case XML.Elem(Markup(Markup.FAILED, _), _) => state.set_status(Command.Status.FAILED)
+ case XML.Elem(Markup(Markup.FORKED, _), _) => state.add_forks(1)
+ case XML.Elem(Markup(Markup.JOINED, _), _) => state.add_forks(-1)
+ case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) =>
atts match {
case Position.Range(begin, end) =>
if (kind == Markup.ML_TYPING) {
@@ -94,7 +94,7 @@
}
else if (kind == Markup.ML_REF) {
body match {
- case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
+ case List(XML.Elem(Markup(Markup.ML_DEF, atts), _)) =>
state.add_markup(command.markup_node(
begin - 1, end - 1,
Command.RefInfo(
--- a/src/Pure/System/isabelle_process.scala Sat Aug 07 21:22:39 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala Sat Aug 07 22:09:52 2010 +0200
@@ -45,26 +45,26 @@
class Result(val message: XML.Elem)
{
- def kind = message.name
+ def kind = message.markup.name
+ def properties = message.markup.properties
def body = message.body
def is_raw = Kind.is_raw(kind)
def is_control = Kind.is_control(kind)
def is_system = Kind.is_system(kind)
def is_status = kind == Markup.STATUS
- def is_ready = is_status && body == List(XML.Elem(Markup.READY, Nil, Nil))
+ def is_ready = is_status && body == List(XML.Elem(Markup(Markup.READY, Nil), Nil))
override def toString: String =
{
val res =
if (is_status) message.body.map(_.toString).mkString
else Pretty.string_of(message.body)
- val props = message.attributes
- if (props.isEmpty)
+ if (properties.isEmpty)
kind.toString + " [[" + res + "]]"
else
kind.toString + " " +
- (for ((x, y) <- props) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
+ (for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
}
def cache(c: XML.Cache): Result = new Result(c.cache_tree(message).asInstanceOf[XML.Elem])
@@ -98,7 +98,7 @@
if (kind == Markup.INIT) {
for ((Markup.PID, p) <- props) pid = p
}
- receiver ! new Result(XML.Elem(kind, props, body))
+ receiver ! new Result(XML.Elem(Markup(kind, props), body))
}
private def put_result(kind: String, text: String)
@@ -300,7 +300,7 @@
val header = read_chunk()
val body = read_chunk()
header match {
- case List(XML.Elem(name, props, Nil))
+ case List(XML.Elem(Markup(name, props), Nil))
if name.size == 1 && Kind.markup.isDefinedAt(name(0)) =>
put_result(Kind.markup(name(0)), props, body)
case _ => throw new Protocol_Error("bad header: " + header.toString)
--- a/src/Pure/System/session.scala Sat Aug 07 21:22:39 2010 +0200
+++ b/src/Pure/System/session.scala Sat Aug 07 22:09:52 2010 +0200
@@ -138,7 +138,7 @@
{
raw_results.event(result)
- val target_id: Option[Session.Entity_ID] = Position.get_id(result.message.attributes)
+ val target_id: Option[Session.Entity_ID] = Position.get_id(result.properties)
val target: Option[Session.Entity] =
target_id match {
case None => None
--- a/src/Pure/Thy/html.scala Sat Aug 07 21:22:39 2010 +0200
+++ b/src/Pure/Thy/html.scala Sat Aug 07 22:09:52 2010 +0200
@@ -42,7 +42,7 @@
// document markup
def span(cls: String, body: List[XML.Tree]): XML.Elem =
- XML.Elem(SPAN, List((CLASS, cls)), body)
+ XML.Elem(Markup(SPAN, List((CLASS, cls))), body)
def hidden(txt: String): XML.Elem =
span(Markup.HIDDEN, List(XML.Text(txt)))
@@ -52,7 +52,7 @@
def spans(tree: XML.Tree): List[XML.Tree] =
tree match {
- case XML.Elem(name, _, ts) =>
+ case XML.Elem(Markup(name, _), ts) =>
List(XML.elem(Markup.DATA, List(tree, span(name, ts.flatMap(spans)))))
case XML.Text(txt) =>
val ts = new ListBuffer[XML.Tree]
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Sat Aug 07 21:22:39 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Sat Aug 07 22:09:52 2010 +0200
@@ -68,8 +68,8 @@
val snapshot = doc_view.model.snapshot()
val filtered_results =
snapshot.document.current_state(cmd).results filter {
- case XML.Elem(Markup.TRACING, _, _) => show_tracing
- case XML.Elem(Markup.DEBUG, _, _) => show_debug
+ case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing
+ case XML.Elem(Markup(Markup.DEBUG, _), _) => show_debug
case _ => true
}
html_panel.render(filtered_results)