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