src/Tools/jEdit/src/jedit_resources.scala
author wenzelm
Wed Apr 09 23:22:58 2014 +0200 (2014-04-09)
changeset 56502 db2836f65d42
parent 56460 af28fdd50690
child 56666 229309cbc508
permissions -rw-r--r--
improved support for external URLs, based on standard Java network operations;
     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, ByteArrayOutputStream}
    14 import javax.swing.text.Segment
    15 
    16 import org.gjt.sp.jedit.io.{VFS, FileVFS, 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 if (path.is_current) dir
    49     else {
    50       val vfs = VFSManager.getVFSForPath(dir)
    51       if (vfs.isInstanceOf[FileVFS])
    52         MiscUtilities.resolveSymlinks(
    53           vfs.constructPath(dir, Isabelle_System.platform_path(path)))
    54       else vfs.constructPath(dir, Isabelle_System.standard_path(path))
    55     }
    56   }
    57 
    58   override def with_thy_text[A](name: Document.Node.Name, consume: CharSequence => A): A =
    59   {
    60     Swing_Thread.now {
    61       JEdit_Lib.jedit_buffer(name) match {
    62         case Some(buffer) =>
    63           JEdit_Lib.buffer_lock(buffer) {
    64             Some(consume(buffer.getSegment(0, buffer.getLength)))
    65           }
    66         case None => None
    67       }
    68     } getOrElse {
    69       if (Url.is_wellformed(name.node)) consume(Url.read(name.node))
    70       else {
    71         val file = new JFile(name.node)
    72         if (file.isFile) consume(File.read(file))
    73         else error("No such file: " + quote(file.toString))
    74       }
    75     }
    76   }
    77 
    78   def check_file(view: View, file: String): Boolean =
    79     try {
    80       if (Url.is_wellformed(file)) Url.is_readable(file)
    81       else (new JFile(file)).isFile
    82     }
    83     catch { case ERROR(_) => false }
    84 
    85 
    86   /* file content */
    87 
    88   def file_content(buffer: Buffer): Bytes =
    89   {
    90     val path = buffer.getPath
    91     val vfs = VFSManager.getVFSForPath(path)
    92     val content =
    93       new BufferIORequest(null, buffer, null, vfs, path) {
    94         def _run() { }
    95         def apply(): Bytes =
    96         {
    97           val out =
    98             new ByteArrayOutputStream(buffer.getLength + 1) {
    99               def content(): Bytes = Bytes(this.buf, 0, this.count)
   100             }
   101           write(buffer, out)
   102           out.content()
   103         }
   104       }
   105     content()
   106   }
   107 
   108 
   109   /* theory text edits */
   110 
   111   override def commit(change: Session.Change)
   112   {
   113     if (change.syntax_changed) Swing_Thread.later { jEdit.propertiesChanged() }
   114   }
   115 }
   116