--- a/src/Tools/jEdit/src/jedit_lib.scala Fri Jan 11 22:35:04 2019 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Fri Jan 11 22:35:41 2019 +0100
@@ -148,6 +148,9 @@
def jedit_views(): Iterator[View] = jEdit.getViews().iterator
+ def jedit_view(view: View = null): View =
+ if (view == null) jEdit.getActiveView() else view
+
def jedit_edit_panes(view: View): Iterator[EditPane] =
if (view == null) Iterator.empty
else view.getEditPanes().iterator.filter(_ != null)
--- a/src/Tools/jEdit/src/plugin.scala Fri Jan 11 22:35:04 2019 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Fri Jan 11 22:35:41 2019 +0100
@@ -26,17 +26,18 @@
{
/* semantic document content */
- def snapshot(view: View): Document.Snapshot = GUI_Thread.now
+ def snapshot(view: View = null): Document.Snapshot = GUI_Thread.now
{
- Document_Model.get(view.getBuffer) match {
+ val buffer = JEdit_Lib.jedit_view(view).getBuffer
+ Document_Model.get(buffer) match {
case Some(model) => model.snapshot
case None => error("No document model for current buffer")
}
}
- def rendering(view: View): JEdit_Rendering = GUI_Thread.now
+ def rendering(view: View = null): JEdit_Rendering = GUI_Thread.now
{
- val text_area = view.getTextArea
+ val text_area = JEdit_Lib.jedit_view(view).getTextArea
Document_View.get(text_area) match {
case Some(doc_view) => doc_view.get_rendering()
case None => error("No document view for current text area")