--- a/src/Pure/PIDE/command.scala Fri Jan 11 19:05:26 2019 +0100
+++ b/src/Pure/PIDE/command.scala Fri Jan 11 22:59:00 2019 +0100
@@ -79,6 +79,7 @@
final class Exports private(private val rep: SortedMap[Long, Export.Entry])
{
+ def is_empty: Boolean = rep.isEmpty
def iterator: Iterator[Exports.Entry] = rep.iterator
def + (entry: Exports.Entry): Exports =
--- a/src/Pure/PIDE/document.scala Fri Jan 11 19:05:26 2019 +0100
+++ b/src/Pure/PIDE/document.scala Fri Jan 11 22:59:00 2019 +0100
@@ -761,6 +761,13 @@
}
}
+ def node_exports(version: Version, node_name: Node.Name): Command.Exports =
+ Command.Exports.merge(
+ for {
+ command <- version.nodes(node_name).commands.iterator
+ st <- command_states(version, command).iterator
+ } yield st.exports)
+
def assign(id: Document_ID.Version, update: Assign_Update): (List[Command], State) =
{
val version = the_version(id)
@@ -1071,11 +1078,7 @@
} yield (tree, pos)).toList
lazy val exports: List[Export.Entry] =
- Command.Exports.merge(
- for {
- command <- node.commands.iterator
- st <- state.command_states(version, command).iterator
- } yield st.exports).iterator.map(_._2).toList
+ state.node_exports(version, node_name).iterator.map(_._2).toList
lazy val exports_map: Map[String, Export.Entry] =
(for (entry <- exports.iterator) yield (entry.name, entry)).toMap
--- a/src/Pure/Thy/export.scala Fri Jan 11 19:05:26 2019 +0100
+++ b/src/Pure/Thy/export.scala Fri Jan 11 22:59:00 2019 +0100
@@ -13,6 +13,15 @@
object Export
{
+ /* structured name */
+
+ val sep_char: Char = '/'
+ val sep: String = sep_char.toString
+
+ def explode_name(s: String): List[String] = space_explode(sep_char, s)
+ def implode_name(elems: Iterable[String]): String = elems.mkString(sep)
+
+
/* SQL data model */
object Data
@@ -73,7 +82,12 @@
name: String,
body: Future[(Boolean, Bytes)])
{
- override def toString: String = uncompressed().toString
+ override def toString: String = name
+
+ val name_elems: List[String] = explode_name(name)
+
+ def name_extends(elems: List[String]): Boolean =
+ name_elems.startsWith(elems) && name_elems != elems
def text: String = uncompressed().text
--- a/src/Tools/jEdit/lib/Tools/jedit Fri Jan 11 19:05:26 2019 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Fri Jan 11 22:59:00 2019 +0100
@@ -35,6 +35,7 @@
"src/info_dockable.scala"
"src/isabelle.scala"
"src/isabelle_encoding.scala"
+ "src/isabelle_export.scala"
"src/isabelle_options.scala"
"src/isabelle_sidekick.scala"
"src/jedit_bibtex.scala"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/isabelle_export.scala Fri Jan 11 22:59:00 2019 +0100
@@ -0,0 +1,117 @@
+/* Title: Tools/jEdit/src/isabelle_export.scala
+ Author: Makarius
+
+Access Isabelle theory exports via virtual file-system.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.Component
+import java.io.InputStream
+
+import org.gjt.sp.jedit.io.{VFS => JEditVFS, VFSFile, VFSManager}
+
+
+object Isabelle_Export
+{
+ val vfs_name = "isabelle-export"
+ val vfs_caps =
+ JEditVFS.READ_CAP |
+ JEditVFS.BROWSE_CAP |
+ JEditVFS.LOW_LATENCY_CAP |
+ JEditVFS.NON_AWT_SESSION_CAP
+
+ val vfs_prefix = vfs_name + ":"
+
+ def vfs_error(component: Component, path: String, prop: String, args: AnyRef*): Unit =
+ VFSManager.error(component, path, prop, args.toArray)
+
+ def vfs_file(path: String, is_dir: Boolean = false, size: Long = 0L): VFSFile =
+ {
+ val name = Export.explode_name(path).lastOption getOrElse ""
+ val url = vfs_prefix + path
+ new VFSFile(name, url, url, if (is_dir) VFSFile.DIRECTORY else VFSFile.FILE, size, false)
+ }
+
+ def explode_url(url: String, component: Component = null): Option[List[String]] =
+ {
+ def bad: None.type =
+ {
+ if (component != null) vfs_error(component, url, "ioerror.badurl", url)
+ None
+ }
+ Library.try_unprefix(vfs_prefix, url) match {
+ case Some(path) =>
+ val elems = Export.explode_name(path)
+ if (elems.exists(_.isEmpty)) bad else Some(elems)
+ case None => bad
+ }
+ }
+
+ class VFS extends JEditVFS(vfs_name, vfs_caps)
+ {
+ override def constructPath(parent: String, path: String): String =
+ {
+ if (parent == vfs_prefix || parent.endsWith(Export.sep)) parent + path
+ else parent + Export.sep + path
+ }
+
+ override def _listFiles(session: AnyRef, url: String, component: Component): Array[VFSFile] =
+ {
+ explode_url(url, component = component) match {
+ case None => null
+ case Some(elems) =>
+ val snapshot = PIDE.snapshot()
+ val version = snapshot.version
+ elems match {
+ case Nil =>
+ (for {
+ (node_name, _) <- version.nodes.iterator
+ if !snapshot.state.node_exports(version, node_name).is_empty
+ } yield vfs_file(node_name.theory, is_dir = true)).toArray
+ case theory :: prefix =>
+ val depth = prefix.length + 1
+ val entries: List[(String, Option[Long])] =
+ (for {
+ (node_name, _) <- version.nodes.iterator if node_name.theory == theory
+ exports = snapshot.state.node_exports(version, node_name)
+ (_, entry) <- exports.iterator if entry.name_extends(prefix)
+ } yield {
+ val is_dir = entry.name_elems.length > depth
+ val path = Export.implode_name(theory :: entry.name_elems.take(depth))
+ val file_size = if (is_dir) None else Some(entry.uncompressed().length.toLong)
+ (path, file_size)
+ }).toSet.toList
+ (for ((path, file_size) <- entries.iterator) yield {
+ file_size match {
+ case None => vfs_file(path, is_dir = true)
+ case Some(size) => vfs_file(path, size = size)
+ }
+ }).toArray
+ }
+ }
+ }
+
+ override def _createInputStream(
+ session: AnyRef, url: String, ignore_errors: Boolean, component: Component): InputStream =
+ {
+ explode_url(url, component = if (ignore_errors) null else component) match {
+ case None | Some(Nil) => Bytes.empty.stream()
+ case Some(theory :: name_elems) =>
+ val snapshot = PIDE.snapshot()
+ val version = snapshot.version
+ val bytes =
+ (for {
+ (node_name, _) <- version.nodes.iterator
+ if node_name.theory == theory
+ (_, entry) <- snapshot.state.node_exports(version, node_name).iterator
+ if entry.name_elems == name_elems
+ } yield entry.uncompressed()).find(_ => true).getOrElse(Bytes.empty)
+ bytes.stream()
+ }
+ }
+ }
+}
--- a/src/Tools/jEdit/src/jedit_lib.scala Fri Jan 11 19:05:26 2019 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Fri Jan 11 22:59:00 2019 +0100
@@ -148,6 +148,9 @@
def jedit_views(): Iterator[View] = jEdit.getViews().iterator
+ def jedit_view(view: View = null): View =
+ if (view == null) jEdit.getActiveView() else view
+
def jedit_edit_panes(view: View): Iterator[EditPane] =
if (view == null) Iterator.empty
else view.getEditPanes().iterator.filter(_ != null)
--- a/src/Tools/jEdit/src/plugin.scala Fri Jan 11 19:05:26 2019 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Fri Jan 11 22:59:00 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")
--- a/src/Tools/jEdit/src/services.xml Fri Jan 11 19:05:26 2019 +0100
+++ b/src/Tools/jEdit/src/services.xml Fri Jan 11 22:59:00 2019 +0100
@@ -8,6 +8,9 @@
<SERVICE CLASS="org.gjt.sp.jedit.gui.DynamicContextMenuService" NAME="Spell_Checker">
new isabelle.jedit.Context_Menu();
</SERVICE>
+ <SERVICE NAME="isabelle-export" CLASS="org.gjt.sp.jedit.io.VFS">
+ new isabelle.jedit.Isabelle_Export.VFS();
+ </SERVICE>
<SERVICE NAME="isabelle" CLASS="sidekick.SideKickParser">
new isabelle.jedit.Isabelle_Sidekick_Default();
</SERVICE>