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