author | wenzelm |
Wed, 30 Jan 2019 22:46:49 +0100 | |
changeset 69766 | 76fbd806ebc5 |
parent 69765 | c5778547ed03 |
child 70253 | cb334a92a4db |
permissions | -rw-r--r-- |
69762
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Tools/jEdit/src/isabelle_session.scala |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
3 |
|
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
4 |
Access Isabelle session information via virtual file-system. |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
6 |
|
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle.jedit |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
8 |
|
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
9 |
|
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
10 |
import isabelle._ |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
11 |
|
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
12 |
import java.awt.Component |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
13 |
import java.io.InputStream |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
14 |
|
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
15 |
import org.gjt.sp.jedit.View |
69763 | 16 |
import org.gjt.sp.jedit.io.{VFS => JEdit_VFS, VFSFile} |
69762
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
17 |
import org.gjt.sp.jedit.browser.VFSBrowser |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
18 |
|
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
19 |
|
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
20 |
object Isabelle_Session |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
21 |
{ |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
22 |
/* sessions structure */ |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
23 |
|
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
24 |
def sessions_structure(): Sessions.Structure = |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
25 |
JEdit_Sessions.sessions_structure(PIDE.options.value) |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
26 |
|
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
27 |
|
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
28 |
/* virtual file-system */ |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
29 |
|
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
30 |
val vfs_prefix = "isabelle-session:" |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
31 |
|
69765 | 32 |
class Session_Entry(name: String, path: String, marker: String) |
69766
76fbd806ebc5
more robust: avoid crash of browser right-click menu;
wenzelm
parents:
69765
diff
changeset
|
33 |
extends VFSFile(name, path, vfs_prefix + name, VFSFile.FILE, 0L, false) |
69763 | 34 |
{ |
69765 | 35 |
override def getPathMarker: String = marker |
36 |
||
69763 | 37 |
override def getExtendedAttribute(att: String): String = |
38 |
if (att == JEdit_VFS.EA_SIZE) null |
|
39 |
else super.getExtendedAttribute(att) |
|
40 |
} |
|
41 |
||
69762
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
42 |
class VFS extends Isabelle_VFS(vfs_prefix, |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
43 |
read = true, browse = true, low_latency = true, non_awt_session = true) |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
44 |
{ |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
45 |
override def _listFiles(vfs_session: AnyRef, url: String, component: Component): Array[VFSFile] = |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
46 |
{ |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
47 |
explode_url(url, component = component) match { |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
48 |
case None => null |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
49 |
case Some(elems) => |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
50 |
val sessions = sessions_structure() |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
51 |
elems match { |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
52 |
case Nil => |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
53 |
sessions.chapters.iterator.map(p => make_entry(p._1, is_dir = true)).toArray |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
54 |
case List(chapter) => |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
55 |
sessions.chapters.get(chapter) match { |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
56 |
case None => null |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
57 |
case Some(infos) => |
69763 | 58 |
infos.map(info => |
59 |
{ |
|
60 |
val name = chapter + "/" + info.name |
|
61 |
val path = |
|
62 |
Position.File.unapply(info.pos) match { |
|
63 |
case Some(path) => File.platform_path(path) |
|
64 |
case None => null |
|
65 |
} |
|
69765 | 66 |
val marker = |
67 |
Position.Line.unapply(info.pos) match { |
|
68 |
case Some(line) => "+line:" + line |
|
69 |
case None => null |
|
70 |
} |
|
71 |
new Session_Entry(name, path, marker) |
|
69763 | 72 |
}).toArray |
69762
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
73 |
} |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
74 |
case _ => null |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
75 |
} |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
76 |
} |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
77 |
} |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
78 |
} |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
79 |
|
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
80 |
|
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
81 |
/* open browser */ |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
82 |
|
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
83 |
def open_browser(view: View) |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
84 |
{ |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
85 |
val path = |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
86 |
PIDE.maybe_snapshot(view) match { |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
87 |
case None => "" |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
88 |
case Some(snapshot) => |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
89 |
val sessions = sessions_structure() |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
90 |
val session = PIDE.resources.session_base.theory_qualifier(snapshot.node_name) |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
91 |
val chapter = sessions.get(session).getOrElse(Sessions.UNSORTED) |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
92 |
chapter + "/" + session |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
93 |
} |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
94 |
VFSBrowser.browseDirectory(view, vfs_prefix + path) |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
95 |
} |
58fb0d779583
support for session information via virtual file-system;
wenzelm
parents:
diff
changeset
|
96 |
} |