more operations;
authorwenzelm
Sun May 07 16:04:19 2017 +0200 (2017-05-07)
changeset 65753787e5ee6ef53
parent 65752 ed7b5cd3a7f2
child 65754 05c6a29c9132
more operations;
tuned;
src/Pure/PIDE/markup.scala
src/Pure/PIDE/xml.scala
src/Pure/Thy/html.scala
     1.1 --- a/src/Pure/PIDE/markup.scala	Sun May 07 13:42:20 2017 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Sun May 07 16:04:19 2017 +0200
     1.3 @@ -634,4 +634,7 @@
     1.4    def update_properties(more_props: Properties.T): Markup =
     1.5      if (more_props.isEmpty) this
     1.6      else Markup(name, (more_props :\ properties) { case (p, ps) => Properties.put(ps, p) })
     1.7 +
     1.8 +  def + (entry: Properties.Entry): Markup =
     1.9 +    Markup(name, Properties.put(properties, entry))
    1.10  }
     2.1 --- a/src/Pure/PIDE/xml.scala	Sun May 07 13:42:20 2017 +0200
     2.2 +++ b/src/Pure/PIDE/xml.scala	Sun May 07 16:04:19 2017 +0200
     2.3 @@ -18,6 +18,7 @@
     2.4  
     2.5    /* datatype representation */
     2.6  
     2.7 +  type Attribute = Properties.Entry
     2.8    type Attributes = Properties.T
     2.9  
    2.10    sealed abstract class Tree { override def toString: String = string_of_tree(this) }
    2.11 @@ -25,9 +26,12 @@
    2.12    case class Elem(markup: Markup, body: Body) extends Tree
    2.13    {
    2.14      def name: String = markup.name
    2.15 +
    2.16      def update_attributes(more_attributes: Attributes): Elem =
    2.17        if (more_attributes.isEmpty) this
    2.18        else Elem(markup.update_properties(more_attributes), body)
    2.19 +
    2.20 +    def + (att: Attribute): Tree = Elem(markup + att, body)
    2.21    }
    2.22    case class Text(content: String) extends Tree
    2.23  
     3.1 --- a/src/Pure/Thy/html.scala	Sun May 07 13:42:20 2017 +0200
     3.2 +++ b/src/Pure/Thy/html.scala	Sun May 07 16:04:19 2017 +0200
     3.3 @@ -81,9 +81,15 @@
     3.4    def output(tree: XML.Tree): String = output(List(tree))
     3.5  
     3.6  
     3.7 +  /* attributes */
     3.8 +
     3.9 +  def id(s: String): Properties.Entry = ("id" -> s)
    3.10 +
    3.11 +
    3.12    /* structured markup operators */
    3.13  
    3.14    def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt))
    3.15 +  val break: XML.Body = List(XML.elem("br"))
    3.16  
    3.17    class Operator(name: String)
    3.18    { def apply(body: XML.Body): XML.Elem = XML.elem(name, body) }
    3.19 @@ -93,6 +99,7 @@
    3.20  
    3.21    val div = new Operator("div")
    3.22    val span = new Operator("span")
    3.23 +  val pre = new Operator("pre")
    3.24    val par = new Operator("p")
    3.25    val emph = new Operator("em")
    3.26    val bold = new Operator("b")
    3.27 @@ -117,6 +124,9 @@
    3.28    def link(href: String, body: XML.Body = Nil): XML.Elem =
    3.29      XML.Elem(Markup("a", List("href" -> href)), if (body.isEmpty) text(href) else body)
    3.30  
    3.31 +  def image(src: String, alt: String = ""): XML.Elem =
    3.32 +    XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil)
    3.33 +
    3.34  
    3.35    /* document */
    3.36  
    3.37 @@ -157,9 +167,7 @@
    3.38    private def session_entry(entry: (String, String)): String =
    3.39    {
    3.40      val (name, description) = entry
    3.41 -    val descr =
    3.42 -      if (description == "") Nil
    3.43 -      else List(XML.elem("br"), XML.elem("pre", List(XML.Text(description))))
    3.44 +    val descr = if (description == "") Nil else break ::: List(pre(text(description)))
    3.45      XML.string_of_tree(
    3.46        XML.elem("li",
    3.47          List(XML.Elem(Markup("a", List(("href", name + "/index.html"))),