1.1 --- a/src/Pure/System/session.scala Mon Aug 29 08:31:09 2011 -0700
1.2 +++ b/src/Pure/System/session.scala Mon Aug 29 22:10:08 2011 +0200
1.3 @@ -16,15 +16,6 @@
1.4
1.5 object Session
1.6 {
1.7 - /* file store */
1.8 -
1.9 - abstract class File_Store
1.10 - {
1.11 - def append(master_dir: String, path: Path): String
1.12 - def require(file: String): Unit
1.13 - }
1.14 -
1.15 -
1.16 /* events */
1.17
1.18 //{{{
1.19 @@ -43,13 +34,14 @@
1.20 }
1.21
1.22
1.23 -class Session(val file_store: Session.File_Store)
1.24 +class Session(thy_load: Thy_Load)
1.25 {
1.26 /* real time parameters */ // FIXME properties or settings (!?)
1.27
1.28 val input_delay = Time.seconds(0.3) // user input (e.g. text edits, cursor movement)
1.29 val output_delay = Time.seconds(0.1) // prover output (markup, common messages)
1.30 val update_delay = Time.seconds(0.5) // GUI layout updates
1.31 + val load_delay = Time.seconds(0.5) // file load operations (new buffers etc.)
1.32
1.33
1.34 /* pervasive event buses */
1.35 @@ -116,8 +108,6 @@
1.36
1.37 @volatile var verbose: Boolean = false
1.38
1.39 - @volatile private var loaded_theories: Set[String] = Set()
1.40 -
1.41 @volatile private var syntax = new Outer_Syntax
1.42 def current_syntax(): Outer_Syntax = syntax
1.43
1.44 @@ -142,23 +132,6 @@
1.45
1.46 /* theory files */
1.47
1.48 - val thy_load = new Thy_Load
1.49 - {
1.50 - override def is_loaded(name: String): Boolean =
1.51 - loaded_theories.contains(name)
1.52 -
1.53 - override def check_thy(dir: Path, name: String): (String, Thy_Header) =
1.54 - {
1.55 - val file = Isabelle_System.platform_file(dir + Thy_Header.thy_path(name))
1.56 - if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
1.57 - val text = Standard_System.read_file(file)
1.58 - val header = Thy_Header.read(text)
1.59 - (text, header)
1.60 - }
1.61 - }
1.62 -
1.63 - val thy_info = new Thy_Info(thy_load)
1.64 -
1.65 def header_edit(name: String, master_dir: String,
1.66 header: Document.Node_Header): Document.Edit_Text =
1.67 {
1.68 @@ -166,10 +139,10 @@
1.69 {
1.70 val thy_name = Thy_Header.base_name(s)
1.71 if (thy_load.is_loaded(thy_name)) thy_name
1.72 - else file_store.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
1.73 + else thy_load.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
1.74 }
1.75 def norm_use(s: String): String =
1.76 - file_store.append(master_dir, Path.explode(s))
1.77 + thy_load.append(master_dir, Path.explode(s))
1.78
1.79 val header1: Document.Node_Header =
1.80 header match {
1.81 @@ -335,7 +308,7 @@
1.82 catch { case _: Document.State.Fail => bad_result(result) }
1.83 case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
1.84 case List(Keyword.Keyword_Decl(name)) => syntax += name
1.85 - case List(Thy_Info.Loaded_Theory(name)) => loaded_theories += name
1.86 + case List(Thy_Info.Loaded_Theory(name)) => thy_load.register_thy(name)
1.87 case _ => bad_result(result)
1.88 }
1.89 }
2.1 --- a/src/Pure/System/swing_thread.scala Mon Aug 29 08:31:09 2011 -0700
2.2 +++ b/src/Pure/System/swing_thread.scala Mon Aug 29 22:10:08 2011 +0200
2.3 @@ -52,7 +52,7 @@
2.4 val timer = new Timer(time.ms.toInt, listener)
2.5 timer.setRepeats(false)
2.6
2.7 - def invoke() { if (first) timer.start() else timer.restart() }
2.8 + def invoke() { now { if (first) timer.start() else timer.restart() } }
2.9 invoke _
2.10 }
2.11
3.1 --- a/src/Pure/Thy/thy_info.scala Mon Aug 29 08:31:09 2011 -0700
3.2 +++ b/src/Pure/Thy/thy_info.scala Mon Aug 29 22:10:08 2011 +0200
3.3 @@ -38,37 +38,38 @@
3.4
3.5 /* dependencies */
3.6
3.7 - type Deps = Map[String, Exn.Result[(String, Thy_Header)]] // name -> (text, header)
3.8 + type Deps = Map[String, Document.Node_Header]
3.9
3.10 - private def require_thys(ignored: String => Boolean,
3.11 - initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps =
3.12 - (deps /: strs)(require_thy(ignored, initiators, dir, _, _))
3.13 + private def require_thys(initiators: List[String],
3.14 + deps: Deps, thys: List[(String, String)]): Deps =
3.15 + (deps /: thys)(require_thy(initiators, _, _))
3.16
3.17 - private def require_thy(ignored: String => Boolean,
3.18 - initiators: List[String], dir: Path, deps: Deps, str: String): Deps =
3.19 + private def require_thy(initiators: List[String], deps: Deps, thy: (String, String)): Deps =
3.20 {
3.21 + val (dir, str) = thy
3.22 val path = Path.explode(str)
3.23 - val name = path.base.implode
3.24 + val thy_name = path.base.implode
3.25 + val node_name = thy_load.append(dir, Thy_Header.thy_path(path))
3.26
3.27 - if (deps.isDefinedAt(name) || ignored(name)) deps
3.28 + if (deps.isDefinedAt(node_name) || thy_load.is_loaded(thy_name)) deps
3.29 else {
3.30 - val dir1 = dir + path.dir
3.31 + val dir1 = thy_load.append(dir, path.dir)
3.32 try {
3.33 - if (initiators.contains(name)) error(cycle_msg(initiators))
3.34 - val (text, header) =
3.35 - try { thy_load.check_thy(dir1, name) }
3.36 + if (initiators.contains(node_name)) error(cycle_msg(initiators))
3.37 + val header =
3.38 + try { thy_load.check_thy(node_name) }
3.39 catch {
3.40 case ERROR(msg) =>
3.41 - cat_error(msg, "The error(s) above occurred while examining theory " +
3.42 - quote(name) + required_by("\n", initiators))
3.43 + cat_error(msg, "The error(s) above occurred while examining theory file " +
3.44 + quote(node_name) + required_by("\n", initiators))
3.45 }
3.46 - require_thys(ignored, name :: initiators, dir1,
3.47 - deps + (name -> Exn.Res(text, header)), header.imports)
3.48 + val thys = header.imports.map(str => (dir1, str))
3.49 + require_thys(node_name :: initiators, deps + (node_name -> Exn.Res(header)), thys)
3.50 }
3.51 - catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
3.52 + catch { case e: Throwable => deps + (node_name -> Exn.Exn(e)) }
3.53 }
3.54 }
3.55
3.56 - def dependencies(dir: Path, str: String): Deps =
3.57 - require_thy(thy_load.is_loaded, Nil, dir, Map.empty, str)
3.58 + def dependencies(thys: List[(String, String)]): Deps =
3.59 + require_thys(Nil, Map.empty, thys)
3.60 }
4.1 --- a/src/Pure/Thy/thy_load.scala Mon Aug 29 08:31:09 2011 -0700
4.2 +++ b/src/Pure/Thy/thy_load.scala Mon Aug 29 22:10:08 2011 +0200
4.3 @@ -8,8 +8,9 @@
4.4
4.5 abstract class Thy_Load
4.6 {
4.7 - def is_loaded(name: String): Boolean
4.8 -
4.9 - def check_thy(dir: Path, name: String): (String, Thy_Header)
4.10 + def register_thy(thy_name: String)
4.11 + def is_loaded(thy_name: String): Boolean
4.12 + def append(master_dir: String, path: Path): String
4.13 + def check_thy(node_name: String): Thy_Header
4.14 }
4.15
5.1 --- a/src/Pure/library.scala Mon Aug 29 08:31:09 2011 -0700
5.2 +++ b/src/Pure/library.scala Mon Aug 29 22:10:08 2011 +0200
5.3 @@ -142,6 +142,14 @@
5.4 def warning_dialog = simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning") _
5.5 def error_dialog = simple_dialog(JOptionPane.ERROR_MESSAGE, "Error") _
5.6
5.7 + def confirm_dialog(parent: Component, title: String, option_type: Int, message: Any*): Int =
5.8 + Swing_Thread.now {
5.9 + val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
5.10 + JOptionPane.showConfirmDialog(parent,
5.11 + java_message.toArray.asInstanceOf[Array[AnyRef]], title,
5.12 + option_type, JOptionPane.QUESTION_MESSAGE)
5.13 + }
5.14 +
5.15
5.16 /* zoom box */
5.17
6.1 --- a/src/Tools/jEdit/src/plugin.scala Mon Aug 29 08:31:09 2011 -0700
6.2 +++ b/src/Tools/jEdit/src/plugin.scala Mon Aug 29 22:10:08 2011 +0200
6.3 @@ -12,9 +12,12 @@
6.4 import java.lang.System
6.5 import java.io.{File, FileInputStream, IOException}
6.6 import java.awt.Font
6.7 +import javax.swing.JOptionPane
6.8 +import javax.swing.text.Segment
6.9
6.10 import scala.collection.mutable
6.11 import scala.swing.ComboBox
6.12 +import scala.util.Sorting
6.13
6.14 import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
6.15 Buffer, EditPane, MiscUtilities, ServiceManager, View}
6.16 @@ -186,12 +189,10 @@
6.17 def buffer_text(buffer: JEditBuffer): String =
6.18 buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
6.19
6.20 + def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
6.21 +
6.22 def buffer_path(buffer: Buffer): (String, String) =
6.23 - {
6.24 - val master_dir = buffer.getDirectory
6.25 - val path = buffer.getSymlinkPath
6.26 - (master_dir, path)
6.27 - }
6.28 + (buffer.getDirectory, buffer_name(buffer))
6.29
6.30
6.31 /* document model and view */
6.32 @@ -346,10 +347,19 @@
6.33
6.34 class Plugin extends EBPlugin
6.35 {
6.36 - /* editor file store */
6.37 + /* theory files via editor document model */
6.38
6.39 - private val file_store = new Session.File_Store
6.40 + val thy_load = new Thy_Load
6.41 {
6.42 + private var loaded_theories: Set[String] = Set()
6.43 +
6.44 + def register_thy(thy_name: String)
6.45 + {
6.46 + synchronized { loaded_theories += thy_name }
6.47 + }
6.48 + def is_loaded(thy_name: String): Boolean =
6.49 + synchronized { loaded_theories.contains(thy_name) }
6.50 +
6.51 def append(master_dir: String, source_path: Path): String =
6.52 {
6.53 val path = source_path.expand
6.54 @@ -363,15 +373,56 @@
6.55 }
6.56 }
6.57
6.58 - def require(canonical_name: String)
6.59 + def check_thy(node_name: String): Thy_Header =
6.60 {
6.61 - Swing_Thread.later {
6.62 - if (!Isabelle.jedit_buffers().exists(_.getSymlinkPath == canonical_name))
6.63 - jEdit.openFile(null: View, canonical_name)
6.64 + Swing_Thread.now {
6.65 + Isabelle.jedit_buffers().find(buffer => Isabelle.buffer_name(buffer) == node_name) match {
6.66 + case Some(buffer) =>
6.67 + Isabelle.buffer_lock(buffer) {
6.68 + val text = new Segment
6.69 + buffer.getText(0, buffer.getLength, text)
6.70 + Some(Thy_Header.read(text))
6.71 + }
6.72 + case None => None
6.73 + }
6.74 + } getOrElse {
6.75 + val file = new File(node_name) // FIXME load URL via jEdit VFS (!?)
6.76 + if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
6.77 + Thy_Header.read(file)
6.78 }
6.79 }
6.80 }
6.81
6.82 + val thy_info = new Thy_Info(thy_load)
6.83 +
6.84 + private lazy val delay_load =
6.85 + Swing_Thread.delay_last(Isabelle.session.load_delay)
6.86 + {
6.87 + val buffers = Isabelle.jedit_buffers().toList
6.88 + def loaded_buffer(name: String): Boolean =
6.89 + buffers.exists(buffer => Isabelle.buffer_name(buffer) == name)
6.90 +
6.91 + val thys =
6.92 + for (buffer <- buffers; model <- Isabelle.document_model(buffer))
6.93 + yield (model.master_dir, model.thy_name)
6.94 + val files = thy_info.dependencies(thys).map(_._1).filterNot(loaded_buffer _)
6.95 +
6.96 + val do_load = !files.isEmpty &&
6.97 + {
6.98 + val files_sorted = { val a = files.toArray; Sorting.quickSort(a); a.toList }
6.99 + val files_text = new scala.swing.TextArea(files_sorted.mkString("\n"))
6.100 + files_text.editable = false
6.101 + Library.confirm_dialog(jEdit.getActiveView(),
6.102 + "Auto loading of required files",
6.103 + JOptionPane.YES_NO_OPTION,
6.104 + "The following files are required to resolve theory imports. Reload now?",
6.105 + files_text) == 0
6.106 + }
6.107 + if (do_load)
6.108 + for (file <- files if !loaded_buffer(file))
6.109 + jEdit.openFile(null: View, file)
6.110 + }
6.111 +
6.112
6.113 /* session manager */
6.114
6.115 @@ -387,7 +438,10 @@
6.116 Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
6.117 }
6.118
6.119 - case Session.Ready => Isabelle.jedit_buffers.foreach(Isabelle.init_model)
6.120 + case Session.Ready =>
6.121 + Isabelle.jedit_buffers.foreach(Isabelle.init_model)
6.122 + delay_load()
6.123 +
6.124 case Session.Shutdown => Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
6.125 case _ =>
6.126 }
6.127 @@ -410,17 +464,17 @@
6.128
6.129 case msg: BufferUpdate
6.130 if msg.getWhat == BufferUpdate.LOADED =>
6.131 -
6.132 - val buffer = msg.getBuffer
6.133 - if (buffer != null && Isabelle.session.is_ready)
6.134 - Isabelle.init_model(buffer)
6.135 + if (Isabelle.session.is_ready) {
6.136 + val buffer = msg.getBuffer
6.137 + if (buffer != null) Isabelle.init_model(buffer)
6.138 + delay_load()
6.139 + }
6.140
6.141 case msg: EditPaneUpdate
6.142 if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
6.143 msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
6.144 msg.getWhat == EditPaneUpdate.CREATED ||
6.145 msg.getWhat == EditPaneUpdate.DESTROYED) =>
6.146 -
6.147 val edit_pane = msg.getEditPane
6.148 val buffer = edit_pane.getBuffer
6.149 val text_area = edit_pane.getTextArea
6.150 @@ -448,7 +502,7 @@
6.151 Isabelle.setup_tooltips()
6.152 Isabelle_System.init()
6.153 Isabelle_System.install_fonts()
6.154 - Isabelle.session = new Session(file_store)
6.155 + Isabelle.session = new Session(thy_load)
6.156 SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
6.157 if (ModeProvider.instance.isInstanceOf[ModeProvider])
6.158 ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)