src/Tools/jEdit/src/jedit_resources.scala
changeset 56208 06cc31dff138
parent 55134 1b67b17cdad5
child 56316 b1cf8ddc2e04
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Tue Mar 18 17:39:03 2014 +0100
     1.3 @@ -0,0 +1,123 @@
     1.4 +/*  Title:      Tools/jEdit/src/jedit_resources.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Resources for theories and auxiliary files, based on jEdit buffer
     1.8 +content and virtual file-systems.
     1.9 +*/
    1.10 +
    1.11 +package isabelle.jedit
    1.12 +
    1.13 +
    1.14 +import isabelle._
    1.15 +
    1.16 +import java.io.{File => JFile, IOException, ByteArrayOutputStream}
    1.17 +import javax.swing.text.Segment
    1.18 +
    1.19 +import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager}
    1.20 +import org.gjt.sp.jedit.MiscUtilities
    1.21 +import org.gjt.sp.jedit.{jEdit, View, Buffer}
    1.22 +import org.gjt.sp.jedit.bufferio.BufferIORequest
    1.23 +
    1.24 +
    1.25 +class JEdit_Resources(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax)
    1.26 +  extends Resources(loaded_theories, base_syntax)
    1.27 +{
    1.28 +  /* document node names */
    1.29 +
    1.30 +  def node_name(buffer: Buffer): Document.Node.Name =
    1.31 +  {
    1.32 +    val node = JEdit_Lib.buffer_name(buffer)
    1.33 +    val theory = Thy_Header.thy_name(node).getOrElse("")
    1.34 +    val master_dir = if (theory == "") "" else buffer.getDirectory
    1.35 +    Document.Node.Name(node, master_dir, theory)
    1.36 +  }
    1.37 +
    1.38 +  def theory_node_name(buffer: Buffer): Option[Document.Node.Name] =
    1.39 +  {
    1.40 +    val name = node_name(buffer)
    1.41 +    if (name.is_theory) Some(name) else None
    1.42 +  }
    1.43 +
    1.44 +
    1.45 +  /* file-system operations */
    1.46 +
    1.47 +  override def append(dir: String, source_path: Path): String =
    1.48 +  {
    1.49 +    val path = source_path.expand
    1.50 +    if (dir == "" || path.is_absolute) Isabelle_System.platform_path(path)
    1.51 +    else {
    1.52 +      val vfs = VFSManager.getVFSForPath(dir)
    1.53 +      if (vfs.isInstanceOf[FileVFS])
    1.54 +        MiscUtilities.resolveSymlinks(
    1.55 +          vfs.constructPath(dir, Isabelle_System.platform_path(path)))
    1.56 +      else vfs.constructPath(dir, Isabelle_System.standard_path(path))
    1.57 +    }
    1.58 +  }
    1.59 +
    1.60 +  override def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
    1.61 +  {
    1.62 +    Swing_Thread.now {
    1.63 +      JEdit_Lib.jedit_buffer(name.node) match {
    1.64 +        case Some(buffer) =>
    1.65 +          JEdit_Lib.buffer_lock(buffer) {
    1.66 +            Some(f(buffer.getSegment(0, buffer.getLength)))
    1.67 +          }
    1.68 +        case None => None
    1.69 +      }
    1.70 +    } getOrElse {
    1.71 +      val file = new JFile(name.node)  // FIXME load URL via jEdit VFS (!?)
    1.72 +      if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
    1.73 +      f(File.read(file))
    1.74 +    }
    1.75 +  }
    1.76 +
    1.77 +  def check_file(view: View, path: String): Boolean =
    1.78 +  {
    1.79 +    val vfs = VFSManager.getVFSForPath(path)
    1.80 +    val session = vfs.createVFSSession(path, view)
    1.81 +
    1.82 +    try {
    1.83 +      session != null && {
    1.84 +        try {
    1.85 +          val file = vfs._getFile(session, path, view)
    1.86 +          file != null && file.isReadable && file.getType == VFSFile.FILE
    1.87 +        }
    1.88 +        catch { case _: IOException => false }
    1.89 +      }
    1.90 +    }
    1.91 +    finally {
    1.92 +      try { vfs._endVFSSession(session, view) }
    1.93 +      catch { case _: IOException => }
    1.94 +    }
    1.95 +  }
    1.96 +
    1.97 +
    1.98 +  /* file content */
    1.99 +
   1.100 +  def file_content(buffer: Buffer): Bytes =
   1.101 +  {
   1.102 +    val path = buffer.getPath
   1.103 +    val vfs = VFSManager.getVFSForPath(path)
   1.104 +    val content =
   1.105 +      new BufferIORequest(null, buffer, null, vfs, path) {
   1.106 +        def _run() { }
   1.107 +        def apply(): Bytes =
   1.108 +        {
   1.109 +          val out =
   1.110 +            new ByteArrayOutputStream(buffer.getLength + 1) {
   1.111 +              def content(): Bytes = Bytes(this.buf, 0, this.count)
   1.112 +            }
   1.113 +          write(buffer, out)
   1.114 +          out.content()
   1.115 +        }
   1.116 +      }
   1.117 +    content()
   1.118 +  }
   1.119 +
   1.120 +
   1.121 +  /* theory text edits */
   1.122 +
   1.123 +  override def syntax_changed(): Unit =
   1.124 +    Swing_Thread.later { jEdit.propertiesChanged() }
   1.125 +}
   1.126 +