equal
deleted
inserted
replaced
11 |
11 |
12 import java.io.{File => JFile} |
12 import java.io.{File => JFile} |
13 |
13 |
14 |
14 |
15 object Resources { |
15 object Resources { |
16 def empty: Resources = |
16 def empty: Resources = new Resources(Sessions.Structure.empty, Sessions.bootstrap_base) |
17 new Resources(Sessions.Structure.empty, Sessions.Structure.empty.bootstrap) |
|
18 |
17 |
19 def hidden_node(name: Document.Node.Name): Boolean = |
18 def hidden_node(name: Document.Node.Name): Boolean = |
20 !name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name) |
19 !name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name) |
21 |
20 |
22 def html_document(snapshot: Document.Snapshot): Option[Browser_Info.HTML_Document] = |
21 def html_document(snapshot: Document.Snapshot): Option[Browser_Info.HTML_Document] = |