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