15 import org.gjt.sp.jedit.View |
15 import org.gjt.sp.jedit.View |
16 import org.gjt.sp.jedit.io.{VFS => JEdit_VFS, VFSFile} |
16 import org.gjt.sp.jedit.io.{VFS => JEdit_VFS, VFSFile} |
17 import org.gjt.sp.jedit.browser.VFSBrowser |
17 import org.gjt.sp.jedit.browser.VFSBrowser |
18 |
18 |
19 |
19 |
20 object Isabelle_Session |
20 object Isabelle_Session { |
21 { |
|
22 /* sessions structure */ |
21 /* sessions structure */ |
23 |
22 |
24 def sessions_structure(): Sessions.Structure = |
23 def sessions_structure(): Sessions.Structure = |
25 JEdit_Sessions.sessions_structure(PIDE.options.value) |
24 JEdit_Sessions.sessions_structure(PIDE.options.value) |
26 |
25 |
28 /* virtual file-system */ |
27 /* virtual file-system */ |
29 |
28 |
30 val vfs_prefix = "isabelle-session:" |
29 val vfs_prefix = "isabelle-session:" |
31 |
30 |
32 class Session_Entry(name: String, path: String, marker: String) |
31 class Session_Entry(name: String, path: String, marker: String) |
33 extends VFSFile(name, path, vfs_prefix + name, VFSFile.FILE, 0L, false) |
32 extends VFSFile(name, path, vfs_prefix + name, VFSFile.FILE, 0L, false) { |
34 { |
|
35 override def getPathMarker: String = marker |
33 override def getPathMarker: String = marker |
36 |
34 |
37 override def getExtendedAttribute(att: String): String = |
35 override def getExtendedAttribute(att: String): String = |
38 if (att == JEdit_VFS.EA_SIZE) null |
36 if (att == JEdit_VFS.EA_SIZE) null |
39 else super.getExtendedAttribute(att) |
37 else super.getExtendedAttribute(att) |
40 } |
38 } |
41 |
39 |
42 class VFS extends Isabelle_VFS(vfs_prefix, |
40 class VFS |
43 read = true, browse = true, low_latency = true, non_awt_session = true) |
41 extends Isabelle_VFS( |
44 { |
42 vfs_prefix, |
45 override def _listFiles(vfs_session: AnyRef, url: String, component: Component): Array[VFSFile] = |
43 read = true, |
46 { |
44 browse = true, |
|
45 low_latency = true, |
|
46 non_awt_session = true |
|
47 ) { |
|
48 override def _listFiles( |
|
49 vfs_session: AnyRef, |
|
50 url: String, |
|
51 component: Component |
|
52 ): Array[VFSFile] = { |
47 explode_url(url, component = component) match { |
53 explode_url(url, component = component) match { |
48 case None => null |
54 case None => null |
49 case Some(elems) => |
55 case Some(elems) => |
50 val sessions = sessions_structure() |
56 val sessions = sessions_structure() |
51 elems match { |
57 elems match { |
53 sessions.chapters.iterator.map(p => make_entry(p._1, is_dir = true)).toArray |
59 sessions.chapters.iterator.map(p => make_entry(p._1, is_dir = true)).toArray |
54 case List(chapter) => |
60 case List(chapter) => |
55 sessions.chapters.get(chapter) match { |
61 sessions.chapters.get(chapter) match { |
56 case None => null |
62 case None => null |
57 case Some(infos) => |
63 case Some(infos) => |
58 infos.map(info => |
64 infos.map(info => { |
59 { |
|
60 val name = chapter + "/" + info.name |
65 val name = chapter + "/" + info.name |
61 val path = |
66 val path = |
62 Position.File.unapply(info.pos) match { |
67 Position.File.unapply(info.pos) match { |
63 case Some(path) => File.platform_path(path) |
68 case Some(path) => File.platform_path(path) |
64 case None => null |
69 case None => null |