equal
deleted
inserted
replaced
21 resources => |
21 resources => |
22 |
22 |
23 |
23 |
24 /* file formats */ |
24 /* file formats */ |
25 |
25 |
26 val file_formats: File_Format.Environment = File_Format.environment() |
|
27 |
|
28 def make_theory_name(name: Document.Node.Name): Option[Document.Node.Name] = |
26 def make_theory_name(name: Document.Node.Name): Option[Document.Node.Name] = |
29 file_formats.get(name).flatMap(_.make_theory_name(resources, name)) |
27 File_Format.registry.get(name).flatMap(_.make_theory_name(resources, name)) |
30 |
28 |
31 def make_theory_content(thy_name: Document.Node.Name): Option[String] = |
29 def make_theory_content(thy_name: Document.Node.Name): Option[String] = |
32 file_formats.get_theory(thy_name).flatMap(_.make_theory_content(resources, thy_name)) |
30 File_Format.registry.get_theory(thy_name).flatMap(_.make_theory_content(resources, thy_name)) |
33 |
31 |
34 def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] = |
32 def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] = |
35 file_formats.get(snapshot.node_name).flatMap(_.make_preview(snapshot)) |
33 File_Format.registry.get(snapshot.node_name).flatMap(_.make_preview(snapshot)) |
36 |
34 |
37 def is_hidden(name: Document.Node.Name): Boolean = |
35 def is_hidden(name: Document.Node.Name): Boolean = |
38 !name.is_theory || name.theory == Sessions.root_name || file_formats.is_theory(name) |
36 !name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name) |
39 |
37 |
40 def thy_path(path: Path): Path = path.ext("thy") |
38 def thy_path(path: Path): Path = path.ext("thy") |
41 |
39 |
42 |
40 |
43 /* file-system operations */ |
41 /* file-system operations */ |