merged
authorwenzelm
Fri, 11 Jan 2019 22:59:00 +0100
changeset 69651 938b28a99863
parent 69645 7d02b7bee660 (current diff)
parent 69650 f3b564a13236 (diff)
child 69652 091f57432f05
merged
--- 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>