equal
deleted
inserted
replaced
40 def invoke_generated(): Unit = { delay1_flush.invoke(); delay2_flush.invoke() } |
40 def invoke_generated(): Unit = { delay1_flush.invoke(); delay2_flush.invoke() } |
41 |
41 |
42 def visible_node(name: Document.Node.Name): Boolean = |
42 def visible_node(name: Document.Node.Name): Boolean = |
43 (for { |
43 (for { |
44 text_area <- JEdit_Lib.jedit_text_areas() |
44 text_area <- JEdit_Lib.jedit_text_areas() |
45 doc_view <- Document_View(text_area) |
45 doc_view <- Document_View.get(text_area) |
46 } yield doc_view.model.node_name).contains(name) |
46 } yield doc_view.model.node_name).contains(name) |
47 |
47 |
48 |
48 |
49 /* current situation */ |
49 /* current situation */ |
50 |
50 |
71 GUI_Thread.require {} |
71 GUI_Thread.require {} |
72 |
72 |
73 val text_area = view.getTextArea |
73 val text_area = view.getTextArea |
74 val buffer = view.getBuffer |
74 val buffer = view.getBuffer |
75 |
75 |
76 PIDE.document_view(text_area) match { |
76 Document_View.get(text_area) match { |
77 case Some(doc_view) if doc_view.model.is_theory => |
77 case Some(doc_view) if doc_view.model.is_theory => |
78 val node = snapshot.version.nodes(doc_view.model.node_name) |
78 val node = snapshot.version.nodes(doc_view.model.node_name) |
79 val caret = snapshot.revert(text_area.getCaretPosition) |
79 val caret = snapshot.revert(text_area.getCaretPosition) |
80 if (caret < buffer.getLength) { |
80 if (caret < buffer.getLength) { |
81 val caret_command_iterator = node.command_iterator(caret) |
81 val caret_command_iterator = node.command_iterator(caret) |