support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
authorwenzelm
Fri Sep 28 22:53:18 2012 +0200 (2012-09-28 ago)
changeset 496509fad6480300d
parent 49649 83094a50c53f
child 49651 c7585f8addc2
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
src/Pure/General/pretty.scala
src/Pure/PIDE/markup_tree.scala
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/xml.ML
src/Pure/PIDE/xml.scala
src/Pure/Thy/html.scala
     1.1 --- a/src/Pure/General/pretty.scala	Fri Sep 28 17:06:07 2012 +0200
     1.2 +++ b/src/Pure/General/pretty.scala	Fri Sep 28 22:53:18 2012 +0200
     1.3 @@ -66,6 +66,8 @@
     1.4  
     1.5    def standard_format(body: XML.Body): XML.Body =
     1.6      body flatMap {
     1.7 +      case XML.Wrapped_Elem(markup, body1, body2) =>
     1.8 +        List(XML.Wrapped_Elem(markup, body1, standard_format(body)))
     1.9        case XML.Elem(markup, body) => List(XML.Elem(markup, standard_format(body)))
    1.10        case XML.Text(text) => Library.separate(FBreak, split_lines(text).map(XML.Text))
    1.11      }
    1.12 @@ -96,6 +98,7 @@
    1.13  
    1.14      def content_length(tree: XML.Tree): Double =
    1.15        tree match {
    1.16 +        case XML.Wrapped_Elem(_, _, body) => (0.0 /: body)(_ + content_length(_))
    1.17          case XML.Elem(_, body) => (0.0 /: body)(_ + content_length(_))
    1.18          case XML.Text(s) => metric(s)
    1.19        }
    1.20 @@ -136,13 +139,21 @@
    1.21            else format(ts, blockin, after, text.newline.blanks(blockin.toInt))
    1.22          case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin.toInt))
    1.23  
    1.24 +        case XML.Wrapped_Elem(markup, body1, body2) :: ts =>
    1.25 +          val btext = format(body2, blockin, breakdist(ts, after), text.copy(tx = Nil))
    1.26 +          val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
    1.27 +          val btext1 = btext.copy(tx = XML.Wrapped_Elem(markup, body1, btext.content) :: text.tx)
    1.28 +          format(ts1, blockin, after, btext1)
    1.29 +
    1.30          case XML.Elem(markup, body) :: ts =>
    1.31            val btext = format(body, blockin, breakdist(ts, after), text.copy(tx = Nil))
    1.32            val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
    1.33            val btext1 = btext.copy(tx = XML.Elem(markup, btext.content) :: text.tx)
    1.34            format(ts1, blockin, after, btext1)
    1.35 +
    1.36          case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s, metric(s)))
    1.37        }
    1.38 +
    1.39      format(standard_format(input), 0.0, 0.0, Text()).content
    1.40    }
    1.41  
    1.42 @@ -160,6 +171,8 @@
    1.43          case Block(_, body) => body.flatMap(fmt)
    1.44          case Break(wd) => List(XML.Text(spaces(wd)))
    1.45          case FBreak => List(XML.Text(space))
    1.46 +        case XML.Wrapped_Elem(markup, body1, body2) =>
    1.47 +          List(XML.Wrapped_Elem(markup, body1, body2.flatMap(fmt)))
    1.48          case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt)))
    1.49          case XML.Text(_) => List(tree)
    1.50        }
     2.1 --- a/src/Pure/PIDE/markup_tree.scala	Fri Sep 28 17:06:07 2012 +0200
     2.2 +++ b/src/Pure/PIDE/markup_tree.scala	Fri Sep 28 22:53:18 2012 +0200
     2.3 @@ -66,11 +66,14 @@
     2.4  
     2.5    /* XML representation */
     2.6  
     2.7 -  // FIXME decode markup body
     2.8 -  @tailrec private def strip_elems(markups: List[Markup], body: XML.Body): (List[Markup], XML.Body) =
     2.9 +  @tailrec private def strip_elems(
    2.10 +      elems: List[XML.Elem], body: XML.Body): (List[XML.Elem], XML.Body) =
    2.11      body match {
    2.12 -      case List(XML.Elem(markup1, body1)) => strip_elems(markup1 :: markups, body1)
    2.13 -      case _ => (markups, body)
    2.14 +      case List(XML.Wrapped_Elem(markup1, body1, body2)) =>
    2.15 +        strip_elems(XML.Elem(markup1, body1) :: elems, body2)
    2.16 +      case List(XML.Elem(markup1, body1)) =>
    2.17 +        strip_elems(XML.Elem(markup1, Nil) :: elems, body1)
    2.18 +      case _ => (elems, body)
    2.19      }
    2.20  
    2.21    private def make_trees(acc: (Int, List[Markup_Tree]), tree: XML.Tree): (Int, List[Markup_Tree]) =
    2.22 @@ -84,7 +87,7 @@
    2.23          case (elems, body) =>
    2.24            val (end_offset, subtrees) = ((offset, Nil: List[Markup_Tree]) /: body)(make_trees)
    2.25            val range = Text.Range(offset, end_offset)
    2.26 -          val entry = Entry(range, elems.map(XML.Elem(_, Nil)), merge_disjoint(subtrees))
    2.27 +          val entry = Entry(range, elems, merge_disjoint(subtrees))
    2.28            (end_offset, new Markup_Tree(Branches.empty, entry) :: markup_trees)
    2.29        }
    2.30      }
    2.31 @@ -152,8 +155,10 @@
    2.32  
    2.33      def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body =
    2.34        (body /: rev_markups) {
    2.35 -        case (b, elem) => // FIXME encode markup body
    2.36 -          if (filter(elem)) List(XML.Elem(elem.markup, b)) else b
    2.37 +        case (b, elem) =>
    2.38 +          if (!filter(elem)) b
    2.39 +          else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b))
    2.40 +          else List(XML.Wrapped_Elem(elem.markup, elem.body, b))
    2.41        }
    2.42  
    2.43      def make_body(elem_range: Text.Range, elem_markup: List[XML.Elem], entries: Branches.T)
     3.1 --- a/src/Pure/PIDE/protocol.scala	Fri Sep 28 17:06:07 2012 +0200
     3.2 +++ b/src/Pure/PIDE/protocol.scala	Fri Sep 28 22:53:18 2012 +0200
     3.3 @@ -123,12 +123,17 @@
     3.4        case XML.Elem(Markup(Isabelle_Markup.REPORT, _), _) => false
     3.5        case XML.Elem(Markup(Isabelle_Markup.NO_REPORT, _), _) => false
     3.6        case _ => true
     3.7 -    } map { case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts)) case t => t }
     3.8 +    } map {
     3.9 +      case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_message(ts))
    3.10 +      case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts))
    3.11 +      case t => t
    3.12 +    }
    3.13  
    3.14    def message_reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
    3.15      body flatMap {
    3.16        case XML.Elem(Markup(Isabelle_Markup.REPORT, ps), ts) =>
    3.17          List(XML.Elem(Markup(Isabelle_Markup.REPORT, props ::: ps), ts))
    3.18 +      case XML.Wrapped_Elem(_, _, ts) => message_reports(props, ts)
    3.19        case XML.Elem(_, ts) => message_reports(props, ts)
    3.20        case XML.Text(_) => Nil
    3.21      }
    3.22 @@ -175,13 +180,24 @@
    3.23  
    3.24    def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =
    3.25    {
    3.26 +    def elem_positions(raw_range: Text.Range, set: Set[Text.Range], body: XML.Body)
    3.27 +      : Set[Text.Range] =
    3.28 +    {
    3.29 +      val range = command.decode(raw_range).restrict(command.range)
    3.30 +      body.foldLeft(if (range.is_singularity) set else set + range)(positions)
    3.31 +    }
    3.32      def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
    3.33        tree match {
    3.34 -        case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body)
    3.35 -        if include_pos(name) && id == command.id =>
    3.36 -          val range = command.decode(raw_range).restrict(command.range)
    3.37 -          body.foldLeft(if (range.is_singularity) set else set + range)(positions)
    3.38 -        case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(positions)
    3.39 +        case XML.Wrapped_Elem(Markup(name, Position.Id_Range(id, range)), _, body)
    3.40 +        if include_pos(name) && id == command.id => elem_positions(range, set, body)
    3.41 +
    3.42 +        case XML.Elem(Markup(name, Position.Id_Range(id, range)), body)
    3.43 +        if include_pos(name) && id == command.id => elem_positions(range, set, body)
    3.44 +
    3.45 +        case XML.Wrapped_Elem(_, _, body) => body.foldLeft(set)(positions)
    3.46 +
    3.47 +        case XML.Elem(_, body) => body.foldLeft(set)(positions)
    3.48 +
    3.49          case _ => set
    3.50        }
    3.51      val set = positions(Set.empty, message)
     4.1 --- a/src/Pure/PIDE/xml.ML	Fri Sep 28 17:06:07 2012 +0200
     4.2 +++ b/src/Pure/PIDE/xml.ML	Fri Sep 28 22:53:18 2012 +0200
     4.3 @@ -33,6 +33,8 @@
     4.4        Elem of (string * attributes) * tree list
     4.5      | Text of string
     4.6    type body = tree list
     4.7 +  val wrap_elem: ((string * attributes) * tree list) * tree list -> tree
     4.8 +  val unwrap_elem: tree -> (((string * attributes) * tree list) * tree list) option
     4.9    val add_content: tree -> Buffer.T -> Buffer.T
    4.10    val content_of: body -> string
    4.11    val header: string
    4.12 @@ -66,8 +68,31 @@
    4.13  
    4.14  type body = tree list;
    4.15  
    4.16 -fun add_content (Elem (_, ts)) = fold add_content ts
    4.17 -  | add_content (Text s) = Buffer.add s;
    4.18 +
    4.19 +(* wrapped elements *)
    4.20 +
    4.21 +val xml_elemN = "xml_elem";
    4.22 +val xml_nameN = "xml_name";
    4.23 +val xml_bodyN = "xml_body";
    4.24 +
    4.25 +fun wrap_elem (((a, atts), body1), body2) =
    4.26 +  Elem ((xml_elemN, (xml_nameN, a) :: atts), Elem ((xml_bodyN, []), body1) :: body2);
    4.27 +
    4.28 +fun unwrap_elem (Elem ((name, (n, a) :: atts), Elem ((name', atts'), body1) :: body2)) =
    4.29 +      if name = xml_elemN andalso n = xml_nameN andalso name' = xml_bodyN andalso null atts'
    4.30 +      then SOME (((a, atts), body1), body2) else NONE
    4.31 +  | unwrap_elem _ = NONE;
    4.32 +
    4.33 +
    4.34 +(* text context *)
    4.35 +
    4.36 +fun add_content tree =
    4.37 +  (case unwrap_elem tree of
    4.38 +    SOME (_, ts) => fold add_content ts
    4.39 +  | NONE =>
    4.40 +      (case tree of
    4.41 +        Elem (_, ts) => fold add_content ts
    4.42 +      | Text s => Buffer.add s));
    4.43  
    4.44  fun content_of body = Buffer.empty |> fold add_content body |> Buffer.content;
    4.45  
     5.1 --- a/src/Pure/PIDE/xml.scala	Fri Sep 28 17:06:07 2012 +0200
     5.2 +++ b/src/Pure/PIDE/xml.scala	Fri Sep 28 22:53:18 2012 +0200
     5.3 @@ -30,7 +30,59 @@
     5.4    type Body = List[Tree]
     5.5  
     5.6  
     5.7 -  /* string representation */
     5.8 +  /* wrapped elements */
     5.9 +
    5.10 +  val XML_ELEM = "xml_elem";
    5.11 +  val XML_NAME = "xml_name";
    5.12 +  val XML_BODY = "xml_body";
    5.13 +
    5.14 +  object Wrapped_Elem
    5.15 +  {
    5.16 +    def apply(markup: Markup, body1: Body, body2: Body): XML.Elem =
    5.17 +      Elem(Markup(XML_ELEM, (XML_NAME, markup.name) :: markup.properties),
    5.18 +        Elem(Markup(XML_BODY, Nil), body1) :: body2)
    5.19 +
    5.20 +    def unapply(tree: Tree): Option[(Markup, Body, Body)] =
    5.21 +      tree match {
    5.22 +        case
    5.23 +          Elem(Markup(XML_ELEM, (XML_NAME, name) :: props),
    5.24 +            Elem(Markup(XML_BODY, Nil), body1) :: body2) =>
    5.25 +          Some(Markup(name, props), body1, body2)
    5.26 +        case _ => None
    5.27 +      }
    5.28 +  }
    5.29 +
    5.30 +
    5.31 +  /* traverse text */
    5.32 +
    5.33 +  def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A =
    5.34 +  {
    5.35 +    def traverse(x: A, t: Tree): A =
    5.36 +      t match {
    5.37 +        case Wrapped_Elem(_, _, ts) => (x /: ts)(traverse)
    5.38 +        case Elem(_, ts) => (x /: ts)(traverse)
    5.39 +        case Text(s) => op(x, s)
    5.40 +      }
    5.41 +    (a /: body)(traverse)
    5.42 +  }
    5.43 +
    5.44 +  def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length }
    5.45 +
    5.46 +
    5.47 +  /* text content */
    5.48 +
    5.49 +  def content(body: Body): String =
    5.50 +  {
    5.51 +    val text = new StringBuilder(text_length(body))
    5.52 +    traverse_text(body)(()) { case (_, s) => text.append(s) }
    5.53 +    text.toString
    5.54 +  }
    5.55 +
    5.56 +  def content(tree: Tree): String = content(List(tree))
    5.57 +
    5.58 +
    5.59 +
    5.60 +  /** string representation **/
    5.61  
    5.62    def string_of_body(body: Body): String =
    5.63    {
    5.64 @@ -68,33 +120,6 @@
    5.65    def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
    5.66  
    5.67  
    5.68 -  /* traverse text */
    5.69 -
    5.70 -  def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A =
    5.71 -  {
    5.72 -    def traverse(x: A, t: Tree): A =
    5.73 -      t match {
    5.74 -        case Elem(_, ts) => (x /: ts)(traverse)
    5.75 -        case Text(s) => op(x, s)
    5.76 -      }
    5.77 -    (a /: body)(traverse)
    5.78 -  }
    5.79 -
    5.80 -  def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length }
    5.81 -
    5.82 -
    5.83 -  /* text content */
    5.84 -
    5.85 -  def content(body: Body): String =
    5.86 -  {
    5.87 -    val text = new StringBuilder(text_length(body))
    5.88 -    traverse_text(body)(()) { case (_, s) => text.append(s) }
    5.89 -    text.toString
    5.90 -  }
    5.91 -
    5.92 -  def content(tree: Tree): String = content(List(tree))
    5.93 -
    5.94 -
    5.95  
    5.96    /** cache for partial sharing (weak table) **/
    5.97  
     6.1 --- a/src/Pure/Thy/html.scala	Fri Sep 28 17:06:07 2012 +0200
     6.2 +++ b/src/Pure/Thy/html.scala	Fri Sep 28 22:53:18 2012 +0200
     6.3 @@ -61,8 +61,10 @@
     6.4    {
     6.5      def html_spans(tree: XML.Tree): XML.Body =
     6.6        tree match {
     6.7 -        case XML.Elem(m @ Markup(name, props), ts) =>
     6.8 -          List(span(name, ts.flatMap(html_spans)))
     6.9 +        case XML.Wrapped_Elem(markup, _, ts) =>
    6.10 +          List(span(markup.name, ts.flatMap(html_spans)))
    6.11 +        case XML.Elem(markup, ts) =>
    6.12 +          List(span(markup.name, ts.flatMap(html_spans)))
    6.13          case XML.Text(txt) =>
    6.14            val ts = new ListBuffer[XML.Tree]
    6.15            val t = new StringBuilder