separate module for jEdit primitives for loading theory files;
authorwenzelm
Tue Aug 30 11:43:47 2011 +0200 (2011-08-30)
changeset 4457796b6388d06c4
parent 44576 f23ac1a679d1
child 44578 ca3844a3dcf7
separate module for jEdit primitives for loading theory files;
src/Pure/Thy/thy_load.scala
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/jedit_thy_load.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/Thy/thy_load.scala	Mon Aug 29 22:10:08 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_load.scala	Tue Aug 30 11:43:47 2011 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  /*  Title:      Pure/Thy/thy_load.scala
     1.5      Author:     Makarius
     1.6  
     1.7 -Loading files that contribute to a theory.
     1.8 +Primitives for loading theory files.
     1.9  */
    1.10  
    1.11  package isabelle
     2.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Mon Aug 29 22:10:08 2011 +0200
     2.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Tue Aug 30 11:43:47 2011 +0200
     2.3 @@ -17,6 +17,7 @@
     2.4    "src/isabelle_markup.scala"
     2.5    "src/isabelle_options.scala"
     2.6    "src/isabelle_sidekick.scala"
     2.7 +  "src/jedit_thy_load.scala"
     2.8    "src/output_dockable.scala"
     2.9    "src/plugin.scala"
    2.10    "src/protocol_dockable.scala"
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Tue Aug 30 11:43:47 2011 +0200
     3.3 @@ -0,0 +1,68 @@
     3.4 +/*  Title:      Tools/jEdit/src/plugin.scala
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Primitives for loading theory files, based on jEdit buffer content.
     3.8 +*/
     3.9 +
    3.10 +package isabelle.jedit
    3.11 +
    3.12 +
    3.13 +import isabelle._
    3.14 +
    3.15 +import java.io.File
    3.16 +import javax.swing.text.Segment
    3.17 +
    3.18 +import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
    3.19 +import org.gjt.sp.jedit.MiscUtilities
    3.20 +
    3.21 +
    3.22 +class JEdit_Thy_Load extends Thy_Load
    3.23 +{
    3.24 +  /* loaded theories provided by prover */
    3.25 +
    3.26 +  private var loaded_theories: Set[String] = Set()
    3.27 +
    3.28 +  override def register_thy(thy_name: String)
    3.29 +  {
    3.30 +    synchronized { loaded_theories += thy_name }
    3.31 +  }
    3.32 +
    3.33 +  override def is_loaded(thy_name: String): Boolean =
    3.34 +    synchronized { loaded_theories.contains(thy_name) }
    3.35 +
    3.36 +
    3.37 +  /* file-system operations */
    3.38 +
    3.39 +  override def append(master_dir: String, source_path: Path): String =
    3.40 +  {
    3.41 +    val path = source_path.expand
    3.42 +    if (path.is_absolute) Isabelle_System.platform_path(path)
    3.43 +    else {
    3.44 +      val vfs = VFSManager.getVFSForPath(master_dir)
    3.45 +      if (vfs.isInstanceOf[FileVFS])
    3.46 +        MiscUtilities.resolveSymlinks(
    3.47 +          vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
    3.48 +      else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
    3.49 +    }
    3.50 +  }
    3.51 +
    3.52 +  override def check_thy(node_name: String): Thy_Header =
    3.53 +  {
    3.54 +    Swing_Thread.now {
    3.55 +      Isabelle.jedit_buffers().find(buffer => Isabelle.buffer_name(buffer) == node_name) match {
    3.56 +        case Some(buffer) =>
    3.57 +          Isabelle.buffer_lock(buffer) {
    3.58 +            val text = new Segment
    3.59 +            buffer.getText(0, buffer.getLength, text)
    3.60 +            Some(Thy_Header.read(text))
    3.61 +          }
    3.62 +        case None => None
    3.63 +      }
    3.64 +    } getOrElse {
    3.65 +      val file = new File(node_name)  // FIXME load URL via jEdit VFS (!?)
    3.66 +      if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
    3.67 +      Thy_Header.read(file)
    3.68 +    }
    3.69 +  }
    3.70 +}
    3.71 +
     4.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Aug 29 22:10:08 2011 +0200
     4.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 30 11:43:47 2011 +0200
     4.3 @@ -10,23 +10,20 @@
     4.4  import isabelle._
     4.5  
     4.6  import java.lang.System
     4.7 -import java.io.{File, FileInputStream, IOException}
     4.8  import java.awt.Font
     4.9  import javax.swing.JOptionPane
    4.10 -import javax.swing.text.Segment
    4.11  
    4.12  import scala.collection.mutable
    4.13  import scala.swing.ComboBox
    4.14  import scala.util.Sorting
    4.15  
    4.16  import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
    4.17 -  Buffer, EditPane, MiscUtilities, ServiceManager, View}
    4.18 +  Buffer, EditPane, ServiceManager, View}
    4.19  import org.gjt.sp.jedit.buffer.JEditBuffer
    4.20  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
    4.21  import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider}
    4.22  import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
    4.23  import org.gjt.sp.jedit.gui.DockableWindowManager
    4.24 -import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
    4.25  
    4.26  import org.gjt.sp.util.SyntaxUtilities
    4.27  import org.gjt.sp.util.Log
    4.28 @@ -347,52 +344,9 @@
    4.29  
    4.30  class Plugin extends EBPlugin
    4.31  {
    4.32 -  /* theory files via editor document model */
    4.33 -
    4.34 -  val thy_load = new Thy_Load
    4.35 -  {
    4.36 -    private var loaded_theories: Set[String] = Set()
    4.37 -
    4.38 -    def register_thy(thy_name: String)
    4.39 -    {
    4.40 -      synchronized { loaded_theories += thy_name }
    4.41 -    }
    4.42 -    def is_loaded(thy_name: String): Boolean =
    4.43 -      synchronized { loaded_theories.contains(thy_name) }
    4.44 +  /* theory files */
    4.45  
    4.46 -    def append(master_dir: String, source_path: Path): String =
    4.47 -    {
    4.48 -      val path = source_path.expand
    4.49 -      if (path.is_absolute) Isabelle_System.platform_path(path)
    4.50 -      else {
    4.51 -        val vfs = VFSManager.getVFSForPath(master_dir)
    4.52 -        if (vfs.isInstanceOf[FileVFS])
    4.53 -          MiscUtilities.resolveSymlinks(
    4.54 -            vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
    4.55 -        else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
    4.56 -      }
    4.57 -    }
    4.58 -
    4.59 -    def check_thy(node_name: String): Thy_Header =
    4.60 -    {
    4.61 -      Swing_Thread.now {
    4.62 -        Isabelle.jedit_buffers().find(buffer => Isabelle.buffer_name(buffer) == node_name) match {
    4.63 -          case Some(buffer) =>
    4.64 -            Isabelle.buffer_lock(buffer) {
    4.65 -              val text = new Segment
    4.66 -              buffer.getText(0, buffer.getLength, text)
    4.67 -              Some(Thy_Header.read(text))
    4.68 -            }
    4.69 -          case None => None
    4.70 -        }
    4.71 -      } getOrElse {
    4.72 -        val file = new File(node_name)  // FIXME load URL via jEdit VFS (!?)
    4.73 -        if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
    4.74 -        Thy_Header.read(file)
    4.75 -      }
    4.76 -    }
    4.77 -  }
    4.78 -
    4.79 +  val thy_load = new JEdit_Thy_Load
    4.80    val thy_info = new Thy_Info(thy_load)
    4.81  
    4.82    private lazy val delay_load =