src/Tools/jEdit/src/jedit_thy_load.scala
changeset 44577 96b6388d06c4
child 44580 3bc9a215a56d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Tue Aug 30 11:43:47 2011 +0200
     1.3 @@ -0,0 +1,68 @@
     1.4 +/*  Title:      Tools/jEdit/src/plugin.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Primitives for loading theory files, based on jEdit buffer content.
     1.8 +*/
     1.9 +
    1.10 +package isabelle.jedit
    1.11 +
    1.12 +
    1.13 +import isabelle._
    1.14 +
    1.15 +import java.io.File
    1.16 +import javax.swing.text.Segment
    1.17 +
    1.18 +import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
    1.19 +import org.gjt.sp.jedit.MiscUtilities
    1.20 +
    1.21 +
    1.22 +class JEdit_Thy_Load extends Thy_Load
    1.23 +{
    1.24 +  /* loaded theories provided by prover */
    1.25 +
    1.26 +  private var loaded_theories: Set[String] = Set()
    1.27 +
    1.28 +  override def register_thy(thy_name: String)
    1.29 +  {
    1.30 +    synchronized { loaded_theories += thy_name }
    1.31 +  }
    1.32 +
    1.33 +  override def is_loaded(thy_name: String): Boolean =
    1.34 +    synchronized { loaded_theories.contains(thy_name) }
    1.35 +
    1.36 +
    1.37 +  /* file-system operations */
    1.38 +
    1.39 +  override def append(master_dir: String, source_path: Path): String =
    1.40 +  {
    1.41 +    val path = source_path.expand
    1.42 +    if (path.is_absolute) Isabelle_System.platform_path(path)
    1.43 +    else {
    1.44 +      val vfs = VFSManager.getVFSForPath(master_dir)
    1.45 +      if (vfs.isInstanceOf[FileVFS])
    1.46 +        MiscUtilities.resolveSymlinks(
    1.47 +          vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
    1.48 +      else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
    1.49 +    }
    1.50 +  }
    1.51 +
    1.52 +  override def check_thy(node_name: String): Thy_Header =
    1.53 +  {
    1.54 +    Swing_Thread.now {
    1.55 +      Isabelle.jedit_buffers().find(buffer => Isabelle.buffer_name(buffer) == node_name) match {
    1.56 +        case Some(buffer) =>
    1.57 +          Isabelle.buffer_lock(buffer) {
    1.58 +            val text = new Segment
    1.59 +            buffer.getText(0, buffer.getLength, text)
    1.60 +            Some(Thy_Header.read(text))
    1.61 +          }
    1.62 +        case None => None
    1.63 +      }
    1.64 +    } getOrElse {
    1.65 +      val file = new File(node_name)  // FIXME load URL via jEdit VFS (!?)
    1.66 +      if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
    1.67 +      Thy_Header.read(file)
    1.68 +    }
    1.69 +  }
    1.70 +}
    1.71 +