# HG changeset patch
# User wenzelm
# Date 1348865598 -7200
# Node ID 9fad6480300deb81edbacc911f4fc58f467608f2
# Parent  83094a50c53f138e37aaf970350dcbabff4cf1ad
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;

diff -r 83094a50c53f -r 9fad6480300d src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Fri Sep 28 17:06:07 2012 +0200
+++ b/src/Pure/General/pretty.scala	Fri Sep 28 22:53:18 2012 +0200
@@ -66,6 +66,8 @@
 
   def standard_format(body: XML.Body): XML.Body =
     body flatMap {
+      case XML.Wrapped_Elem(markup, body1, body2) =>
+        List(XML.Wrapped_Elem(markup, body1, standard_format(body)))
       case XML.Elem(markup, body) => List(XML.Elem(markup, standard_format(body)))
       case XML.Text(text) => Library.separate(FBreak, split_lines(text).map(XML.Text))
     }
@@ -96,6 +98,7 @@
 
     def content_length(tree: XML.Tree): Double =
       tree match {
+        case XML.Wrapped_Elem(_, _, body) => (0.0 /: body)(_ + content_length(_))
         case XML.Elem(_, body) => (0.0 /: body)(_ + content_length(_))
         case XML.Text(s) => metric(s)
       }
@@ -136,13 +139,21 @@
           else format(ts, blockin, after, text.newline.blanks(blockin.toInt))
         case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin.toInt))
 
+        case XML.Wrapped_Elem(markup, body1, body2) :: ts =>
+          val btext = format(body2, 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.Wrapped_Elem(markup, body1, btext.content) :: text.tx)
+          format(ts1, blockin, after, btext1)
+
         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(markup, btext.content) :: text.tx)
           format(ts1, blockin, after, btext1)
+
         case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s, metric(s)))
       }
+
     format(standard_format(input), 0.0, 0.0, Text()).content
   }
 
@@ -160,6 +171,8 @@
         case Block(_, body) => body.flatMap(fmt)
         case Break(wd) => List(XML.Text(spaces(wd)))
         case FBreak => List(XML.Text(space))
+        case XML.Wrapped_Elem(markup, body1, body2) =>
+          List(XML.Wrapped_Elem(markup, body1, body2.flatMap(fmt)))
         case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt)))
         case XML.Text(_) => List(tree)
       }
diff -r 83094a50c53f -r 9fad6480300d src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Fri Sep 28 17:06:07 2012 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Fri Sep 28 22:53:18 2012 +0200
@@ -66,11 +66,14 @@
 
   /* XML representation */
 
-  // FIXME decode markup body
-  @tailrec private def strip_elems(markups: List[Markup], body: XML.Body): (List[Markup], XML.Body) =
+  @tailrec private def strip_elems(
+      elems: List[XML.Elem], body: XML.Body): (List[XML.Elem], XML.Body) =
     body match {
-      case List(XML.Elem(markup1, body1)) => strip_elems(markup1 :: markups, body1)
-      case _ => (markups, body)
+      case List(XML.Wrapped_Elem(markup1, body1, body2)) =>
+        strip_elems(XML.Elem(markup1, body1) :: elems, body2)
+      case List(XML.Elem(markup1, body1)) =>
+        strip_elems(XML.Elem(markup1, Nil) :: elems, body1)
+      case _ => (elems, body)
     }
 
   private def make_trees(acc: (Int, List[Markup_Tree]), tree: XML.Tree): (Int, List[Markup_Tree]) =
@@ -84,7 +87,7 @@
         case (elems, body) =>
           val (end_offset, subtrees) = ((offset, Nil: List[Markup_Tree]) /: body)(make_trees)
           val range = Text.Range(offset, end_offset)
-          val entry = Entry(range, elems.map(XML.Elem(_, Nil)), merge_disjoint(subtrees))
+          val entry = Entry(range, elems, merge_disjoint(subtrees))
           (end_offset, new Markup_Tree(Branches.empty, entry) :: markup_trees)
       }
     }
