src/Pure/PIDE/xml.scala
changeset 49650 9fad6480300d
parent 49613 2f6986e2ef06
child 51223 c6a8a05ff0a0
     1.1 --- a/src/Pure/PIDE/xml.scala	Fri Sep 28 17:06:07 2012 +0200
     1.2 +++ b/src/Pure/PIDE/xml.scala	Fri Sep 28 22:53:18 2012 +0200
     1.3 @@ -30,7 +30,59 @@
     1.4    type Body = List[Tree]
     1.5  
     1.6  
     1.7 -  /* string representation */
     1.8 +  /* wrapped elements */
     1.9 +
    1.10 +  val XML_ELEM = "xml_elem";
    1.11 +  val XML_NAME = "xml_name";
    1.12 +  val XML_BODY = "xml_body";
    1.13 +
    1.14 +  object Wrapped_Elem
    1.15 +  {
    1.16 +    def apply(markup: Markup, body1: Body, body2: Body): XML.Elem =
    1.17 +      Elem(Markup(XML_ELEM, (XML_NAME, markup.name) :: markup.properties),
    1.18 +        Elem(Markup(XML_BODY, Nil), body1) :: body2)
    1.19 +
    1.20 +    def unapply(tree: Tree): Option[(Markup, Body, Body)] =
    1.21 +      tree match {
    1.22 +        case
    1.23 +          Elem(Markup(XML_ELEM, (XML_NAME, name) :: props),
    1.24 +            Elem(Markup(XML_BODY, Nil), body1) :: body2) =>
    1.25 +          Some(Markup(name, props), body1, body2)
    1.26 +        case _ => None
    1.27 +      }
    1.28 +  }
    1.29 +
    1.30 +
    1.31 +  /* traverse text */
    1.32 +
    1.33 +  def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A =
    1.34 +  {
    1.35 +    def traverse(x: A, t: Tree): A =
    1.36 +      t match {
    1.37 +        case Wrapped_Elem(_, _, ts) => (x /: ts)(traverse)
    1.38 +        case Elem(_, ts) => (x /: ts)(traverse)
    1.39 +        case Text(s) => op(x, s)
    1.40 +      }
    1.41 +    (a /: body)(traverse)
    1.42 +  }
    1.43 +
    1.44 +  def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length }
    1.45 +
    1.46 +
    1.47 +  /* text content */
    1.48 +
    1.49 +  def content(body: Body): String =
    1.50 +  {
    1.51 +    val text = new StringBuilder(text_length(body))
    1.52 +    traverse_text(body)(()) { case (_, s) => text.append(s) }
    1.53 +    text.toString
    1.54 +  }
    1.55 +
    1.56 +  def content(tree: Tree): String = content(List(tree))
    1.57 +
    1.58 +
    1.59 +
    1.60 +  /** string representation **/
    1.61  
    1.62    def string_of_body(body: Body): String =
    1.63    {
    1.64 @@ -68,33 +120,6 @@
    1.65    def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
    1.66  
    1.67  
    1.68 -  /* traverse text */
    1.69 -
    1.70 -  def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A =
    1.71 -  {
    1.72 -    def traverse(x: A, t: Tree): A =
    1.73 -      t match {
    1.74 -        case Elem(_, ts) => (x /: ts)(traverse)
    1.75 -        case Text(s) => op(x, s)
    1.76 -      }
    1.77 -    (a /: body)(traverse)
    1.78 -  }
    1.79 -
    1.80 -  def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length }
    1.81 -
    1.82 -
    1.83 -  /* text content */
    1.84 -
    1.85 -  def content(body: Body): String =
    1.86 -  {
    1.87 -    val text = new StringBuilder(text_length(body))
    1.88 -    traverse_text(body)(()) { case (_, s) => text.append(s) }
    1.89 -    text.toString
    1.90 -  }
    1.91 -
    1.92 -  def content(tree: Tree): String = content(List(tree))
    1.93 -
    1.94 -
    1.95  
    1.96    /** cache for partial sharing (weak table) **/
    1.97