equal
deleted
inserted
replaced
20 class JEdit_Thy_Load(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax) |
20 class JEdit_Thy_Load(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax) |
21 extends Thy_Load(loaded_theories, base_syntax) |
21 extends Thy_Load(loaded_theories, base_syntax) |
22 { |
22 { |
23 /* document node names */ |
23 /* document node names */ |
24 |
24 |
25 def dummy_node_name(buffer: Buffer): Document.Node.Name = |
|
26 Document.Node.Name(JEdit_Lib.buffer_name(buffer), buffer.getDirectory, buffer.getName) |
|
27 |
|
28 def node_name(buffer: Buffer): Document.Node.Name = |
25 def node_name(buffer: Buffer): Document.Node.Name = |
29 { |
26 { |
30 val name = JEdit_Lib.buffer_name(buffer) |
27 val node = JEdit_Lib.buffer_name(buffer) |
31 Document.Node.Name(name, buffer.getDirectory, Thy_Header.thy_name(name).getOrElse("")) |
28 val theory = Thy_Header.thy_name(node).getOrElse("") |
|
29 val master_dir = if (theory == "") "" else buffer.getDirectory |
|
30 Document.Node.Name(node, master_dir, theory) |
32 } |
31 } |
33 |
32 |
34 def theory_node_name(buffer: Buffer): Option[Document.Node.Name] = |
33 def theory_node_name(buffer: Buffer): Option[Document.Node.Name] = |
35 { |
34 { |
36 val name = node_name(buffer) |
35 val name = node_name(buffer) |