added action "isabelle-export-browser";
authorwenzelm
Sun, 13 Jan 2019 13:33:23 +0100
changeset 69656 83f15deb2d36
parent 69655 3694b021e555
child 69657 f044766cd94f
added action "isabelle-export-browser";
NEWS
src/Tools/jEdit/src/Isabelle.props
src/Tools/jEdit/src/actions.xml
src/Tools/jEdit/src/isabelle_export.scala
src/Tools/jEdit/src/jEdit.props
--- 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
--- 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 \
   - \
--- 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);
--- 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)
+  }
 }
--- 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