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