removed obsolete org.w3c.dom operations;
authorwenzelm
Thu Sep 27 15:55:38 2012 +0200 (2012-09-27 ago)
changeset 496132f6986e2ef06
parent 49612 e6a53d203362
child 49614 0009a6ebc83b
removed obsolete org.w3c.dom operations;
src/Pure/PIDE/markup.scala
src/Pure/PIDE/xml.scala
src/Pure/Thy/html.scala
     1.1 --- a/src/Pure/PIDE/markup.scala	Thu Sep 27 15:38:28 2012 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Thu Sep 27 15:55:38 2012 +0200
     1.3 @@ -22,7 +22,6 @@
     1.4    /* elements */
     1.5  
     1.6    val Empty = Markup("", Nil)
     1.7 -  val Data = Markup("data", Nil)
     1.8    val Broken = Markup("broken", Nil)
     1.9  }
    1.10  
     2.1 --- a/src/Pure/PIDE/xml.scala	Thu Sep 27 15:38:28 2012 +0200
     2.2 +++ b/src/Pure/PIDE/xml.scala	Thu Sep 27 15:55:38 2012 +0200
     2.3 @@ -7,7 +7,6 @@
     2.4  
     2.5  package isabelle
     2.6  
     2.7 -import java.lang.System
     2.8  import java.util.WeakHashMap
     2.9  import java.lang.ref.WeakReference
    2.10  import javax.xml.parsers.DocumentBuilderFactory
    2.11 @@ -171,35 +170,6 @@
    2.12  
    2.13  
    2.14  
    2.15 -  /** document object model (W3C DOM) **/
    2.16 -
    2.17 -  def get_data(node: org.w3c.dom.Node): Option[XML.Tree] =
    2.18 -    node.getUserData(Markup.Data.name) match {
    2.19 -      case tree: XML.Tree => Some(tree)
    2.20 -      case _ => None
    2.21 -    }
    2.22 -
    2.23 -  def document_node(doc: org.w3c.dom.Document, tree: Tree): org.w3c.dom.Node =
    2.24 -  {
    2.25 -    def DOM(tr: Tree): org.w3c.dom.Node = tr match {
    2.26 -      case Elem(Markup.Data, List(data, t)) =>
    2.27 -        val node = DOM(t)
    2.28 -        node.setUserData(Markup.Data.name, data, null)
    2.29 -        node
    2.30 -      case Elem(Markup(name, atts), ts) =>
    2.31 -        if (name == Markup.Data.name)
    2.32 -          error("Malformed data element: " + tr.toString)
    2.33 -        val node = doc.createElement(name)
    2.34 -        for ((name, value) <- atts) node.setAttribute(name, value)
    2.35 -        for (t <- ts) node.appendChild(DOM(t))
    2.36 -        node
    2.37 -      case Text(txt) => doc.createTextNode(txt)
    2.38 -    }
    2.39 -    DOM(tree)
    2.40 -  }
    2.41 -
    2.42 -
    2.43 -
    2.44    /** XML as data representation language **/
    2.45  
    2.46    class XML_Atom(s: String) extends Exception(s)
     3.1 --- a/src/Pure/Thy/html.scala	Thu Sep 27 15:38:28 2012 +0200
     3.2 +++ b/src/Pure/Thy/html.scala	Thu Sep 27 15:55:38 2012 +0200
     3.3 @@ -29,6 +29,8 @@
     3.4    }
     3.5  
     3.6  
     3.7 +  /// FIXME unused stuff
     3.8 +
     3.9    // common elements and attributes
    3.10  
    3.11    val BODY = "body"
    3.12 @@ -55,14 +57,12 @@
    3.13    def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
    3.14    def bold(txt: String): XML.Elem = span("bold", List(XML.Text(txt)))
    3.15  
    3.16 -  def spans(input: XML.Tree, original_data: Boolean = false): XML.Body =
    3.17 +  def spans(input: XML.Tree): XML.Body =
    3.18    {
    3.19      def html_spans(tree: XML.Tree): XML.Body =
    3.20        tree match {
    3.21          case XML.Elem(m @ Markup(name, props), ts) =>
    3.22 -          val html_span = span(name, ts.flatMap(html_spans))
    3.23 -          if (original_data) List(XML.Elem(Markup.Data, List(tree, html_span)))
    3.24 -          else List(html_span)
    3.25 +          List(span(name, ts.flatMap(html_spans)))
    3.26          case XML.Text(txt) =>
    3.27            val ts = new ListBuffer[XML.Tree]
    3.28            val t = new StringBuilder