# HG changeset patch
# User wenzelm
# Date 1609848525 -3600
# Node ID 517b17e54d283f4130f5fd6d0dac2941b1effb41
# Parent  2138a4a9031ab8775086e7313eddc6724a3dd08a
tuned signature;

diff -r 2138a4a9031a -r 517b17e54d28 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Tue Jan 05 11:24:35 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Tue Jan 05 13:08:45 2021 +0100
@@ -67,42 +67,47 @@
     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
-    }
+  def make_html_body(xml: XML.Body): XML.Body =
+  {
+    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.forall(_ == XML.no_text)) XML.no_text
-    else if (html_div(html)) HTML.div(c, html)
-    else HTML.span(c, html)
+    def html_class(c: String, html: XML.Body): XML.Tree =
+      if (html.forall(_ == XML.no_text)) XML.no_text
+      else if (html_div(html)) HTML.div(c, html)
+      else HTML.span(c, html)
 
-  private def html_body(xml: XML.Body): XML.Body =
-    xml map {
-      case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(Markup.Language.DOCUMENT)), body) =>
-        html_class(Markup.Language.DOCUMENT, html_body(body))
-      case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) => HTML.par(html_body(body))
-      case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) => HTML.item(html_body(body))
-      case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => XML.no_text
-      case XML.Elem(Markup.Markdown_List(kind), body) =>
-        if (kind == Markup.ENUMERATE) HTML.enum(html_body(body)) else HTML.list(html_body(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_class(kind, html_body(body)))
-            case _ =>
-              html_body(body)
+    def html_body(xml_body: XML.Body): XML.Body =
+      xml_body map {
+        case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(Markup.Language.DOCUMENT)), body) =>
+          html_class(Markup.Language.DOCUMENT, html_body(body))
+        case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) => HTML.par(html_body(body))
+        case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) => HTML.item(html_body(body))
+        case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => XML.no_text
+        case XML.Elem(Markup.Markdown_List(kind), body) =>
+          if (kind == Markup.ENUMERATE) HTML.enum(html_body(body)) else HTML.list(html_body(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_class(kind, html_body(body)))
+              case _ =>
+                html_body(body)
+            }
+          Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match {
+            case Some(c) => html_class(c.toString, html)
+            case None => html_class(name, html)
           }
-        Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match {
-          case Some(c) => html_class(c.toString, html)
-          case None => html_class(name, html)
-        }
-      case XML.Text(text) =>
-        XML.Text(Symbol.decode(text))
-    }
+        case XML.Text(text) =>
+          XML.Text(Symbol.decode(text))
+      }
+
+    html_body(xml)
+  }
 
 
   /* PIDE HTML document */
@@ -127,7 +132,7 @@
         val title =
           if (name.is_theory) "Theory " + quote(name.theory_base_name)
           else "File " + Symbol.cartouche_decoded(name.path.file_name)
-        val body = html_body(snapshot.xml_markup(elements = html_elements))
+        val body = make_html_body(snapshot.xml_markup(elements = html_elements))
         html_context.html_document(title, body)
       }
     }
@@ -499,7 +504,7 @@
             val file_title = "File " + Symbol.cartouche_decoded(src_path.implode_short)
             HTML.write_document(file_path.dir, file_path.file_name,
               List(HTML.title(file_title)),
-              List(html_context.head(file_title), html_context.source(html_body(xml))))
+              List(html_context.head(file_title), html_context.source(make_html_body(xml))))
 
             List(HTML.link(file_name, HTML.text(file_title)))
           }