1.1 --- a/src/Pure/System/session.scala Mon Aug 29 16:38:56 2011 +0200
1.2 +++ b/src/Pure/System/session.scala Mon Aug 29 21:55:49 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,7 +34,7 @@
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 @@ -117,8 +108,6 @@
1.29
1.30 @volatile var verbose: Boolean = false
1.31
1.32 - @volatile private var loaded_theories: Set[String] = Set()
1.33 -
1.34 @volatile private var syntax = new Outer_Syntax
1.35 def current_syntax(): Outer_Syntax = syntax
1.36
1.37 @@ -143,23 +132,6 @@
1.38
1.39 /* theory files */
1.40
1.41 - val thy_load = new Thy_Load
1.42 - {
1.43 - override def is_loaded(name: String): Boolean =
1.44 - loaded_theories.contains(name)
1.45 -
1.46 - override def check_thy(dir: Path, name: String): (String, Thy_Header) =
1.47 - {
1.48 - val file = Isabelle_System.platform_file(dir + Thy_Header.thy_path(name))
1.49 - if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
1.50 - val text = Standard_System.read_file(file)
1.51 - val header = Thy_Header.read(text)
1.52 - (text, header)
1.53 - }
1.54 - }
1.55 -
1.56 - val thy_info = new Thy_Info(thy_load)
1.57 -
1.58 def header_edit(name: String, master_dir: String,
1.59 header: Document.Node_Header): Document.Edit_Text =
1.60 {
1.61 @@ -167,10 +139,10 @@
1.62 {
1.63 val thy_name = Thy_Header.base_name(s)
1.64 if (thy_load.is_loaded(thy_name)) thy_name
1.65 - else file_store.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
1.66 + else thy_load.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
1.67 }
1.68 def norm_use(s: String): String =
1.69 - file_store.append(master_dir, Path.explode(s))
1.70 + thy_load.append(master_dir, Path.explode(s))
1.71
1.72 val header1: Document.Node_Header =
1.73 header match {
1.74 @@ -187,7 +159,6 @@
1.75
1.76 private case class Start(timeout: Time, args: List[String])
1.77 private case object Interrupt
1.78 - private case class Check_Loaded_Files(ask: List[String] => Boolean)
1.79 private case class Init_Node(name: String, master_dir: String,
1.80 header: Document.Node_Header, perspective: Text.Perspective, text: String)
1.81 private case class Edit_Node(name: String, master_dir: String,
1.82 @@ -337,7 +308,7 @@
1.83 catch { case _: Document.State.Fail => bad_result(result) }
1.84 case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
1.85 case List(Keyword.Keyword_Decl(name)) => syntax += name
1.86 - case List(Thy_Info.Loaded_Theory(name)) => loaded_theories += name
1.87 + case List(Thy_Info.Loaded_Theory(name)) => thy_load.register_thy(name)
1.88 case _ => bad_result(result)
1.89 }
1.90 }
1.91 @@ -373,8 +344,6 @@
1.92 case Interrupt if prover.isDefined =>
1.93 prover.get.interrupt
1.94
1.95 - case Check_Loaded_Files(ask) => // FIXME
1.96 -
1.97 case Init_Node(name, master_dir, header, perspective, text) if prover.isDefined =>
1.98 // FIXME compare with existing node
1.99 handle_edits(name, master_dir, header,
1.100 @@ -417,11 +386,6 @@
1.101
1.102 def interrupt() { session_actor ! Interrupt }
1.103
1.104 - def check_loaded_files(ask: List[String] => Boolean)
1.105 - {
1.106 - session_actor ! Check_Loaded_Files(ask)
1.107 - }
1.108 -
1.109 // FIXME simplify signature
1.110 def init_node(name: String, master_dir: String,
1.111 header: Document.Node_Header, perspective: Text.Perspective, text: String)
2.1 --- a/src/Pure/Thy/thy_info.scala Mon Aug 29 16:38:56 2011 +0200
2.2 +++ b/src/Pure/Thy/thy_info.scala Mon Aug 29 21:55:49 2011 +0200
2.3 @@ -38,37 +38,38 @@
2.4
2.5 /* dependencies */
2.6
2.7 - type Deps = Map[String, Exn.Result[(String, Thy_Header)]] // name -> (text, header)
2.8 + type Deps = Map[String, Document.Node_Header]
2.9
2.10 - private def require_thys(ignored: String => Boolean,
2.11 - initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps =
2.12 - (deps /: strs)(require_thy(ignored, initiators, dir, _, _))
2.13 + private def require_thys(initiators: List[String],
2.14 + deps: Deps, thys: List[(String, String)]): Deps =
2.15 + (deps /: thys)(require_thy(initiators, _, _))
2.16
2.17 - private def require_thy(ignored: String => Boolean,
2.18 - initiators: List[String], dir: Path, deps: Deps, str: String): Deps =
2.19 + private def require_thy(initiators: List[String], deps: Deps, thy: (String, String)): Deps =
2.20 {
2.21 + val (dir, str) = thy
2.22 val path = Path.explode(str)
2.23 - val name = path.base.implode
2.24 + val thy_name = path.base.implode
2.25 + val node_name = thy_load.append(dir, Thy_Header.thy_path(path))
2.26
2.27 - if (deps.isDefinedAt(name) || ignored(name)) deps
2.28 + if (deps.isDefinedAt(node_name) || thy_load.is_loaded(thy_name)) deps
2.29 else {
2.30 - val dir1 = dir + path.dir
2.31 + val dir1 = thy_load.append(dir, path.dir)
2.32 try {
2.33 - if (initiators.contains(name)) error(cycle_msg(initiators))
2.34 - val (text, header) =
2.35 - try { thy_load.check_thy(dir1, name) }
2.36 + if (initiators.contains(node_name)) error(cycle_msg(initiators))
2.37 + val header =
2.38 + try { thy_load.check_thy(node_name) }
2.39 catch {
2.40 case ERROR(msg) =>
2.41 - cat_error(msg, "The error(s) above occurred while examining theory " +
2.42 - quote(name) + required_by("\n", initiators))
2.43 + cat_error(msg, "The error(s) above occurred while examining theory file " +
2.44 + quote(node_name) + required_by("\n", initiators))
2.45 }
2.46 - require_thys(ignored, name :: initiators, dir1,
2.47 - deps + (name -> Exn.Res(text, header)), header.imports)
2.48 + val thys = header.imports.map(str => (dir1, str))
2.49 + require_thys(node_name :: initiators, deps + (node_name -> Exn.Res(header)), thys)
2.50 }
2.51 - catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
2.52 + catch { case e: Throwable => deps + (node_name -> Exn.Exn(e)) }
2.53 }
2.54 }
2.55
2.56 - def dependencies(dir: Path, str: String): Deps =
2.57 - require_thy(thy_load.is_loaded, Nil, dir, Map.empty, str)
2.58 + def dependencies(thys: List[(String, String)]): Deps =
2.59 + require_thys(Nil, Map.empty, thys)
2.60 }
3.1 --- a/src/Pure/Thy/thy_load.scala Mon Aug 29 16:38:56 2011 +0200
3.2 +++ b/src/Pure/Thy/thy_load.scala Mon Aug 29 21:55:49 2011 +0200
3.3 @@ -8,8 +8,9 @@
3.4
3.5 abstract class Thy_Load
3.6 {
3.7 - def is_loaded(name: String): Boolean
3.8 -
3.9 - def check_thy(dir: Path, name: String): (String, Thy_Header)
3.10 + def register_thy(thy_name: String)
3.11 + def is_loaded(thy_name: String): Boolean
3.12 + def append(master_dir: String, path: Path): String
3.13 + def check_thy(node_name: String): Thy_Header
3.14 }
3.15
4.1 --- a/src/Tools/jEdit/src/plugin.scala Mon Aug 29 16:38:56 2011 +0200
4.2 +++ b/src/Tools/jEdit/src/plugin.scala Mon Aug 29 21:55:49 2011 +0200
4.3 @@ -13,9 +13,11 @@
4.4 import java.io.{File, FileInputStream, IOException}
4.5 import java.awt.Font
4.6 import javax.swing.JOptionPane
4.7 +import javax.swing.text.Segment
4.8
4.9 import scala.collection.mutable
4.10 import scala.swing.ComboBox
4.11 +import scala.util.Sorting
4.12
4.13 import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
4.14 Buffer, EditPane, MiscUtilities, ServiceManager, View}
4.15 @@ -187,12 +189,10 @@
4.16 def buffer_text(buffer: JEditBuffer): String =
4.17 buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
4.18
4.19 + def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
4.20 +
4.21 def buffer_path(buffer: Buffer): (String, String) =
4.22 - {
4.23 - val master_dir = buffer.getDirectory
4.24 - val path = buffer.getSymlinkPath
4.25 - (master_dir, path)
4.26 - }
4.27 + (buffer.getDirectory, buffer_name(buffer))
4.28
4.29
4.30 /* document model and view */
4.31 @@ -347,10 +347,19 @@
4.32
4.33 class Plugin extends EBPlugin
4.34 {
4.35 - /* editor file store */
4.36 + /* theory files via editor document model */
4.37
4.38 - private val file_store = new Session.File_Store
4.39 + val thy_load = new Thy_Load
4.40 {
4.41 + private var loaded_theories: Set[String] = Set()
4.42 +
4.43 + def register_thy(thy_name: String)
4.44 + {
4.45 + synchronized { loaded_theories += thy_name }
4.46 + }
4.47 + def is_loaded(thy_name: String): Boolean =
4.48 + synchronized { loaded_theories.contains(thy_name) }
4.49 +
4.50 def append(master_dir: String, source_path: Path): String =
4.51 {
4.52 val path = source_path.expand
4.53 @@ -364,37 +373,59 @@
4.54 }
4.55 }
4.56
4.57 - def require(canonical_name: String)
4.58 + def check_thy(node_name: String): Thy_Header =
4.59 {
4.60 - Swing_Thread.later {
4.61 - if (!Isabelle.jedit_buffers().exists(_.getSymlinkPath == canonical_name))
4.62 - jEdit.openFile(null: View, canonical_name)
4.63 + Swing_Thread.now {
4.64 + Isabelle.jedit_buffers().find(buffer => Isabelle.buffer_name(buffer) == node_name) match {
4.65 + case Some(buffer) =>
4.66 + Isabelle.buffer_lock(buffer) {
4.67 + val text = new Segment
4.68 + buffer.getText(0, buffer.getLength, text)
4.69 + Some(Thy_Header.read(text))
4.70 + }
4.71 + case None => None
4.72 + }
4.73 + } getOrElse {
4.74 + val file = new File(node_name) // FIXME load URL via jEdit VFS (!?)
4.75 + if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
4.76 + Thy_Header.read(file)
4.77 }
4.78 }
4.79 }
4.80
4.81 + val thy_info = new Thy_Info(thy_load)
4.82 +
4.83 + private lazy val delay_load =
4.84 + Swing_Thread.delay_last(Isabelle.session.load_delay)
4.85 + {
4.86 + val buffers = Isabelle.jedit_buffers().toList
4.87 + def loaded_buffer(name: String): Boolean =
4.88 + buffers.exists(buffer => Isabelle.buffer_name(buffer) == name)
4.89 +
4.90 + val thys =
4.91 + for (buffer <- buffers; model <- Isabelle.document_model(buffer))
4.92 + yield (model.master_dir, model.thy_name)
4.93 + val files = thy_info.dependencies(thys).map(_._1).filterNot(loaded_buffer _)
4.94 +
4.95 + val do_load = !files.isEmpty &&
4.96 + {
4.97 + val files_sorted = { val a = files.toArray; Sorting.quickSort(a); a.toList }
4.98 + val files_text = new scala.swing.TextArea(files_sorted.mkString("\n"))
4.99 + files_text.editable = false
4.100 + Library.confirm_dialog(jEdit.getActiveView(),
4.101 + "Auto loading of required files",
4.102 + JOptionPane.YES_NO_OPTION,
4.103 + "The following files are required to resolve theory imports. Reload now?",
4.104 + files_text) == 0
4.105 + }
4.106 + if (do_load)
4.107 + for (file <- files if !loaded_buffer(file))
4.108 + jEdit.openFile(null: View, file)
4.109 + }
4.110 +
4.111
4.112 /* session manager */
4.113
4.114 - private lazy val delay_load =
4.115 - Swing_Thread.delay_last(Isabelle.session.load_delay) {
4.116 - def ask(files: List[String]): Boolean = Swing_Thread.now
4.117 - {
4.118 - val file_list = new scala.swing.TextArea(files.mkString("\n"))
4.119 - file_list.editable = false
4.120 - val answer =
4.121 - Library.confirm_dialog(jEdit.getActiveView(),
4.122 - "Auto loading of required files",
4.123 - JOptionPane.YES_NO_OPTION,
4.124 - "The following files are required to resolve theory imports.",
4.125 - "Reload now?",
4.126 - file_list)
4.127 - answer == 0
4.128 - }
4.129 -
4.130 - Isabelle.session.check_loaded_files(ask _)
4.131 - }
4.132 -
4.133 private val session_manager = actor {
4.134 loop {
4.135 react {
4.136 @@ -471,7 +502,7 @@
4.137 Isabelle.setup_tooltips()
4.138 Isabelle_System.init()
4.139 Isabelle_System.install_fonts()
4.140 - Isabelle.session = new Session(file_store)
4.141 + Isabelle.session = new Session(thy_load)
4.142 SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
4.143 if (ModeProvider.instance.isInstanceOf[ModeProvider])
4.144 ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)