1/* Title: Tools/jEdit/src/isabelle_export.scala 2 Author: Makarius 3 4Access Isabelle theory exports via virtual file-system. 5*/ 6 7package isabelle.jedit 8 9 10import isabelle._ 11 12import java.awt.Component 13import java.io.InputStream 14 15import org.gjt.sp.jedit.View 16import org.gjt.sp.jedit.io.VFSFile 17import org.gjt.sp.jedit.browser.VFSBrowser 18 19 20object Isabelle_Export 21{ 22 /* virtual file-system */ 23 24 val vfs_prefix = "isabelle-export:" 25 26 class VFS extends Isabelle_VFS(vfs_prefix, 27 read = true, browse = true, low_latency = true, non_awt_session = true) 28 { 29 override def _listFiles(vfs_session: AnyRef, url: String, component: Component): Array[VFSFile] = 30 { 31 explode_url(url, component = component) match { 32 case None => null 33 case Some(elems) => 34 val snapshot = PIDE.session.await_stable_snapshot() 35 val version = snapshot.version 36 elems match { 37 case Nil => 38 (for { 39 (node_name, _) <- version.nodes.iterator 40 if !snapshot.state.node_exports(version, node_name).is_empty 41 } yield make_entry(node_name.theory, is_dir = true)).toArray 42 case theory :: prefix => 43 val depth = prefix.length + 1 44 val entries: List[(String, Option[Long])] = 45 (for { 46 (node_name, _) <- version.nodes.iterator if node_name.theory == theory 47 exports = snapshot.state.node_exports(version, node_name) 48 (_, entry) <- exports.iterator if entry.name_extends(prefix) 49 } yield { 50 val is_dir = entry.name_elems.length > depth 51 val path = Export.implode_name(theory :: entry.name_elems.take(depth)) 52 val file_size = if (is_dir) None else Some(entry.uncompressed().length.toLong) 53 (path, file_size) 54 }).toSet.toList 55 (for ((path, file_size) <- entries.iterator) yield { 56 file_size match { 57 case None => make_entry(path, is_dir = true) 58 case Some(size) => make_entry(path, size = size) 59 } 60 }).toArray 61 } 62 } 63 } 64 65 override def _createInputStream( 66 vfs_session: AnyRef, url: String, ignore_errors: Boolean, component: Component): InputStream = 67 { 68 explode_url(url, component = if (ignore_errors) null else component) match { 69 case None | Some(Nil) => Bytes.empty.stream() 70 case Some(theory :: name_elems) => 71 val snapshot = PIDE.session.await_stable_snapshot() 72 val version = snapshot.version 73 val bytes = 74 (for { 75 (node_name, _) <- version.nodes.iterator 76 if node_name.theory == theory 77 (_, entry) <- snapshot.state.node_exports(version, node_name).iterator 78 if entry.name_elems == name_elems 79 } yield entry.uncompressed()).find(_ => true).getOrElse(Bytes.empty) 80 81 bytes.stream() 82 } 83 } 84 } 85 86 87 /* open browser */ 88 89 def open_browser(view: View) 90 { 91 val path = 92 PIDE.maybe_snapshot(view) match { 93 case None => "" 94 case Some(snapshot) => snapshot.node_name.theory 95 } 96 VFSBrowser.browseDirectory(view, vfs_prefix + path) 97 } 98} 99