HTML output for Markdown elements;
clarified HTML operations;

--- 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; }

--- 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 *)

--- 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 */

--- 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(

--- 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)

--- 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)];
 

--- 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))