src/Tools/jEdit/src/jedit_thy_load.scala
author wenzelm
Tue Aug 30 15:43:27 2011 +0200 (2011-08-30)
changeset 44580 3bc9a215a56d
parent 44577 96b6388d06c4
child 44615 a4ff8a787202
permissions -rw-r--r--
some support for hyperlinks between different buffers;
tuned signature;
     1 /*  Title:      Tools/jEdit/src/plugin.scala
     2     Author:     Makarius
     3 
     4 Primitives for loading theory files, based on jEdit buffer content.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import java.io.File
    13 import javax.swing.text.Segment
    14 
    15 import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
    16 import org.gjt.sp.jedit.MiscUtilities
    17 
    18 
    19 class JEdit_Thy_Load extends Thy_Load
    20 {
    21   /* loaded theories provided by prover */
    22 
    23   private var loaded_theories: Set[String] = Set()
    24 
    25   override def register_thy(thy_name: String)
    26   {
    27     synchronized { loaded_theories += thy_name }
    28   }
    29 
    30   override def is_loaded(thy_name: String): Boolean =
    31     synchronized { loaded_theories.contains(thy_name) }
    32 
    33 
    34   /* file-system operations */
    35 
    36   override def append(master_dir: String, source_path: Path): String =
    37   {
    38     val path = source_path.expand
    39     if (path.is_absolute) Isabelle_System.platform_path(path)
    40     else {
    41       val vfs = VFSManager.getVFSForPath(master_dir)
    42       if (vfs.isInstanceOf[FileVFS])
    43         MiscUtilities.resolveSymlinks(
    44           vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
    45       else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
    46     }
    47   }
    48 
    49   override def check_thy(node_name: String): Thy_Header =
    50   {
    51     Swing_Thread.now {
    52       Isabelle.jedit_buffer(node_name) match {
    53         case Some(buffer) =>
    54           Isabelle.buffer_lock(buffer) {
    55             val text = new Segment
    56             buffer.getText(0, buffer.getLength, text)
    57             Some(Thy_Header.read(text))
    58           }
    59         case None => None
    60       }
    61     } getOrElse {
    62       val file = new File(node_name)  // FIXME load URL via jEdit VFS (!?)
    63       if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
    64       Thy_Header.read(file)
    65     }
    66   }
    67 }
    68