# HG changeset patch
# User wenzelm
# Date 1547242541 -3600
# Node ID dd1e0e1570d20719ff009a174dd24cc9919efc59
# Parent  95dc926fa39c7b981801d65815ea75b1fda097db
clarified signature;

diff -r 95dc926fa39c -r dd1e0e1570d2 src/Tools/jEdit/src/jedit_lib.scala
--- 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)
diff -r 95dc926fa39c -r dd1e0e1570d2 src/Tools/jEdit/src/plugin.scala
--- 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")