11 import scala.collection.immutable.SortedMap |
11 import scala.collection.immutable.SortedMap |
12 import scala.collection.mutable |
12 import scala.collection.mutable |
13 |
13 |
14 |
14 |
15 object Browser_Info { |
15 object Browser_Info { |
16 /** browser_info store configuration **/ |
16 /* browser_info store configuration */ |
17 |
17 |
18 object Config { |
18 object Config { |
19 val none: Config = new Config { def enabled: Boolean = false } |
19 val none: Config = new Config { def enabled: Boolean = false } |
20 val standard: Config = new Config { def enabled: Boolean = true } |
20 val standard: Config = new Config { def enabled: Boolean = true } |
21 |
21 |
32 abstract class Config private { |
32 abstract class Config private { |
33 def enabled: Boolean |
33 def enabled: Boolean |
34 def enabled(info: Sessions.Info): Boolean = enabled || info.browser_info |
34 def enabled(info: Sessions.Info): Boolean = enabled || info.browser_info |
35 def dir(store: Sessions.Store): Path = store.presentation_dir |
35 def dir(store: Sessions.Store): Path = store.presentation_dir |
36 } |
36 } |
|
37 |
|
38 |
|
39 /* presentation elements */ |
|
40 |
|
41 sealed case class Elements( |
|
42 html: Markup.Elements = Markup.Elements.empty, |
|
43 entity: Markup.Elements = Markup.Elements.empty, |
|
44 language: Markup.Elements = Markup.Elements.empty) |
|
45 |
|
46 val elements1: Elements = |
|
47 Elements( |
|
48 html = Rendering.foreground_elements ++ Rendering.text_color_elements + |
|
49 Markup.NUMERAL + Markup.COMMENT + Markup.ENTITY + Markup.LANGUAGE, |
|
50 entity = Markup.Elements(Markup.THEORY, Markup.TYPE_NAME, Markup.CONSTANT, Markup.FACT, |
|
51 Markup.CLASS, Markup.LOCALE, Markup.FREE)) |
|
52 |
|
53 val elements2: Elements = |
|
54 Elements( |
|
55 html = elements1.html ++ Rendering.markdown_elements, |
|
56 language = Markup.Elements(Markup.Language.DOCUMENT)) |
37 |
57 |
38 |
58 |
39 |
59 |
40 /** PDF/HTML presentation context **/ |
60 /** PDF/HTML presentation context **/ |
41 |
61 |
138 } |
158 } |
139 } |
159 } |
140 } |
160 } |
141 |
161 |
142 sealed case class HTML_Document(title: String, content: String) |
162 sealed case class HTML_Document(title: String, content: String) |
143 |
|
144 |
|
145 /* presentation elements */ |
|
146 |
|
147 sealed case class Elements( |
|
148 html: Markup.Elements = Markup.Elements.empty, |
|
149 entity: Markup.Elements = Markup.Elements.empty, |
|
150 language: Markup.Elements = Markup.Elements.empty) |
|
151 |
|
152 val elements1: Elements = |
|
153 Elements( |
|
154 html = Rendering.foreground_elements ++ Rendering.text_color_elements + |
|
155 Markup.NUMERAL + Markup.COMMENT + Markup.ENTITY + Markup.LANGUAGE, |
|
156 entity = Markup.Elements(Markup.THEORY, Markup.TYPE_NAME, Markup.CONSTANT, Markup.FACT, |
|
157 Markup.CLASS, Markup.LOCALE, Markup.FREE)) |
|
158 |
|
159 val elements2: Elements = |
|
160 Elements( |
|
161 html = elements1.html ++ Rendering.markdown_elements, |
|
162 language = Markup.Elements(Markup.Language.DOCUMENT)) |
|
163 |
163 |
164 |
164 |
165 /* formal entities */ |
165 /* formal entities */ |
166 |
166 |
167 object Theory_Ref { |
167 object Theory_Ref { |