# HG changeset patch # User wenzelm # Date 1547243940 -3600 # Node ID 938b28a998637f6582ff5cfa4506e1c89a8fde12 # Parent 7d02b7bee660bb38af33a7a52236424f8f6d6453# Parent f3b564a13236fb6254f2267fa248c6f75b2e89ab merged diff -r 7d02b7bee660 -r 938b28a99863 src/Pure/PIDE/command.scala --- 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 = diff -r 7d02b7bee660 -r 938b28a99863 src/Pure/PIDE/document.scala --- 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 diff -r 7d02b7bee660 -r 938b28a99863 src/Pure/Thy/export.scala --- 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 diff -r 7d02b7bee660 -r 938b28a99863 src/Tools/jEdit/lib/Tools/jedit --- 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" diff -r 7d02b7bee660 -r 938b28a99863 src/Tools/jEdit/src/isabelle_export.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() + } + } + } +} diff -r 7d02b7bee660 -r 938b28a99863 src/Tools/jEdit/src/jedit_lib.scala --- 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) diff -r 7d02b7bee660 -r 938b28a99863 src/Tools/jEdit/src/plugin.scala --- 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") diff -r 7d02b7bee660 -r 938b28a99863 src/Tools/jEdit/src/services.xml --- 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 @@ new isabelle.jedit.Context_Menu(); + + new isabelle.jedit.Isabelle_Export.VFS(); + new isabelle.jedit.Isabelle_Sidekick_Default();