HTML output for Markdown elements;
authorwenzelm
Wed Jan 03 20:55:13 2018 +0100 (23 months ago ago)
changeset 673363ee6da378183
parent 67335 641d7da6ff96
child 67337 4254cfd15b00
HTML output for Markdown elements;
clarified HTML operations;
etc/isabelle.css
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/rendering.scala
src/Pure/Thy/html.scala
src/Pure/Thy/markdown.ML
src/Pure/Thy/present.scala
     1.1 --- a/etc/isabelle.css	Wed Jan 03 11:06:41 2018 +0100
     1.2 +++ b/etc/isabelle.css	Wed Jan 03 20:55:13 2018 +0100
     1.3 @@ -23,6 +23,7 @@
     1.4  
     1.5  .theories { background-color: #FFFFFF; padding: 10px; }
     1.6  .sessions { background-color: #FFFFFF; padding: 10px; }
     1.7 +.document { white-space: normal; font-family: sans-serif; }
     1.8  
     1.9  .name     { font-style: italic; }
    1.10  .filename { font-family: fixed; }
     2.1 --- a/src/Pure/PIDE/markup.ML	Wed Jan 03 11:06:41 2018 +0100
     2.2 +++ b/src/Pure/PIDE/markup.ML	Wed Jan 03 20:55:13 2018 +0100
     2.3 @@ -123,8 +123,11 @@
     2.4    val text_foldN: string val text_fold: T
     2.5    val markdown_paragraphN: string val markdown_paragraph: T
     2.6    val markdown_itemN: string val markdown_item: T
     2.7 +  val markdown_bulletN: string val markdown_bullet: int -> T
     2.8    val markdown_listN: string val markdown_list: string -> T
     2.9 -  val markdown_bulletN: string val markdown_bullet: int -> T
    2.10 +  val itemizeN: string
    2.11 +  val enumerateN: string
    2.12 +  val descriptionN: string
    2.13    val inputN: string val input: bool -> Properties.T -> T
    2.14    val command_keywordN: string val command_keyword: T
    2.15    val commandN: string val command_properties: T -> T
    2.16 @@ -475,8 +478,12 @@
    2.17  
    2.18  val (markdown_paragraphN, markdown_paragraph) = markup_elem "markdown_paragraph";
    2.19  val (markdown_itemN, markdown_item) = markup_elem "markdown_item";
    2.20 +val (markdown_bulletN, markdown_bullet) = markup_int "markdown_bullet" "depth";
    2.21  val (markdown_listN, markdown_list) = markup_string "markdown_list" kindN;
    2.22 -val (markdown_bulletN, markdown_bullet) = markup_int "markdown_bullet" "depth";
    2.23 +
    2.24 +val itemizeN = "itemize";
    2.25 +val enumerateN = "enumerate";
    2.26 +val descriptionN = "description";
    2.27  
    2.28  
    2.29  (* formal input *)
     3.1 --- a/src/Pure/PIDE/markup.scala	Wed Jan 03 11:06:41 2018 +0100
     3.2 +++ b/src/Pure/PIDE/markup.scala	Wed Jan 03 20:55:13 2018 +0100
     3.3 @@ -161,6 +161,7 @@
     3.4    val LANGUAGE = "language"
     3.5    object Language
     3.6    {
     3.7 +    val DOCUMENT = "document"
     3.8      val ML = "ML"
     3.9      val SML = "SML"
    3.10      val PATH = "path"
    3.11 @@ -297,8 +298,12 @@
    3.12  
    3.13    val MARKDOWN_PARAGRAPH = "markdown_paragraph"
    3.14    val MARKDOWN_ITEM = "markdown_item"
    3.15 +  val Markdown_Bullet = new Markup_Int("markdown_bullet", "depth")
    3.16    val Markdown_List = new Markup_String("markdown_list", "kind")
    3.17 -  val Markdown_Bullet = new Markup_Int("markdown_bullet", "depth")
    3.18 +
    3.19 +  val ITEMIZE = "itemize"
    3.20 +  val ENUMERATE = "enumerate"
    3.21 +  val DESCRIPTION = "description"
    3.22  
    3.23  
    3.24    /* ML */
     4.1 --- a/src/Pure/PIDE/rendering.scala	Wed Jan 03 11:06:41 2018 +0100
     4.2 +++ b/src/Pure/PIDE/rendering.scala	Wed Jan 03 20:55:13 2018 +0100
     4.3 @@ -207,6 +207,10 @@
     4.4    val caret_focus_elements = Markup.Elements(Markup.ENTITY)
     4.5  
     4.6    val antiquoted_elements = Markup.Elements(Markup.ANTIQUOTED)
     4.7 +
     4.8 +  val markdown_elements =
     4.9 +    Markup.Elements(Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name,
    4.10 +      Markup.Markdown_Bullet.name)
    4.11  }
    4.12  
    4.13  abstract class Rendering(
     5.1 --- a/src/Pure/Thy/html.scala	Wed Jan 03 11:06:41 2018 +0100
     5.2 +++ b/src/Pure/Thy/html.scala	Wed Jan 03 20:55:13 2018 +0100
     5.3 @@ -153,6 +153,7 @@
     5.4    /* structured markup operators */
     5.5  
     5.6    def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt))
     5.7 +  val no_text: XML.Tree = XML.Text("")
     5.8    val break: XML.Body = List(XML.elem("br"))
     5.9  
    5.10    class Operator(val name: String)
    5.11 @@ -176,6 +177,12 @@
    5.12    val emph = new Operator("em")
    5.13    val bold = new Operator("b")
    5.14    val code = new Operator("code")
    5.15 +  val item = new Operator("li")
    5.16 +  val list = new Operator("ul")
    5.17 +  val enum = new Operator("ol")
    5.18 +  val descr = new Operator("dl")
    5.19 +  val dt = new Operator("dt")
    5.20 +  val dd = new Operator("dd")
    5.21  
    5.22    val title = new Heading("title")
    5.23    val chapter = new Heading("h1")
    5.24 @@ -185,14 +192,10 @@
    5.25    val paragraph = new Heading("h5")
    5.26    val subparagraph = new Heading("h6")
    5.27  
    5.28 -  def itemize(items: List[XML.Body]): XML.Elem =
    5.29 -    XML.elem("ul", items.map(XML.elem("li", _)))
    5.30 -
    5.31 -  def enumerate(items: List[XML.Body]): XML.Elem =
    5.32 -    XML.elem("ol", items.map(XML.elem("li", _)))
    5.33 -
    5.34 +  def itemize(items: List[XML.Body]): XML.Elem = list(items.map(item(_)))
    5.35 +  def enumerate(items: List[XML.Body]): XML.Elem = enum(items.map(item(_)))
    5.36    def description(items: List[(XML.Body, XML.Body)]): XML.Elem =
    5.37 -    XML.elem("dl", items.flatMap({ case (x, y) => List(XML.elem("dt", x), XML.elem("dd", y)) }))
    5.38 +    descr(items.flatMap({ case (x, y) => List(dt(x), dd(y)) }))
    5.39  
    5.40    def link(href: String, body: XML.Body = Nil): XML.Elem =
    5.41      XML.Elem(Markup("a", List("href" -> href)), if (body.isEmpty) text(href) else body)
     6.1 --- a/src/Pure/Thy/markdown.ML	Wed Jan 03 11:06:41 2018 +0100
     6.2 +++ b/src/Pure/Thy/markdown.ML	Wed Jan 03 20:55:13 2018 +0100
     6.3 @@ -43,9 +43,9 @@
     6.4  
     6.5  datatype kind = Itemize | Enumerate | Description;
     6.6  
     6.7 -fun print_kind Itemize = "itemize"
     6.8 -  | print_kind Enumerate = "enumerate"
     6.9 -  | print_kind Description = "description";
    6.10 +fun print_kind Itemize = Markup.itemizeN
    6.11 +  | print_kind Enumerate = Markup.enumerateN
    6.12 +  | print_kind Description = Markup.descriptionN;
    6.13  
    6.14  val kinds = [("item", Itemize), ("enum", Enumerate), ("descr", Description)];
    6.15  
     7.1 --- a/src/Pure/Thy/present.scala	Wed Jan 03 11:06:41 2018 +0100
     7.2 +++ b/src/Pure/Thy/present.scala	Wed Jan 03 20:55:13 2018 +0100
     7.3 @@ -145,32 +145,51 @@
     7.4  
     7.5    /* PIDE document */
     7.6  
     7.7 -  private val document_span_elements =
     7.8 -    Rendering.foreground_elements ++ Rendering.text_color_elements + Markup.NUMERAL + Markup.COMMENT
     7.9 +  private val document_elements =
    7.10 +    Rendering.foreground_elements ++ Rendering.text_color_elements ++ Rendering.markdown_elements +
    7.11 +    Markup.NUMERAL + Markup.COMMENT + Markup.LANGUAGE
    7.12 +
    7.13 +  private val div_elements =
    7.14 +    Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name,
    7.15 +      HTML.descr.name)
    7.16 +
    7.17 +  private def html_div(html: XML.Body): Boolean =
    7.18 +    html exists {
    7.19 +      case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body)
    7.20 +      case XML.Text(_) => false
    7.21 +    }
    7.22 +
    7.23 +  private def html_class(c: String, html: XML.Body): XML.Tree =
    7.24 +    if (html_div(html)) HTML.div(c, html) else HTML.span(c, html)
    7.25  
    7.26    private def make_html(xml: XML.Body): XML.Body =
    7.27      xml map {
    7.28 -      case XML.Wrapped_Elem(markup, body1, body2) =>
    7.29 -        XML.Wrapped_Elem(markup, make_html(body1), make_html(body2))
    7.30 +      case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(Markup.Language.DOCUMENT)), body) =>
    7.31 +        html_class(Markup.Language.DOCUMENT, make_html(body))
    7.32 +      case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) => HTML.par(make_html(body))
    7.33 +      case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) => HTML.item(make_html(body))
    7.34 +      case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => HTML.no_text
    7.35 +      case XML.Elem(Markup.Markdown_List(kind), body) =>
    7.36 +        if (kind == Markup.ENUMERATE) HTML.enum(make_html(body)) else HTML.list(make_html(body))
    7.37        case XML.Elem(markup, body) =>
    7.38          val name = markup.name
    7.39          val html =
    7.40            markup.properties match {
    7.41              case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD =>
    7.42 -              List(HTML.span(kind, make_html(body)))
    7.43 +              List(html_class(kind, make_html(body)))
    7.44              case _ =>
    7.45                make_html(body)
    7.46            }
    7.47          Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match {
    7.48 -          case Some(c) => HTML.span(c.toString, html)
    7.49 -          case None => HTML.span(name, html)
    7.50 +          case Some(c) => html_class(c.toString, html)
    7.51 +          case None => html_class(name, html)
    7.52          }
    7.53        case XML.Text(text) =>
    7.54          XML.Text(Symbol.decode(text))
    7.55      }
    7.56  
    7.57    def pide_document(snapshot: Document.Snapshot): XML.Body =
    7.58 -    make_html(snapshot.markup_to_XML(Text.Range.full, document_span_elements))
    7.59 +    make_html(snapshot.markup_to_XML(Text.Range.full, document_elements))
    7.60  
    7.61  
    7.62