src/Tools/jEdit/src/jedit_resources.scala
author wenzelm
Tue Mar 18 17:39:03 2014 +0100 (2014-03-18)
changeset 56208 06cc31dff138
parent 55134 src/Tools/jEdit/src/jedit_thy_load.scala@1b67b17cdad5
child 56316 b1cf8ddc2e04
permissions -rw-r--r--
clarifed module name;
     1 /*  Title:      Tools/jEdit/src/jedit_resources.scala
     2     Author:     Makarius
     3 
     4 Resources for theories and auxiliary files, based on jEdit buffer
     5 content and virtual file-systems.
     6 */
     7 
     8 package isabelle.jedit
     9 
    10 
    11 import isabelle._
    12 
    13 import java.io.{File => JFile, IOException, ByteArrayOutputStream}
    14 import javax.swing.text.Segment
    15 
    16 import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager}
    17 import org.gjt.sp.jedit.MiscUtilities
    18 import org.gjt.sp.jedit.{jEdit, View, Buffer}
    19 import org.gjt.sp.jedit.bufferio.BufferIORequest
    20 
    21 
    22 class JEdit_Resources(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax)
    23   extends Resources(loaded_theories, base_syntax)
    24 {
    25   /* document node names */
    26 
    27   def node_name(buffer: Buffer): Document.Node.Name =
    28   {
    29     val node = JEdit_Lib.buffer_name(buffer)
    30     val theory = Thy_Header.thy_name(node).getOrElse("")
    31     val master_dir = if (theory == "") "" else buffer.getDirectory
    32     Document.Node.Name(node, master_dir, theory)
    33   }
    34 
    35   def theory_node_name(buffer: Buffer): Option[Document.Node.Name] =
    36   {
    37     val name = node_name(buffer)
    38     if (name.is_theory) Some(name) else None
    39   }
    40 
    41 
    42   /* file-system operations */
    43 
    44   override def append(dir: String, source_path: Path): String =
    45   {
    46     val path = source_path.expand
    47     if (dir == "" || path.is_absolute) Isabelle_System.platform_path(path)
    48     else {
    49       val vfs = VFSManager.getVFSForPath(dir)
    50       if (vfs.isInstanceOf[FileVFS])
    51         MiscUtilities.resolveSymlinks(
    52           vfs.constructPath(dir, Isabelle_System.platform_path(path)))
    53       else vfs.constructPath(dir, Isabelle_System.standard_path(path))
    54     }
    55   }
    56 
    57   override def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
    58   {
    59     Swing_Thread.now {
    60       JEdit_Lib.jedit_buffer(name.node) match {
    61         case Some(buffer) =>
    62           JEdit_Lib.buffer_lock(buffer) {
    63             Some(f(buffer.getSegment(0, buffer.getLength)))
    64           }
    65         case None => None
    66       }
    67     } getOrElse {
    68       val file = new JFile(name.node)  // FIXME load URL via jEdit VFS (!?)
    69       if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
    70       f(File.read(file))
    71     }
    72   }
    73 
    74   def check_file(view: View, path: String): Boolean =
    75   {
    76     val vfs = VFSManager.getVFSForPath(path)
    77     val session = vfs.createVFSSession(path, view)
    78 
    79     try {
    80       session != null && {
    81         try {
    82           val file = vfs._getFile(session, path, view)
    83           file != null && file.isReadable && file.getType == VFSFile.FILE
    84         }
    85         catch { case _: IOException => false }
    86       }
    87     }
    88     finally {
    89       try { vfs._endVFSSession(session, view) }
    90       catch { case _: IOException => }
    91     }
    92   }
    93 
    94 
    95   /* file content */
    96 
    97   def file_content(buffer: Buffer): Bytes =
    98   {
    99     val path = buffer.getPath
   100     val vfs = VFSManager.getVFSForPath(path)
   101     val content =
   102       new BufferIORequest(null, buffer, null, vfs, path) {
   103         def _run() { }
   104         def apply(): Bytes =
   105         {
   106           val out =
   107             new ByteArrayOutputStream(buffer.getLength + 1) {
   108               def content(): Bytes = Bytes(this.buf, 0, this.count)
   109             }
   110           write(buffer, out)
   111           out.content()
   112         }
   113       }
   114     content()
   115   }
   116 
   117 
   118   /* theory text edits */
   119 
   120   override def syntax_changed(): Unit =
   121     Swing_Thread.later { jEdit.propertiesChanged() }
   122 }
   123