@@ -152,8 +155,10 @@
 
     def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body =
       (body /: rev_markups) {
-        case (b, elem) => // FIXME encode markup body
-          if (filter(elem)) List(XML.Elem(elem.markup, b)) else b
+        case (b, elem) =>
+          if (!filter(elem)) b
+          else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b))
+          else List(XML.Wrapped_Elem(elem.markup, elem.body, b))
       }
 
     def make_body(elem_range: Text.Range, elem_markup: List[XML.Elem], entries: Branches.T)
diff -r 83094a50c53f -r 9fad6480300d src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Fri Sep 28 17:06:07 2012 +0200
+++ b/src/Pure/PIDE/protocol.scala	Fri Sep 28 22:53:18 2012 +0200
@@ -123,12 +123,17 @@
       case XML.Elem(Markup(Isabelle_Markup.REPORT, _), _) => false
       case XML.Elem(Markup(Isabelle_Markup.NO_REPORT, _), _) => false
       case _ => true
-    } map { case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts)) case t => t }
+    } map {
+      case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_message(ts))
+      case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts))
+      case t => t
+    }
 
   def message_reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
     body flatMap {
       case XML.Elem(Markup(Isabelle_Markup.REPORT, ps), ts) =>
         List(XML.Elem(Markup(Isabelle_Markup.REPORT, props ::: ps), ts))
+      case XML.Wrapped_Elem(_, _, ts) => message_reports(props, ts)
       case XML.Elem(_, ts) => message_reports(props, ts)
       case XML.Text(_) => Nil
     }
@@ -175,13 +180,24 @@
 
   def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =
   {
+    def elem_positions(raw_range: Text.Range, set: Set[Text.Range], body: XML.Body)
+      : Set[Text.Range] =
+    {
+      val range = command.decode(raw_range).restrict(command.range)
+      body.foldLeft(if (range.is_singularity) set else set + range)(positions)
+    }
     def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
       tree match {
-        case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body)
-        if include_pos(name) && id == command.id =>
-          val range = command.decode(raw_range).restrict(command.range)
-          body.foldLeft(if (range.is_singularity) set else set + range)(positions)
-        case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(positions)
+        case XML.Wrapped_Elem(Markup(name, Position.Id_Range(id, range)), _, body)
+        if include_pos(name) && id == command.id => elem_positions(range, set, body)
+
+        case XML.Elem(Markup(name, Position.Id_Range(id, range)), body)
+        if include_pos(name) && id == command.id => elem_positions(range, set, body)
+
+        case XML.Wrapped_Elem(_, _, body) => body.foldLeft(set)(positions)
+
+        case XML.Elem(_, body) => body.foldLeft(set)(positions)
+
         case _ => set
       }
     val set = positions(Set.empty, message)
diff -r 83094a50c53f -r 9fad6480300d src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Fri Sep 28 17:06:07 2012 +0200
+++ b/src/Pure/PIDE/xml.ML	Fri Sep 28 22:53:18 2012 +0200
@@ -33,6 +33,8 @@
       Elem of (string * attributes) * tree list
     | Text of string
   type body = tree list
+  val wrap_elem: ((string * attributes) * tree list) * tree list -> tree
+  val unwrap_elem: tree -> (((string * attributes) * tree list) * tree list) option
   val add_content: tree -> Buffer.T -> Buffer.T
   val content_of: body -> string
   val header: string
@@ -66,8 +68,31 @@
 
 type body = tree list;
 
-fun add_content (Elem (_, ts)) = fold add_content ts
-  | add_content (Text s) = Buffer.add s;
+
+(* wrapped elements *)
+
+val xml_elemN = "xml_elem";
+val xml_nameN = "xml_name";
+val xml_bodyN = "xml_body";
+
+fun wrap_elem (((a, atts), body1), body2) =
+  Elem ((xml_elemN, (xml_nameN, a) :: atts), Elem ((xml_bodyN, []), body1) :: body2);
+
+fun unwrap_elem (Elem ((name, (n, a) :: atts), Elem ((name', atts'), body1) :: body2)) =
+      if name = xml_elemN andalso n = xml_nameN andalso name' = xml_bodyN andalso null atts'
+      then SOME (((a, atts), body1), body2) else NONE
+  | unwrap_elem _ = NONE;
+
+
+(* text context *)
+
+fun add_content tree =
+  (case unwrap_elem tree of
+    SOME (_, ts) => fold add_content ts
+  | NONE =>
+      (case tree of
+        Elem (_, ts) => fold add_content ts
+      | Text s => Buffer.add s));
 
 fun content_of body = Buffer.empty |> fold add_content body |> Buffer.content;
 
