src/Pure/Thy/html.scala
changeset 64356 ebbe7cf0c2b8
parent 64355 c6a1031cf925
child 64359 27739e1d7978
equal deleted inserted replaced
64355:c6a1031cf925 64356:ebbe7cf0c2b8
    79 
    79 
    80   def output(body: XML.Body): String = Library.make_string(output(body, _))
    80   def output(body: XML.Body): String = Library.make_string(output(body, _))
    81   def output(tree: XML.Tree): String = output(List(tree))
    81   def output(tree: XML.Tree): String = output(List(tree))
    82 
    82 
    83 
    83 
    84   /* structured markup */
    84   /* markup operators */
    85 
    85 
    86   def chapter(body: XML.Body): XML.Elem = XML.elem("h1", body)
    86   type Operator = XML.Body => XML.Elem
    87   def section(body: XML.Body): XML.Elem = XML.elem("h2", body)
    87 
    88   def subsection(body: XML.Body): XML.Elem = XML.elem("h3", body)
    88   val chapter: Operator = XML.elem("h1", _)
    89   def subsubsection(body: XML.Body): XML.Elem = XML.elem("h4", body)
    89   val section: Operator = XML.elem("h2", _)
    90   def paragraph(body: XML.Body): XML.Elem = XML.elem("h5", body)
    90   val subsection: Operator = XML.elem("h3", _)
    91   def subparagraph(body: XML.Body): XML.Elem = XML.elem("h6", body)
    91   val subsubsection: Operator = XML.elem("h4", _)
       
    92   val paragraph: Operator = XML.elem("h5", _)
       
    93   val subparagraph: Operator = XML.elem("h6", _)
    92 
    94 
    93 
    95 
    94   /* document */
    96   /* document */
    95 
    97 
    96   def begin_document(title: String): String =
    98   def begin_document(title: String): String =