equal
deleted
inserted
replaced
55 File_Format.registry.get_theory(thy_name).flatMap(_.make_theory_content(resources, thy_name)) |
55 File_Format.registry.get_theory(thy_name).flatMap(_.make_theory_content(resources, thy_name)) |
56 |
56 |
57 def is_hidden(name: Document.Node.Name): Boolean = |
57 def is_hidden(name: Document.Node.Name): Boolean = |
58 !name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name) |
58 !name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name) |
59 |
59 |
60 def file_preview(snapshot: Document.Snapshot): Option[Presentation.Preview] = |
60 def html_document(snapshot: Document.Snapshot): Option[Presentation.HTML_Document] = |
61 File_Format.registry.get(snapshot.node_name).flatMap(_.make_preview(snapshot)) |
61 File_Format.registry.get(snapshot.node_name).flatMap(_.html_document(snapshot)) |
62 |
62 |
63 |
63 |
64 /* file-system operations */ |
64 /* file-system operations */ |
65 |
65 |
66 def append(dir: String, source_path: Path): String = |
66 def append(dir: String, source_path: Path): String = |