1/*  Title:      Tools/jEdit/src/isabelle_session.scala
2    Author:     Makarius
3
4Access Isabelle session information 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.{VFS => JEdit_VFS, VFSFile}
17import org.gjt.sp.jedit.browser.VFSBrowser
18
19
20object Isabelle_Session
21{
22  /* sessions structure */
23
24  def sessions_structure(): Sessions.Structure =
25    JEdit_Sessions.sessions_structure(PIDE.options.value)
26
27
28  /* virtual file-system */
29
30  val vfs_prefix = "isabelle-session:"
31
32  class Session_Entry(name: String, path: String, marker: String)
33    extends VFSFile(name, path, vfs_prefix + name, VFSFile.FILE, 0L, false)
34  {
35    override def getPathMarker: String = marker
36
37    override def getExtendedAttribute(att: String): String =
38      if (att == JEdit_VFS.EA_SIZE) null
39      else super.getExtendedAttribute(att)
40  }
41
42  class VFS extends Isabelle_VFS(vfs_prefix,
43    read = true, browse = true, low_latency = true, non_awt_session = true)
44  {
45    override def _listFiles(vfs_session: AnyRef, url: String, component: Component): Array[VFSFile] =
46    {
47      explode_url(url, component = component) match {
48        case None => null
49        case Some(elems) =>
50          val sessions = sessions_structure()
51          elems match {
52            case Nil =>
53              sessions.chapters.iterator.map(p => make_entry(p._1, is_dir = true)).toArray
54            case List(chapter) =>
55              sessions.chapters.get(chapter) match {
56                case None => null
57                case Some(infos) =>
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                      }
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)
72                  }).toArray
73              }
74            case _ => null
75          }
76      }
77    }
78  }
79
80
81  /* open browser */
82
83  def open_browser(view: View)
84  {
85    val path =
86      PIDE.maybe_snapshot(view) match {
87        case None => ""
88        case Some(snapshot) =>
89          val sessions = sessions_structure()
90          val session = PIDE.resources.session_base.theory_qualifier(snapshot.node_name)
91          val chapter =
92            sessions.get(session) match {
93              case Some(info) => info.chapter
94              case None => Sessions.UNSORTED
95            }
96          chapter
97      }
98    VFSBrowser.browseDirectory(view, vfs_prefix + path)
99  }
100}
101