# HG changeset patch # User wenzelm # Date 1515009313 -3600 # Node ID 3ee6da3781835894eadb460351e5ae0bdc4e135c # Parent 641d7da6ff96634b0a59c08604bc1e5f4772d205 HTML output for Markdown elements; clarified HTML operations; diff -r 641d7da6ff96 -r 3ee6da378183 etc/isabelle.css --- a/etc/isabelle.css Wed Jan 03 11:06:41 2018 +0100 +++ b/etc/isabelle.css Wed Jan 03 20:55:13 2018 +0100 @@ -23,6 +23,7 @@ .theories { background-color: #FFFFFF; padding: 10px; } .sessions { background-color: #FFFFFF; padding: 10px; } +.document { white-space: normal; font-family: sans-serif; } .name { font-style: italic; } .filename { font-family: fixed; } diff -r 641d7da6ff96 -r 3ee6da378183 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Wed Jan 03 11:06:41 2018 +0100 +++ b/src/Pure/PIDE/markup.ML Wed Jan 03 20:55:13 2018 +0100 @@ -123,8 +123,11 @@ val text_foldN: string val text_fold: T val markdown_paragraphN: string val markdown_paragraph: T val markdown_itemN: string val markdown_item: T + val markdown_bulletN: string val markdown_bullet: int -> T val markdown_listN: string val markdown_list: string -> T - val markdown_bulletN: string val markdown_bullet: int -> T + val itemizeN: string + val enumerateN: string + val descriptionN: string val inputN: string val input: bool -> Properties.T -> T val command_keywordN: string val command_keyword: T val commandN: string val command_properties: T -> T @@ -475,8 +478,12 @@ val (markdown_paragraphN, markdown_paragraph) = markup_elem "markdown_paragraph"; val (markdown_itemN, markdown_item) = markup_elem "markdown_item"; +val (markdown_bulletN, markdown_bullet) = markup_int "markdown_bullet" "depth"; val (markdown_listN, markdown_list) = markup_string "markdown_list" kindN; -val (markdown_bulletN, markdown_bullet) = markup_int "markdown_bullet" "depth"; + +val itemizeN = "itemize"; +val enumerateN = "enumerate"; +val descriptionN = "description"; (* formal input *) diff -r 641d7da6ff96 -r 3ee6da378183 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Wed Jan 03 11:06:41 2018 +0100 +++ b/src/Pure/PIDE/markup.scala Wed Jan 03 20:55:13 2018 +0100 @@ -161,6 +161,7 @@ val LANGUAGE = "language" object Language { + val DOCUMENT = "document" val ML = "ML" val SML = "SML" val PATH = "path" @@ -297,8 +298,12 @@ val MARKDOWN_PARAGRAPH = "markdown_paragraph" val MARKDOWN_ITEM = "markdown_item" + val Markdown_Bullet = new Markup_Int("markdown_bullet", "depth") val Markdown_List = new Markup_String("markdown_list", "kind") - val Markdown_Bullet = new Markup_Int("markdown_bullet", "depth") + + val ITEMIZE = "itemize" + val ENUMERATE = "enumerate" + val DESCRIPTION = "description" /* ML */ diff -r 641d7da6ff96 -r 3ee6da378183 src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Wed Jan 03 11:06:41 2018 +0100 +++ b/src/Pure/PIDE/rendering.scala Wed Jan 03 20:55:13 2018 +0100 @@ -207,6 +207,10 @@ val caret_focus_elements = Markup.Elements(Markup.ENTITY) val antiquoted_elements = Markup.Elements(Markup.ANTIQUOTED) + + val markdown_elements = + Markup.Elements(Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name, + Markup.Markdown_Bullet.name) } abstract class Rendering( diff -r 641d7da6ff96 -r 3ee6da378183 src/Pure/Thy/html.scala --- a/src/Pure/Thy/html.scala Wed Jan 03 11:06:41 2018 +0100 +++ b/src/Pure/Thy/html.scala Wed Jan 03 20:55:13 2018 +0100 @@ -153,6 +153,7 @@ /* structured markup operators */ def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt)) + val no_text: XML.Tree = XML.Text("") val break: XML.Body = List(XML.elem("br")) class Operator(val name: String) @@ -176,6 +177,12 @@ val emph = new Operator("em") val bold = new Operator("b") val code = new Operator("code") + val item = new Operator("li") + val list = new Operator("ul") + val enum = new Operator("ol") + val descr = new Operator("dl") + val dt = new Operator("dt") + val dd = new Operator("dd") val title = new Heading("title") val chapter = new Heading("h1") @@ -185,14 +192,10 @@ val paragraph = new Heading("h5") val subparagraph = new Heading("h6") - def itemize(items: List[XML.Body]): XML.Elem = - XML.elem("ul", items.map(XML.elem("li", _))) - - def enumerate(items: List[XML.Body]): XML.Elem = - XML.elem("ol", items.map(XML.elem("li", _))) - + def itemize(items: List[XML.Body]): XML.Elem = list(items.map(item(_))) + def enumerate(items: List[XML.Body]): XML.Elem = enum(items.map(item(_))) def description(items: List[(XML.Body, XML.Body)]): XML.Elem = - XML.elem("dl", items.flatMap({ case (x, y) => List(XML.elem("dt", x), XML.elem("dd", y)) })) + descr(items.flatMap({ case (x, y) => List(dt(x), dd(y)) })) def link(href: String, body: XML.Body = Nil): XML.Elem = XML.Elem(Markup("a", List("href" -> href)), if (body.isEmpty) text(href) else body) diff -r 641d7da6ff96 -r 3ee6da378183 src/Pure/Thy/markdown.ML --- a/src/Pure/Thy/markdown.ML Wed Jan 03 11:06:41 2018 +0100 +++ b/src/Pure/Thy/markdown.ML Wed Jan 03 20:55:13 2018 +0100 @@ -43,9 +43,9 @@ datatype kind = Itemize | Enumerate | Description; -fun print_kind Itemize = "itemize" - | print_kind Enumerate = "enumerate" - | print_kind Description = "description"; +fun print_kind Itemize = Markup.itemizeN + | print_kind Enumerate = Markup.enumerateN + | print_kind Description = Markup.descriptionN; val kinds = [("item", Itemize), ("enum", Enumerate), ("descr", Description)]; diff -r 641d7da6ff96 -r 3ee6da378183 src/Pure/Thy/present.scala --- a/src/Pure/Thy/present.scala Wed Jan 03 11:06:41 2018 +0100 +++ b/src/Pure/Thy/present.scala Wed Jan 03 20:55:13 2018 +0100 @@ -145,32 +145,51 @@ /* PIDE document */ - private val document_span_elements = - Rendering.foreground_elements ++ Rendering.text_color_elements + Markup.NUMERAL + Markup.COMMENT + private val document_elements = + Rendering.foreground_elements ++ Rendering.text_color_elements ++ Rendering.markdown_elements + + Markup.NUMERAL + Markup.COMMENT + Markup.LANGUAGE + + private val div_elements = + Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name, + HTML.descr.name) + + private def html_div(html: XML.Body): Boolean = + html exists { + case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body) + case XML.Text(_) => false + } + + private def html_class(c: String, html: XML.Body): XML.Tree = + if (html_div(html)) HTML.div(c, html) else HTML.span(c, html) private def make_html(xml: XML.Body): XML.Body = xml map { - case XML.Wrapped_Elem(markup, body1, body2) => - XML.Wrapped_Elem(markup, make_html(body1), make_html(body2)) + case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(Markup.Language.DOCUMENT)), body) => + html_class(Markup.Language.DOCUMENT, make_html(body)) + case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) => HTML.par(make_html(body)) + case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) => HTML.item(make_html(body)) + case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => HTML.no_text + case XML.Elem(Markup.Markdown_List(kind), body) => + if (kind == Markup.ENUMERATE) HTML.enum(make_html(body)) else HTML.list(make_html(body)) case XML.Elem(markup, body) => val name = markup.name val html = markup.properties match { case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD => - List(HTML.span(kind, make_html(body))) + List(html_class(kind, make_html(body))) case _ => make_html(body) } Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match { - case Some(c) => HTML.span(c.toString, html) - case None => HTML.span(name, html) + case Some(c) => html_class(c.toString, html) + case None => html_class(name, html) } case XML.Text(text) => XML.Text(Symbol.decode(text)) } def pide_document(snapshot: Document.Snapshot): XML.Body = - make_html(snapshot.markup_to_XML(Text.Range.full, document_span_elements)) + make_html(snapshot.markup_to_XML(Text.Range.full, document_elements))