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