--- a/src/Pure/System/session.scala Mon Aug 29 08:31:09 2011 -0700
+++ b/src/Pure/System/session.scala Mon Aug 29 22:10:08 2011 +0200
@@ -16,15 +16,6 @@
object Session
{
- /* file store */
-
- abstract class File_Store
- {
- def append(master_dir: String, path: Path): String
- def require(file: String): Unit
- }
-
-
/* events */
//{{{
@@ -43,13 +34,14 @@
}
-class Session(val file_store: Session.File_Store)
+class Session(thy_load: Thy_Load)
{
/* real time parameters */ // FIXME properties or settings (!?)
val input_delay = Time.seconds(0.3) // user input (e.g. text edits, cursor movement)
val output_delay = Time.seconds(0.1) // prover output (markup, common messages)
val update_delay = Time.seconds(0.5) // GUI layout updates
+ val load_delay = Time.seconds(0.5) // file load operations (new buffers etc.)
/* pervasive event buses */
@@ -116,8 +108,6 @@
@volatile var verbose: Boolean = false
- @volatile private var loaded_theories: Set[String] = Set()
-
@volatile private var syntax = new Outer_Syntax
def current_syntax(): Outer_Syntax = syntax
@@ -142,23 +132,6 @@
/* theory files */
- val thy_load = new Thy_Load
- {
- override def is_loaded(name: String): Boolean =
- loaded_theories.contains(name)
-
- override def check_thy(dir: Path, name: String): (String, Thy_Header) =
- {
- val file = Isabelle_System.platform_file(dir + Thy_Header.thy_path(name))
- if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
- val text = Standard_System.read_file(file)
- val header = Thy_Header.read(text)
- (text, header)
- }
- }
-
- val thy_info = new Thy_Info(thy_load)
-
def header_edit(name: String, master_dir: String,
header: Document.Node_Header): Document.Edit_Text =
{
@@ -166,10 +139,10 @@
{
val thy_name = Thy_Header.base_name(s)
if (thy_load.is_loaded(thy_name)) thy_name
- else file_store.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
+ else thy_load.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
}
def norm_use(s: String): String =
- file_store.append(master_dir, Path.explode(s))
+ thy_load.append(master_dir, Path.explode(s))
val header1: Document.Node_Header =
header match {
@@ -335,7 +308,7 @@
catch { case _: Document.State.Fail => bad_result(result) }
case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
case List(Keyword.Keyword_Decl(name)) => syntax += name
- case List(Thy_Info.Loaded_Theory(name)) => loaded_theories += name
+ case List(Thy_Info.Loaded_Theory(name)) => thy_load.register_thy(name)
case _ => bad_result(result)
}
}
--- a/src/Pure/System/swing_thread.scala Mon Aug 29 08:31:09 2011 -0700
+++ b/src/Pure/System/swing_thread.scala Mon Aug 29 22:10:08 2011 +0200
@@ -52,7 +52,7 @@
val timer = new Timer(time.ms.toInt, listener)
timer.setRepeats(false)
- def invoke() { if (first) timer.start() else timer.restart() }
+ def invoke() { now { if (first) timer.start() else timer.restart() } }
invoke _
}
--- a/src/Pure/Thy/thy_info.scala Mon Aug 29 08:31:09 2011 -0700
+++ b/src/Pure/Thy/thy_info.scala Mon Aug 29 22:10:08 2011 +0200
@@ -38,37 +38,38 @@
/* dependencies */
- type Deps = Map[String, Exn.Result[(String, Thy_Header)]] // name -> (text, header)
+ type Deps = Map[String, Document.Node_Header]
- private def require_thys(ignored: String => Boolean,
- initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps =
- (deps /: strs)(require_thy(ignored, initiators, dir, _, _))
+ private def require_thys(initiators: List[String],
+ deps: Deps, thys: List[(String, String)]): Deps =
+ (deps /: thys)(require_thy(initiators, _, _))
- private def require_thy(ignored: String => Boolean,
- initiators: List[String], dir: Path, deps: Deps, str: String): Deps =
+ private def require_thy(initiators: List[String], deps: Deps, thy: (String, String)): Deps =
{
+ val (dir, str) = thy
val path = Path.explode(str)
- val name = path.base.implode
+ val thy_name = path.base.implode
+ val node_name = thy_load.append(dir, Thy_Header.thy_path(path))
- if (deps.isDefinedAt(name) || ignored(name)) deps
+ if (deps.isDefinedAt(node_name) || thy_load.is_loaded(thy_name)) deps
else {
- val dir1 = dir + path.dir
+ val dir1 = thy_load.append(dir, path.dir)
try {
- if (initiators.contains(name)) error(cycle_msg(initiators))
- val (text, header) =
- try { thy_load.check_thy(dir1, name) }
+ if (initiators.contains(node_name)) error(cycle_msg(initiators))
+ val header =
+ try { thy_load.check_thy(node_name) }
catch {
case ERROR(msg) =>
- cat_error(msg, "The error(s) above occurred while examining theory " +
- quote(name) + required_by("\n", initiators))
+ cat_error(msg, "The error(s) above occurred while examining theory file " +
+ quote(node_name) + required_by("\n", initiators))
}
- require_thys(ignored, name :: initiators, dir1,
- deps + (name -> Exn.Res(text, header)), header.imports)
+ val thys = header.imports.map(str => (dir1, str))
+ require_thys(node_name :: initiators, deps + (node_name -> Exn.Res(header)), thys)
}
- catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
+ catch { case e: Throwable => deps + (node_name -> Exn.Exn(e)) }
}
}
- def dependencies(dir: Path, str: String): Deps =
- require_thy(thy_load.is_loaded, Nil, dir, Map.empty, str)
+ def dependencies(thys: List[(String, String)]): Deps =
+ require_thys(Nil, Map.empty, thys)
}
--- a/src/Pure/Thy/thy_load.scala Mon Aug 29 08:31:09 2011 -0700
+++ b/src/Pure/Thy/thy_load.scala Mon Aug 29 22:10:08 2011 +0200
@@ -8,8 +8,9 @@
abstract class Thy_Load
{
- def is_loaded(name: String): Boolean
-
- def check_thy(dir: Path, name: String): (String, Thy_Header)
+ def register_thy(thy_name: String)
+ def is_loaded(thy_name: String): Boolean
+ def append(master_dir: String, path: Path): String
+ def check_thy(node_name: String): Thy_Header
}
--- a/src/Pure/library.scala Mon Aug 29 08:31:09 2011 -0700
+++ b/src/Pure/library.scala Mon Aug 29 22:10:08 2011 +0200
@@ -142,6 +142,14 @@
def warning_dialog = simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning") _
def error_dialog = simple_dialog(JOptionPane.ERROR_MESSAGE, "Error") _
+ def confirm_dialog(parent: Component, title: String, option_type: Int, message: Any*): Int =
+ Swing_Thread.now {
+ val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
+ JOptionPane.showConfirmDialog(parent,
+ java_message.toArray.asInstanceOf[Array[AnyRef]], title,
+ option_type, JOptionPane.QUESTION_MESSAGE)
+ }
+
/* zoom box */
--- a/src/Tools/jEdit/src/plugin.scala Mon Aug 29 08:31:09 2011 -0700
+++ b/src/Tools/jEdit/src/plugin.scala Mon Aug 29 22:10:08 2011 +0200
@@ -12,9 +12,12 @@
import java.lang.System
import java.io.{File, FileInputStream, IOException}
import java.awt.Font
+import javax.swing.JOptionPane
+import javax.swing.text.Segment
import scala.collection.mutable
import scala.swing.ComboBox
+import scala.util.Sorting
import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
Buffer, EditPane, MiscUtilities, ServiceManager, View}
@@ -186,12 +189,10 @@
def buffer_text(buffer: JEditBuffer): String =
buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
+ def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
+
def buffer_path(buffer: Buffer): (String, String) =
- {
- val master_dir = buffer.getDirectory
- val path = buffer.getSymlinkPath
- (master_dir, path)
- }
+ (buffer.getDirectory, buffer_name(buffer))
/* document model and view */
@@ -346,10 +347,19 @@
class Plugin extends EBPlugin
{
- /* editor file store */
+ /* theory files via editor document model */
+
+ val thy_load = new Thy_Load
+ {
+ private var loaded_theories: Set[String] = Set()
- private val file_store = new Session.File_Store
- {
+ def register_thy(thy_name: String)
+ {
+ synchronized { loaded_theories += thy_name }
+ }
+ def is_loaded(thy_name: String): Boolean =
+ synchronized { loaded_theories.contains(thy_name) }
+
def append(master_dir: String, source_path: Path): String =
{
val path = source_path.expand
@@ -363,15 +373,56 @@
}
}
- def require(canonical_name: String)
+ def check_thy(node_name: String): Thy_Header =
{
- Swing_Thread.later {
- if (!Isabelle.jedit_buffers().exists(_.getSymlinkPath == canonical_name))
- jEdit.openFile(null: View, canonical_name)
+ Swing_Thread.now {
+ Isabelle.jedit_buffers().find(buffer => Isabelle.buffer_name(buffer) == node_name) match {
+ case Some(buffer) =>
+ Isabelle.buffer_lock(buffer) {
+ val text = new Segment
+ buffer.getText(0, buffer.getLength, text)
+ Some(Thy_Header.read(text))
+ }
+ case None => None
+ }
+ } getOrElse {
+ val file = new File(node_name) // FIXME load URL via jEdit VFS (!?)
+ if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
+ Thy_Header.read(file)
}
}
}
+ val thy_info = new Thy_Info(thy_load)
+
+ private lazy val delay_load =
+ Swing_Thread.delay_last(Isabelle.session.load_delay)
+ {
+ val buffers = Isabelle.jedit_buffers().toList
+ def loaded_buffer(name: String): Boolean =
+ buffers.exists(buffer => Isabelle.buffer_name(buffer) == name)
+
+ val thys =
+ for (buffer <- buffers; model <- Isabelle.document_model(buffer))
+ yield (model.master_dir, model.thy_name)
+ val files = thy_info.dependencies(thys).map(_._1).filterNot(loaded_buffer _)
+
+ val do_load = !files.isEmpty &&
+ {
+ val files_sorted = { val a = files.toArray; Sorting.quickSort(a); a.toList }
+ val files_text = new scala.swing.TextArea(files_sorted.mkString("\n"))
+ files_text.editable = false
+ Library.confirm_dialog(jEdit.getActiveView(),
+ "Auto loading of required files",
+ JOptionPane.YES_NO_OPTION,
+ "The following files are required to resolve theory imports. Reload now?",
+ files_text) == 0
+ }
+ if (do_load)
+ for (file <- files if !loaded_buffer(file))
+ jEdit.openFile(null: View, file)
+ }
+
/* session manager */
@@ -387,7 +438,10 @@
Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
}
- case Session.Ready => Isabelle.jedit_buffers.foreach(Isabelle.init_model)
+ case Session.Ready =>
+ Isabelle.jedit_buffers.foreach(Isabelle.init_model)
+ delay_load()
+
case Session.Shutdown => Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
case _ =>
}
@@ -410,17 +464,17 @@
case msg: BufferUpdate
if msg.getWhat == BufferUpdate.LOADED =>
-
- val buffer = msg.getBuffer
- if (buffer != null && Isabelle.session.is_ready)
- Isabelle.init_model(buffer)
+ if (Isabelle.session.is_ready) {
+ val buffer = msg.getBuffer
+ if (buffer != null) Isabelle.init_model(buffer)
+ delay_load()
+ }
case msg: EditPaneUpdate
if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
msg.getWhat == EditPaneUpdate.CREATED ||
msg.getWhat == EditPaneUpdate.DESTROYED) =>
-
val edit_pane = msg.getEditPane
val buffer = edit_pane.getBuffer
val text_area = edit_pane.getTextArea
@@ -448,7 +502,7 @@
Isabelle.setup_tooltips()
Isabelle_System.init()
Isabelle_System.install_fonts()
- Isabelle.session = new Session(file_store)
+ Isabelle.session = new Session(thy_load)
SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
if (ModeProvider.instance.isInstanceOf[ModeProvider])
ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)