src/Pure/Thy/html.scala
changeset 38573 d163f0f28e8c
parent 38444 796904799f4d
child 43455 4b4b93672f15
     1.1 --- a/src/Pure/Thy/html.scala	Sun Aug 22 12:54:12 2010 +0200
     1.2 +++ b/src/Pure/Thy/html.scala	Sun Aug 22 13:52:24 2010 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4  
     1.5    // document markup
     1.6  
     1.7 -  def span(cls: String, body: List[XML.Tree]): XML.Elem =
     1.8 +  def span(cls: String, body: XML.Body): XML.Elem =
     1.9      XML.Elem(Markup(SPAN, List((CLASS, cls))), body)
    1.10  
    1.11    def hidden(txt: String): XML.Elem =
    1.12 @@ -50,9 +50,9 @@
    1.13    def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
    1.14    def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
    1.15  
    1.16 -  def spans(input: XML.Tree, original_data: Boolean = false): List[XML.Tree] =
    1.17 +  def spans(input: XML.Tree, original_data: Boolean = false): XML.Body =
    1.18    {
    1.19 -    def html_spans(tree: XML.Tree): List[XML.Tree] =
    1.20 +    def html_spans(tree: XML.Tree): XML.Body =
    1.21        tree match {
    1.22          case XML.Elem(Markup(name, _), ts) =>
    1.23            if (original_data)