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