equal
deleted
inserted
replaced
166 def buffer_text(buffer: JEditBuffer): String = |
166 def buffer_text(buffer: JEditBuffer): String = |
167 buffer_lock(buffer) { buffer.getText(0, buffer.getLength) } |
167 buffer_lock(buffer) { buffer.getText(0, buffer.getLength) } |
168 |
168 |
169 def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath |
169 def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath |
170 |
170 |
171 def buffer_path(buffer: Buffer): (String, String) = |
|
172 (buffer.getDirectory, buffer_name(buffer)) |
|
173 |
|
174 |
171 |
175 /* main jEdit components */ |
172 /* main jEdit components */ |
176 |
173 |
177 def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator |
174 def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator |
178 |
175 |
214 swing_buffer_lock(buffer) { |
211 swing_buffer_lock(buffer) { |
215 val opt_model = |
212 val opt_model = |
216 document_model(buffer) match { |
213 document_model(buffer) match { |
217 case Some(model) => Some(model) |
214 case Some(model) => Some(model) |
218 case None => |
215 case None => |
219 val (master_dir, path) = buffer_path(buffer) |
216 val name = buffer_name(buffer) |
220 Thy_Header.thy_name(path) match { |
217 Thy_Header.thy_name(name) match { |
221 case Some(name) => |
218 case Some(theory) => |
222 Some(Document_Model.init(session, buffer, master_dir, path, name)) |
219 val node_name = Document.Node.Name(name, buffer.getDirectory, theory) |
|
220 Some(Document_Model.init(session, buffer, node_name)) |
223 case None => None |
221 case None => None |
224 } |
222 } |
225 } |
223 } |
226 if (opt_model.isDefined) { |
224 if (opt_model.isDefined) { |
227 for (text_area <- jedit_text_areas(buffer)) { |
225 for (text_area <- jedit_text_areas(buffer)) { |
361 def loaded_buffer(name: String): Boolean = |
359 def loaded_buffer(name: String): Boolean = |
362 buffers.exists(buffer => Isabelle.buffer_name(buffer) == name) |
360 buffers.exists(buffer => Isabelle.buffer_name(buffer) == name) |
363 |
361 |
364 val thys = |
362 val thys = |
365 for (buffer <- buffers; model <- Isabelle.document_model(buffer)) |
363 for (buffer <- buffers; model <- Isabelle.document_model(buffer)) |
366 yield (model.master_dir, model.thy_name) |
364 yield model.name |
367 val files = thy_info.dependencies(thys).toList.map(_._1).filterNot(loaded_buffer _) |
365 val files = thy_info.dependencies(thys).toList.map(_._1.node).filterNot(loaded_buffer _) |
368 |
366 |
369 if (!files.isEmpty) { |
367 if (!files.isEmpty) { |
370 val files_list = new ListView(Library.sort_strings(files)) |
368 val files_list = new ListView(Library.sort_strings(files)) |
371 for (i <- 0 until files.length) |
369 for (i <- 0 until files.length) |
372 files_list.selection.indices += i |
370 files_list.selection.indices += i |