# HG changeset patch
# User wenzelm
# Date 1661078476 -7200
# Node ID c7ee4d140c8046b1591147295a54850fabef9075
# Parent  abc3e052ba5d68e815faef711cecbc4c7b56f4c6
tuned sources and comments;

diff -r abc3e052ba5d -r c7ee4d140c80 src/Pure/Thy/browser_info.scala
--- a/src/Pure/Thy/browser_info.scala	Sun Aug 21 12:35:45 2022 +0200
+++ b/src/Pure/Thy/browser_info.scala	Sun Aug 21 12:41:16 2022 +0200
@@ -13,7 +13,7 @@
 
 
 object Browser_Info {
-  /** browser_info store configuration **/
+  /* browser_info store configuration */
 
   object Config {
     val none: Config = new Config { def enabled: Boolean = false }
@@ -36,6 +36,26 @@
   }
 
 
+  /* presentation elements */
+
+  sealed case class Elements(
+    html: Markup.Elements = Markup.Elements.empty,
+    entity: Markup.Elements = Markup.Elements.empty,
+    language: Markup.Elements = Markup.Elements.empty)
+
+  val elements1: Elements =
+    Elements(
+      html = Rendering.foreground_elements ++ Rendering.text_color_elements +
+        Markup.NUMERAL + Markup.COMMENT + Markup.ENTITY + Markup.LANGUAGE,
+      entity = Markup.Elements(Markup.THEORY, Markup.TYPE_NAME, Markup.CONSTANT, Markup.FACT,
+        Markup.CLASS, Markup.LOCALE, Markup.FREE))
+
+  val elements2: Elements =
+    Elements(
+      html = elements1.html ++ Rendering.markdown_elements,
+      language = Markup.Elements(Markup.Language.DOCUMENT))
+
+
 
   /** PDF/HTML presentation context **/
 
@@ -142,26 +162,6 @@
   sealed case class HTML_Document(title: String, content: String)
 
 
-  /* presentation elements */
-
-  sealed case class Elements(
-    html: Markup.Elements = Markup.Elements.empty,
-    entity: Markup.Elements = Markup.Elements.empty,
-    language: Markup.Elements = Markup.Elements.empty)
-
-  val elements1: Elements =
-    Elements(
-      html = Rendering.foreground_elements ++ Rendering.text_color_elements +
-        Markup.NUMERAL + Markup.COMMENT + Markup.ENTITY + Markup.LANGUAGE,
-      entity = Markup.Elements(Markup.THEORY, Markup.TYPE_NAME, Markup.CONSTANT, Markup.FACT,
-        Markup.CLASS, Markup.LOCALE, Markup.FREE))
-
-  val elements2: Elements =
-    Elements(
-      html = elements1.html ++ Rendering.markdown_elements,
-      language = Markup.Elements(Markup.Language.DOCUMENT))
-
-
   /* formal entities */
 
   object Theory_Ref {
@@ -336,7 +336,7 @@
 
 
 
-  /** HTML presentation **/
+  /** build presentation **/
 
   /* maintain chapter index */