--- a/src/Pure/Thy/browser_info.scala Sun Aug 21 12:19:38 2022 +0200
+++ b/src/Pure/Thy/browser_info.scala Sun Aug 21 12:23:17 2022 +0200
@@ -13,9 +13,31 @@
object Browser_Info {
- /** HTML documents **/
+ /** browser_info store configuration **/
+
+ object Config {
+ val none: Config = new Config { def enabled: Boolean = false }
+ val standard: Config = new Config { def enabled: Boolean = true }
+
+ def dir(path: Path): Config =
+ new Config {
+ def enabled: Boolean = true
+ override def dir(store: Sessions.Store): Path = path
+ }
- /* PDF/HTML presentation context */
+ def make(s: String): Config =
+ if (s == ":") standard else dir(Path.explode(s))
+ }
+
+ abstract class Config private {
+ def enabled: Boolean
+ def enabled(info: Sessions.Info): Boolean = enabled || info.browser_info
+ def dir(store: Sessions.Store): Path = store.presentation_dir
+ }
+
+
+
+ /** PDF/HTML presentation context **/
def context(
sessions_structure: Sessions.Structure,
@@ -317,29 +339,6 @@
/** HTML presentation **/
- /* browser_info store configuration */
-
- object Config {
- val none: Config = new Config { def enabled: Boolean = false }
- val standard: Config = new Config { def enabled: Boolean = true }
-
- def dir(path: Path): Config =
- new Config {
- def enabled: Boolean = true
- override def dir(store: Sessions.Store): Path = path
- }
-
- def make(s: String): Config =
- if (s == ":") standard else dir(Path.explode(s))
- }
-
- abstract class Config private {
- def enabled: Boolean
- def enabled(info: Sessions.Info): Boolean = enabled || info.browser_info
- def dir(store: Sessions.Store): Path = store.presentation_dir
- }
-
-
/* maintain chapter index */
private val sessions_path = Path.basic(".sessions")