# HG changeset patch
# User wenzelm
# Date 1547382803 -3600
# Node ID 83f15deb2d36d09b508367a7a7d0f40cc77e2a58
# Parent  3694b021e55566b59e0f559839a4205d5c0bbbbf
added action "isabelle-export-browser";

diff -r 3694b021e555 -r 83f15deb2d36 NEWS
--- a/NEWS	Sat Jan 12 21:26:35 2019 +0100
+++ b/NEWS	Sun Jan 13 13:33:23 2019 +0100
@@ -43,6 +43,10 @@
 
 *** Isabelle/jEdit Prover IDE ***
 
+* Action "isabelle-export-browser" points the File Browser to the theory
+exports of the current buffer. The directory view needs to be reloaded
+manually to follow ongoing document processing.
+
 * Fonts for the text area, gutter, GUI elements etc. use the "Isabelle
 DejaVu" collection by default, which provides uniform rendering quality
 with the usual Isabelle symbols. Line spacing no longer needs to be
diff -r 3694b021e555 -r 83f15deb2d36 src/Tools/jEdit/src/Isabelle.props
--- a/src/Tools/jEdit/src/Isabelle.props	Sat Jan 12 21:26:35 2019 +0100
+++ b/src/Tools/jEdit/src/Isabelle.props	Sun Jan 13 13:33:23 2019 +0100
@@ -30,6 +30,7 @@
 #menu actions and dockables
 plugin.isabelle.jedit.Plugin.menu.label=Isabelle
 plugin.isabelle.jedit.Plugin.menu= \
+  isabelle-export-browser \
   isabelle.preview \
   isabelle.draft \
   - \
diff -r 3694b021e555 -r 83f15deb2d36 src/Tools/jEdit/src/actions.xml
--- a/src/Tools/jEdit/src/actions.xml	Sat Jan 12 21:26:35 2019 +0100
+++ b/src/Tools/jEdit/src/actions.xml	Sun Jan 13 13:33:23 2019 +0100
@@ -167,6 +167,11 @@
 	    isabelle.jedit.Document_Model.open_preview(view, true);
 	  </CODE>
 	</ACTION>
+	<ACTION NAME="isabelle-export-browser">
+	  <CODE>
+	    isabelle.jedit.Isabelle_Export.open_browser(view);
+	  </CODE>
+	</ACTION>
 	<ACTION NAME="isabelle.keymap-merge">
 	  <CODE>
 	    isabelle.jedit.Keymap_Merge.check_dialog(view);
diff -r 3694b021e555 -r 83f15deb2d36 src/Tools/jEdit/src/isabelle_export.scala
--- a/src/Tools/jEdit/src/isabelle_export.scala	Sat Jan 12 21:26:35 2019 +0100
+++ b/src/Tools/jEdit/src/isabelle_export.scala	Sun Jan 13 13:33:23 2019 +0100
@@ -15,10 +15,13 @@
 import org.gjt.sp.jedit.{Buffer, View}
 import org.gjt.sp.jedit.io.{VFS => JEditVFS, VFSFile, VFSManager}
 import org.gjt.sp.jedit.bufferio.BufferLoadRequest
+import org.gjt.sp.jedit.browser.VFSBrowser
 
 
 object Isabelle_Export
 {
+  /* virtual file-system */
+
   val vfs_name = "isabelle-export"
   val vfs_caps =
     JEditVFS.READ_CAP |
@@ -125,4 +128,15 @@
       }
     }
   }
+
+
+  /* open browser */
+
+  def open_browser(view: View)
+  {
+    val theory =
+      try { PIDE.snapshot(view).node_name.theory }
+      catch { case ERROR(_) => "" }
+    VFSBrowser.browseDirectory(view, vfs_prefix + theory)
+  }
 }
diff -r 3694b021e555 -r 83f15deb2d36 src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Sat Jan 12 21:26:35 2019 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Sun Jan 13 13:33:23 2019 +0100
@@ -230,6 +230,7 @@
 isabelle.newline.shortcut=ENTER
 isabelle.options.label=Isabelle options
 isabelle.preview.label=Show preview in browser
+isabelle-export-browser.label=Browse theory exports
 isabelle.reset-continuous-checking.label=Reset continuous checking
 isabelle.reset-font-size.label=Reset font size
 isabelle.reset-node-required.label=Reset node required