# HG changeset patch # User wenzelm # Date 1314647749 -7200 # Node ID 24444588fddd75d9e4204ec47c84a2a49b966a74 # Parent 51f8895b9ad97a92f961ffb1ce28aedfd116e5cd actual auto loading of required files; eliminated File_Store in favour of Thy_Load; tuned; diff -r 51f8895b9ad9 -r 24444588fddd src/Pure/System/session.scala --- a/src/Pure/System/session.scala Mon Aug 29 16:38:56 2011 +0200 +++ b/src/Pure/System/session.scala Mon Aug 29 21:55:49 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,7 +34,7 @@ } -class Session(val file_store: Session.File_Store) +class Session(thy_load: Thy_Load) { /* real time parameters */ // FIXME properties or settings (!?) @@ -117,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 @@ -143,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 = { @@ -167,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 { @@ -187,7 +159,6 @@ private case class Start(timeout: Time, args: List[String]) private case object Interrupt - private case class Check_Loaded_Files(ask: List[String] => Boolean) private case class Init_Node(name: String, master_dir: String, header: Document.Node_Header, perspective: Text.Perspective, text: String) private case class Edit_Node(name: String, master_dir: String, @@ -337,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) } } @@ -373,8 +344,6 @@ case Interrupt if prover.isDefined => prover.get.interrupt - case Check_Loaded_Files(ask) => // FIXME - case Init_Node(name, master_dir, header, perspective, text) if prover.isDefined => // FIXME compare with existing node handle_edits(name, master_dir, header, @@ -417,11 +386,6 @@ def interrupt() { session_actor ! Interrupt } - def check_loaded_files(ask: List[String] => Boolean) - { - session_actor ! Check_Loaded_Files(ask) - } - // FIXME simplify signature def init_node(name: String, master_dir: String, header: Document.Node_Header, perspective: Text.Perspective, text: String) diff -r 51f8895b9ad9 -r 24444588fddd src/Pure/Thy/thy_info.scala --- a/src/Pure/Thy/thy_info.scala Mon Aug 29 16:38:56 2011 +0200 +++ b/src/Pure/Thy/thy_info.scala Mon Aug 29 21:55:49 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 51f8895b9ad9 -r 24444588fddd src/Pure/Thy/thy_load.scala --- a/src/Pure/Thy/thy_load.scala Mon Aug 29 16:38:56 2011 +0200 +++ b/src/Pure/Thy/thy_load.scala Mon Aug 29 21:55:49 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 51f8895b9ad9 -r 24444588fddd src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Mon Aug 29 16:38:56 2011 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Mon Aug 29 21:55:49 2011 +0200 @@ -13,9 +13,11 @@ 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} @@ -187,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 */ @@ -347,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 @@ -364,36 +373,58 @@ } } - 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) } } } - - /* session manager */ + val thy_info = new Thy_Info(thy_load) private lazy val delay_load = - Swing_Thread.delay_last(Isabelle.session.load_delay) { - def ask(files: List[String]): Boolean = Swing_Thread.now + 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 file_list = new scala.swing.TextArea(files.mkString("\n")) - file_list.editable = false - val answer = - Library.confirm_dialog(jEdit.getActiveView(), + 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?", - file_list) - answer == 0 + "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) + } - Isabelle.session.check_loaded_files(ask _) - } + + /* session manager */ private val session_manager = actor { loop { @@ -471,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)