src/Tools/jEdit/src/plugin.scala
changeset 44574 24444588fddd
parent 44573 51f8895b9ad9
child 44577 96b6388d06c4
     1.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Aug 29 16:38:56 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Aug 29 21:55:49 2011 +0200
     1.3 @@ -13,9 +13,11 @@
     1.4  import java.io.{File, FileInputStream, IOException}
     1.5  import java.awt.Font
     1.6  import javax.swing.JOptionPane
     1.7 +import javax.swing.text.Segment
     1.8  
     1.9  import scala.collection.mutable
    1.10  import scala.swing.ComboBox
    1.11 +import scala.util.Sorting
    1.12  
    1.13  import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
    1.14    Buffer, EditPane, MiscUtilities, ServiceManager, View}
    1.15 @@ -187,12 +189,10 @@
    1.16    def buffer_text(buffer: JEditBuffer): String =
    1.17      buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
    1.18  
    1.19 +  def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
    1.20 +
    1.21    def buffer_path(buffer: Buffer): (String, String) =
    1.22 -  {
    1.23 -    val master_dir = buffer.getDirectory
    1.24 -    val path = buffer.getSymlinkPath
    1.25 -    (master_dir, path)
    1.26 -  }
    1.27 +    (buffer.getDirectory, buffer_name(buffer))
    1.28  
    1.29  
    1.30    /* document model and view */
    1.31 @@ -347,10 +347,19 @@
    1.32  
    1.33  class Plugin extends EBPlugin
    1.34  {
    1.35 -  /* editor file store */
    1.36 +  /* theory files via editor document model */
    1.37 +
    1.38 +  val thy_load = new Thy_Load
    1.39 +  {
    1.40 +    private var loaded_theories: Set[String] = Set()
    1.41  
    1.42 -  private val file_store = new Session.File_Store
    1.43 -  {
    1.44 +    def register_thy(thy_name: String)
    1.45 +    {
    1.46 +      synchronized { loaded_theories += thy_name }
    1.47 +    }
    1.48 +    def is_loaded(thy_name: String): Boolean =
    1.49 +      synchronized { loaded_theories.contains(thy_name) }
    1.50 +
    1.51      def append(master_dir: String, source_path: Path): String =
    1.52      {
    1.53        val path = source_path.expand
    1.54 @@ -364,36 +373,58 @@
    1.55        }
    1.56      }
    1.57  
    1.58 -    def require(canonical_name: String)
    1.59 +    def check_thy(node_name: String): Thy_Header =
    1.60      {
    1.61 -      Swing_Thread.later {
    1.62 -        if (!Isabelle.jedit_buffers().exists(_.getSymlinkPath == canonical_name))
    1.63 -          jEdit.openFile(null: View, canonical_name)
    1.64 +      Swing_Thread.now {
    1.65 +        Isabelle.jedit_buffers().find(buffer => Isabelle.buffer_name(buffer) == node_name) match {
    1.66 +          case Some(buffer) =>
    1.67 +            Isabelle.buffer_lock(buffer) {
    1.68 +              val text = new Segment
    1.69 +              buffer.getText(0, buffer.getLength, text)
    1.70 +              Some(Thy_Header.read(text))
    1.71 +            }
    1.72 +          case None => None
    1.73 +        }
    1.74 +      } getOrElse {
    1.75 +        val file = new File(node_name)  // FIXME load URL via jEdit VFS (!?)
    1.76 +        if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
    1.77 +        Thy_Header.read(file)
    1.78        }
    1.79      }
    1.80    }
    1.81  
    1.82 -
    1.83 -  /* session manager */
    1.84 +  val thy_info = new Thy_Info(thy_load)
    1.85  
    1.86    private lazy val delay_load =
    1.87 -    Swing_Thread.delay_last(Isabelle.session.load_delay) {
    1.88 -      def ask(files: List[String]): Boolean = Swing_Thread.now
    1.89 +    Swing_Thread.delay_last(Isabelle.session.load_delay)
    1.90 +    {
    1.91 +      val buffers = Isabelle.jedit_buffers().toList
    1.92 +      def loaded_buffer(name: String): Boolean =
    1.93 +        buffers.exists(buffer => Isabelle.buffer_name(buffer) == name)
    1.94 +
    1.95 +      val thys =
    1.96 +        for (buffer <- buffers; model <- Isabelle.document_model(buffer))
    1.97 +          yield (model.master_dir, model.thy_name)
    1.98 +      val files = thy_info.dependencies(thys).map(_._1).filterNot(loaded_buffer _)
    1.99 +
   1.100 +      val do_load = !files.isEmpty &&
   1.101          {
   1.102 -          val file_list = new scala.swing.TextArea(files.mkString("\n"))
   1.103 -          file_list.editable = false
   1.104 -          val answer =
   1.105 -            Library.confirm_dialog(jEdit.getActiveView(),
   1.106 +          val files_sorted = { val a = files.toArray; Sorting.quickSort(a); a.toList }
   1.107 +          val files_text = new scala.swing.TextArea(files_sorted.mkString("\n"))
   1.108 +          files_text.editable = false
   1.109 +          Library.confirm_dialog(jEdit.getActiveView(),
   1.110              "Auto loading of required files",
   1.111              JOptionPane.YES_NO_OPTION,
   1.112 -            "The following files are required to resolve theory imports.",
   1.113 -            "Reload now?",
   1.114 -            file_list)
   1.115 -          answer == 0
   1.116 +            "The following files are required to resolve theory imports.  Reload now?",
   1.117 +            files_text) == 0
   1.118          }
   1.119 +      if (do_load)
   1.120 +        for (file <- files if !loaded_buffer(file))
   1.121 +          jEdit.openFile(null: View, file)
   1.122 +    }
   1.123  
   1.124 -      Isabelle.session.check_loaded_files(ask _)
   1.125 -    }
   1.126 +
   1.127 +  /* session manager */
   1.128  
   1.129    private val session_manager = actor {
   1.130      loop {
   1.131 @@ -471,7 +502,7 @@
   1.132      Isabelle.setup_tooltips()
   1.133      Isabelle_System.init()
   1.134      Isabelle_System.install_fonts()
   1.135 -    Isabelle.session = new Session(file_store)
   1.136 +    Isabelle.session = new Session(thy_load)
   1.137      SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
   1.138      if (ModeProvider.instance.isInstanceOf[ModeProvider])
   1.139        ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)