# HG changeset patch
# User wenzelm
# Date 1548860826 -3600
# Node ID 092c6a4bcc2613b7ae34dba789e0e456d08f5172
# Parent  34a93af5b96938de684dec1d5c582d0b18a5930d
tuned signature;

diff -r 34a93af5b969 -r 092c6a4bcc26 src/Tools/jEdit/src/isabelle_export.scala
--- a/src/Tools/jEdit/src/isabelle_export.scala	Wed Jan 30 15:25:19 2019 +0100
+++ b/src/Tools/jEdit/src/isabelle_export.scala	Wed Jan 30 16:07:06 2019 +0100
@@ -99,9 +99,11 @@
 
   def open_browser(view: View)
   {
-    val theory =
-      try { PIDE.snapshot(view).node_name.theory }
-      catch { case ERROR(_) => "" }
-    VFSBrowser.browseDirectory(view, vfs_prefix + theory)
+    val path =
+      PIDE.maybe_snapshot(view) match {
+        case None => ""
+        case Some(snapshot) => snapshot.node_name.theory
+      }
+    VFSBrowser.browseDirectory(view, vfs_prefix + path)
   }
 }
diff -r 34a93af5b969 -r 092c6a4bcc26 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Jan 30 15:25:19 2019 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Jan 30 16:07:06 2019 +0100
@@ -26,24 +26,24 @@
 {
   /* semantic document content */
 
-  def snapshot(view: View = null): Document.Snapshot = GUI_Thread.now
+  def maybe_snapshot(view: View = null): Option[Document.Snapshot] = GUI_Thread.now
   {
     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")
-    }
+    Document_Model.get(buffer).map(_.snapshot)
   }
 
-  def rendering(view: View = null): JEdit_Rendering = GUI_Thread.now
+  def maybe_rendering(view: View = null): Option[JEdit_Rendering] = GUI_Thread.now
   {
     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")
-    }
+    Document_View.get(text_area).map(_.get_rendering())
   }
 
+  def snapshot(view: View = null): Document.Snapshot =
+    maybe_snapshot(view) getOrElse error("No document model for current buffer")
+
+  def rendering(view: View = null): JEdit_Rendering =
+    maybe_rendering(view) getOrElse error("No document view for current text area")
+
 
   /* plugin instance */