diff -r 83094a50c53f -r 9fad6480300d src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Fri Sep 28 17:06:07 2012 +0200
+++ b/src/Pure/PIDE/xml.scala	Fri Sep 28 22:53:18 2012 +0200
@@ -30,7 +30,59 @@
   type Body = List[Tree]
 
 
-  /* string representation */
+  /* wrapped elements */
+
+  val XML_ELEM = "xml_elem";
+  val XML_NAME = "xml_name";
+  val XML_BODY = "xml_body";
+
+  object Wrapped_Elem
+  {
+    def apply(markup: Markup, body1: Body, body2: Body): XML.Elem =
+      Elem(Markup(XML_ELEM, (XML_NAME, markup.name) :: markup.properties),
+        Elem(Markup(XML_BODY, Nil), body1) :: body2)
+
+    def unapply(tree: Tree): Option[(Markup, Body, Body)] =
+      tree match {
+        case
+          Elem(Markup(XML_ELEM, (XML_NAME, name) :: props),
+            Elem(Markup(XML_BODY, Nil), body1) :: body2) =>
+          Some(Markup(name, props), body1, body2)
+        case _ => None
+      }
+  }
+
+
+  /* traverse text */
+
+  def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A =
+  {
+    def traverse(x: A, t: Tree): A =
+      t match {
+        case Wrapped_Elem(_, _, ts) => (x /: ts)(traverse)
+        case Elem(_, ts) => (x /: ts)(traverse)
+        case Text(s) => op(x, s)
+      }
+    (a /: body)(traverse)
+  }
+
+  def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length }
+
+
+  /* text content */
+
+  def content(body: Body): String =
+  {
+    val text = new StringBuilder(text_length(body))
+    traverse_text(body)(()) { case (_, s) => text.append(s) }
+    text.toString
+  }
+
+  def content(tree: Tree): String = content(List(tree))
+
+
+
+  /** string representation **/
 
   def string_of_body(body: Body): String =
   {
@@ -68,33 +120,6 @@
   def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
 
 
-  /* traverse text */
-
-  def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A =
-  {
-    def traverse(x: A, t: Tree): A =
-      t match {
-        case Elem(_, ts) => (x /: ts)(traverse)
-        case Text(s) => op(x, s)
-      }
-    (a /: body)(traverse)
-  }
-
-  def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length }
-
-
-  /* text content */
-
-  def content(body: Body): String =
-  {
-    val text = new StringBuilder(text_length(body))
-    traverse_text(body)(()) { case (_, s) => text.append(s) }
-    text.toString
-  }
-
-  def content(tree: Tree): String = content(List(tree))
-
-
 
   /** cache for partial sharing (weak table) **/
 
diff -r 83094a50c53f -r 9fad6480300d src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Fri Sep 28 17:06:07 2012 +0200
+++ b/src/Pure/Thy/html.scala	Fri Sep 28 22:53:18 2012 +0200
@@ -61,8 +61,10 @@
   {
     def html_spans(tree: XML.Tree): XML.Body =
       tree match {
-        case XML.Elem(m @ Markup(name, props), ts) =>
-          List(span(name, ts.flatMap(html_spans)))
+        case XML.Wrapped_Elem(markup, _, ts) =>
+          List(span(markup.name, ts.flatMap(html_spans)))
+        case XML.Elem(markup, ts) =>
+          List(span(markup.name, ts.flatMap(html_spans)))
         case XML.Text(txt) =>
           val ts = new ListBuffer[XML.Tree]
           val t = new StringBuilder