equal
deleted
inserted
replaced
74 |
74 |
75 def buffer_text(buffer: JEditBuffer): String = |
75 def buffer_text(buffer: JEditBuffer): String = |
76 buffer_lock(buffer) { buffer.getText(0, buffer.getLength) } |
76 buffer_lock(buffer) { buffer.getText(0, buffer.getLength) } |
77 |
77 |
78 def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath |
78 def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath |
79 |
|
80 def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] = |
|
81 Some(Document.Node.Name(buffer_name(buffer), buffer.getDirectory, buffer.getName)) |
|
82 |
|
83 def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] = |
|
84 { |
|
85 val name = buffer_name(buffer) |
|
86 Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory)) |
|
87 } |
|
88 |
79 |
89 |
80 |
90 /* main jEdit components */ |
81 /* main jEdit components */ |
91 |
82 |
92 def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator |
83 def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator |