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")