# HG changeset patch
# User wenzelm
# Date 1548863069 -3600
# Node ID 58fb0d7795834cccb329f389640047b1492d1367
# Parent a899ca03d74ca60cfe14f80ec6d7527ce29da76e
support for session information via virtual file-system;
diff -r a899ca03d74c -r 58fb0d779583 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala Wed Jan 30 16:32:06 2019 +0100
+++ b/src/Pure/Thy/sessions.scala Wed Jan 30 16:44:29 2019 +0100
@@ -11,7 +11,7 @@
import java.nio.channels.FileChannel
import java.nio.file.StandardOpenOption
-import scala.collection.SortedSet
+import scala.collection.{SortedSet, SortedMap}
import scala.collection.mutable
@@ -22,6 +22,7 @@
val root_name: String = "ROOT"
val theory_name: String = "Pure.Sessions"
+ val UNSORTED = "Unsorted"
val DRAFT = "Draft"
def is_pure(name: String): Boolean = name == Thy_Header.PURE
@@ -655,6 +656,11 @@
{
sessions_structure =>
+ lazy val chapters: SortedMap[String, List[Info]] =
+ (SortedMap.empty[String, List[Info]] /: build_graph.iterator)(
+ { case (chs, (_, (info, _))) =>
+ chs + (info.chapter -> (info :: chs.getOrElse(info.chapter, Nil))) })
+
def build_graph_display: Graph_Display.Graph = Graph_Display.make_graph(build_graph)
def imports_graph_display: Graph_Display.Graph = Graph_Display.make_graph(imports_graph)
@@ -912,7 +918,7 @@
def read_root(options: Options, select: Boolean, path: Path): List[Info] =
{
- var entry_chapter = "Unsorted"
+ var entry_chapter = UNSORTED
val infos = new mutable.ListBuffer[Info]
parse_root(path).foreach {
case Chapter(name) => entry_chapter = name
diff -r a899ca03d74c -r 58fb0d779583 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit Wed Jan 30 16:32:06 2019 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Wed Jan 30 16:44:29 2019 +0100
@@ -36,9 +36,10 @@
"src/isabelle.scala"
"src/isabelle_encoding.scala"
"src/isabelle_export.scala"
+ "src/isabelle_options.scala"
+ "src/isabelle_session.scala"
+ "src/isabelle_sidekick.scala"
"src/isabelle_vfs.scala"
- "src/isabelle_options.scala"
- "src/isabelle_sidekick.scala"
"src/jedit_bibtex.scala"
"src/jedit_editor.scala"
"src/jedit_lib.scala"
diff -r a899ca03d74c -r 58fb0d779583 src/Tools/jEdit/src/Isabelle.props
--- a/src/Tools/jEdit/src/Isabelle.props Wed Jan 30 16:32:06 2019 +0100
+++ b/src/Tools/jEdit/src/Isabelle.props Wed Jan 30 16:44:29 2019 +0100
@@ -31,6 +31,7 @@
plugin.isabelle.jedit.Plugin.menu.label=Isabelle
plugin.isabelle.jedit.Plugin.menu= \
isabelle-export-browser \
+ isabelle-session-browser \
isabelle.preview \
isabelle.draft \
- \
diff -r a899ca03d74c -r 58fb0d779583 src/Tools/jEdit/src/actions.xml
--- a/src/Tools/jEdit/src/actions.xml Wed Jan 30 16:32:06 2019 +0100
+++ b/src/Tools/jEdit/src/actions.xml Wed Jan 30 16:44:29 2019 +0100
@@ -172,6 +172,11 @@
isabelle.jedit.Isabelle_Export.open_browser(view);
+
+
+ isabelle.jedit.Isabelle_Session.open_browser(view);
+
+
isabelle.jedit.Keymap_Merge.check_dialog(view);
diff -r a899ca03d74c -r 58fb0d779583 src/Tools/jEdit/src/isabelle_session.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/isabelle_session.scala Wed Jan 30 16:44:29 2019 +0100
@@ -0,0 +1,72 @@
+/* Title: Tools/jEdit/src/isabelle_session.scala
+ Author: Makarius
+
+Access Isabelle session information via virtual file-system.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.Component
+import java.io.InputStream
+
+import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.io.VFSFile
+import org.gjt.sp.jedit.browser.VFSBrowser
+
+
+object Isabelle_Session
+{
+ /* sessions structure */
+
+ def sessions_structure(): Sessions.Structure =
+ JEdit_Sessions.sessions_structure(PIDE.options.value)
+
+
+ /* virtual file-system */
+
+ val vfs_prefix = "isabelle-session:"
+
+ class VFS extends Isabelle_VFS(vfs_prefix,
+ read = true, browse = true, low_latency = true, non_awt_session = true)
+ {
+ override def _listFiles(vfs_session: AnyRef, url: String, component: Component): Array[VFSFile] =
+ {
+ explode_url(url, component = component) match {
+ case None => null
+ case Some(elems) =>
+ val sessions = sessions_structure()
+ elems match {
+ case Nil =>
+ sessions.chapters.iterator.map(p => make_entry(p._1, is_dir = true)).toArray
+ case List(chapter) =>
+ sessions.chapters.get(chapter) match {
+ case None => null
+ case Some(infos) =>
+ infos.map(info => make_entry(chapter + "/" + info.name, is_dir = true)).toArray
+ }
+ case _ => null
+ }
+ }
+ }
+ }
+
+
+ /* open browser */
+
+ def open_browser(view: View)
+ {
+ val path =
+ PIDE.maybe_snapshot(view) match {
+ case None => ""
+ case Some(snapshot) =>
+ val sessions = sessions_structure()
+ val session = PIDE.resources.session_base.theory_qualifier(snapshot.node_name)
+ val chapter = sessions.get(session).getOrElse(Sessions.UNSORTED)
+ chapter + "/" + session
+ }
+ VFSBrowser.browseDirectory(view, vfs_prefix + path)
+ }
+}
diff -r a899ca03d74c -r 58fb0d779583 src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props Wed Jan 30 16:32:06 2019 +0100
+++ b/src/Tools/jEdit/src/jEdit.props Wed Jan 30 16:44:29 2019 +0100
@@ -231,6 +231,7 @@
isabelle.options.label=Isabelle options
isabelle.preview.label=Show preview in browser
isabelle-export-browser.label=Browse theory exports
+isabelle-session-browser.label=Browse session information
isabelle.reset-continuous-checking.label=Reset continuous checking
isabelle.reset-font-size.label=Reset font size
isabelle.reset-node-required.label=Reset node required
@@ -300,6 +301,8 @@
vfs.favorite.3=$JEDIT_SETTINGS
vfs.favorite.4.type=1
vfs.favorite.4=isabelle-export:
+vfs.favorite.5.type=1
+vfs.favorite.5=isabelle-session:
view.antiAlias=standard
view.blockCaret=true
view.caretBlink=false
diff -r a899ca03d74c -r 58fb0d779583 src/Tools/jEdit/src/services.xml
--- a/src/Tools/jEdit/src/services.xml Wed Jan 30 16:32:06 2019 +0100
+++ b/src/Tools/jEdit/src/services.xml Wed Jan 30 16:44:29 2019 +0100
@@ -11,6 +11,9 @@
new isabelle.jedit.Isabelle_Export.VFS();
+
+ new isabelle.jedit.Isabelle_Session.VFS();
+
new isabelle.jedit.Isabelle_Sidekick_Default();