# HG changeset patch # User wenzelm # Date 1314648608 -7200 # Node ID f23ac1a679d1ec91076ea3f170bd80e0bdec3bc5 # Parent c5e42b8590dd52b385ad25e35aae82040e1bcee6# Parent 24444588fddd75d9e4204ec47c84a2a49b966a74 merged diff -r c5e42b8590dd -r f23ac1a679d1 src/Pure/System/session.scala --- 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) } } diff -r c5e42b8590dd -r f23ac1a679d1 src/Pure/System/swing_thread.scala --- 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 _ } diff -r c5e42b8590dd -r f23ac1a679d1 src/Pure/Thy/thy_info.scala --- 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) } diff -r c5e42b8590dd -r f23ac1a679d1 src/Pure/Thy/thy_load.scala --- 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 } diff -r c5e42b8590dd -r f23ac1a679d1 src/Pure/library.scala --- 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 */ diff -r c5e42b8590dd -r f23ac1a679d1 src/Tools/jEdit/src/plugin.scala --- 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)