src/Tools/jEdit/src/jedit_resources.scala
author wenzelm
Wed Apr 23 11:40:42 2014 +0200 (2014-04-23 ago)
changeset 56666 229309cbc508
parent 56502 db2836f65d42
child 56801 8dd9df88f647
permissions -rw-r--r--
avoid accidental use of scala.language.reflectiveCalls;
     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   private class File_Content_Output(buffer: Buffer) extends
    89     ByteArrayOutputStream(buffer.getLength + 1)
    90   {
    91     def content(): Bytes = Bytes(this.buf, 0, this.count)
    92   }
    93 
    94   private class File_Content(buffer: Buffer) extends
    95     BufferIORequest(null, buffer, null, VFSManager.getVFSForPath(buffer.getPath), buffer.getPath)
    96   {
    97     def _run() { }
    98     def content(): Bytes =
    99     {
   100       val out = new File_Content_Output(buffer)
   101       write(buffer, out)
   102       out.content()
   103     }
   104   }
   105 
   106   def file_content(buffer: Buffer): Bytes = (new File_Content(buffer)).content()
   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