equal
deleted
inserted
replaced
17 val session_base: Sessions.Base, |
17 val session_base: Sessions.Base, |
18 val log: Logger = No_Logger) |
18 val log: Logger = No_Logger) |
19 { |
19 { |
20 resources => |
20 resources => |
21 |
21 |
22 |
|
23 /* theory files */ |
|
24 |
|
25 def thy_path(path: Path): Path = path.ext("thy") |
22 def thy_path(path: Path): Path = path.ext("thy") |
26 |
|
27 def thy_node_name(qualifier: String, file: JFile, bootstrap: Boolean = false) |
|
28 : Document.Node.Name = |
|
29 { |
|
30 session_base.known.get_file(file, bootstrap) getOrElse { |
|
31 val node = file.getPath |
|
32 theory_name(qualifier, Thy_Header.theory_name(node)) match { |
|
33 case (true, theory) => Document.Node.Name.loaded_theory(theory) |
|
34 case (false, theory) => |
|
35 val master_dir = if (theory == "") "" else file.getParent |
|
36 Document.Node.Name(node, master_dir, theory) |
|
37 } |
|
38 } |
|
39 } |
|
40 |
23 |
41 |
24 |
42 /* file-system operations */ |
25 /* file-system operations */ |
43 |
26 |
44 def append(dir: String, source_path: Path): String = |
27 def append(dir: String, source_path: Path): String = |