--- a/src/Pure/PIDE/resources.scala Sun Jan 08 14:46:04 2017 +0100
+++ b/src/Pure/PIDE/resources.scala Sun Jan 08 16:47:53 2017 +0100
@@ -145,13 +145,6 @@
start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header =
with_thy_reader(name, check_thy_reader(qualifier, name, _, start, strict))
- def check_file(file: String): Boolean =
- try {
- if (Url.is_wellformed(file)) Url.is_readable(file)
- else (new JFile(file)).isFile
- }
- catch { case ERROR(_) => false }
-
/* special header */
--- a/src/Tools/jEdit/etc/options Sun Jan 08 14:46:04 2017 +0100
+++ b/src/Tools/jEdit/etc/options Sun Jan 08 16:47:53 2017 +0100
@@ -6,11 +6,8 @@
public option jedit_print_mode : string = ""
-- "default print modes for output, separated by commas (change requires restart)"
-public option jedit_auto_load : bool = false
- -- "load all required files automatically to resolve theory imports"
-
public option jedit_auto_resolve : bool = false
- -- "automatically resolve auxiliary files within the editor"
+ -- "automatically resolve auxiliary files within the document model"
public option jedit_reset_font_size : int = 18
-- "reset main text font size"
--- a/src/Tools/jEdit/src/document_model.scala Sun Jan 08 14:46:04 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Sun Jan 08 16:47:53 2017 +0100
@@ -64,18 +64,21 @@
buffer_models = buffer_models - buffer)
}
}
+
+ def provide_file(session: Session, node_name: Document.Node.Name, text: String): State =
+ if (models.isDefinedAt(node_name)) this
+ else {
+ val edit = Text.Edit.insert(0, text)
+ val model = File_Model(session, node_name, File_Content(text), pending_edits = List(edit))
+ copy(models = models + (node_name -> model))
+ }
}
private val state = Synchronized(State()) // owned by GUI thread
- def get(name: Document.Node.Name): Option[Document_Model] =
- state.value.models.get(name)
-
- def get(buffer: JEditBuffer): Option[Buffer_Model] =
- state.value.buffer_models.get(buffer)
-
- def is_stable(): Boolean =
- state.value.models_iterator.forall(_.is_stable)
+ def get_models(): Map[Document.Node.Name, Document_Model] = state.value.models
+ def get(name: Document.Node.Name): Option[Document_Model] = get_models.get(name)
+ def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer)
def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
for {
@@ -113,6 +116,13 @@
else st)
}
+ def provide_files(session: Session, files: List[(Document.Node.Name, String)])
+ {
+ GUI_Thread.require {}
+ state.change(st =>
+ (st /: files) { case (st1, (node_name, text)) => st1.provide_file(session, node_name, text) })
+ }
+
/* required nodes */
@@ -191,7 +201,7 @@
sealed case class File_Content(text: String)
{
- lazy val bytes: Bytes = Bytes(text)
+ lazy val bytes: Bytes = Bytes(Symbol.encode(text))
lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
lazy val bibtex_entries: List[Text.Info[String]] =
try { Bibtex.document_entries(text) }
@@ -341,7 +351,7 @@
_blob match {
case Some(x) => x
case None =>
- val bytes = PIDE.resources.file_content(buffer)
+ val bytes = PIDE.resources.make_file_content(buffer)
val chunk = Symbol.Text_Chunk(buffer.getSegment(0, buffer.getLength))
_blob = Some((bytes, chunk))
(bytes, chunk)
@@ -418,7 +428,7 @@
}
}
- def is_stable(): Boolean = !pending_edits.nonEmpty
+ def is_stable: Boolean = !pending_edits.nonEmpty
def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.get_edits)
def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
--- a/src/Tools/jEdit/src/jedit_editor.scala Sun Jan 08 14:46:04 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Sun Jan 08 16:47:53 2017 +0100
@@ -37,13 +37,6 @@
def invoke(): Unit = delay1_flush.invoke()
def invoke_generated(): Unit = { delay1_flush.invoke(); delay2_flush.invoke() }
- def stable_tip_version(): Option[Document.Version] =
- GUI_Thread.require {
- if (Document_Model.is_stable())
- session.current_state().stable_tip_version
- else None
- }
-
def visible_node(name: Document.Node.Name): Boolean =
JEdit_Lib.jedit_buffer(name) match {
case Some(buffer) => JEdit_Lib.jedit_text_areas(buffer).nonEmpty
--- a/src/Tools/jEdit/src/jedit_resources.scala Sun Jan 08 14:46:04 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Sun Jan 08 16:47:53 2017 +0100
@@ -67,6 +67,18 @@
/* file content */
+ def read_file_content(node_name: Document.Node.Name): Option[String] =
+ {
+ val name = node_name.node
+ try {
+ val text =
+ if (Url.is_wellformed(name)) Url.read(Url(name))
+ else File.read(new JFile(name))
+ Some(Symbol.decode(Line.normalize(text)))
+ }
+ catch { case ERROR(_) => None }
+ }
+
override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
{
GUI_Thread.now {
@@ -104,7 +116,7 @@
}
}
- def file_content(buffer: Buffer): Bytes = (new File_Content(buffer)).content()
+ def make_file_content(buffer: Buffer): Bytes = (new File_Content(buffer)).content()
/* theory text edits */
--- a/src/Tools/jEdit/src/plugin.scala Sun Jan 08 14:46:04 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Sun Jan 08 16:47:53 2017 +0100
@@ -180,65 +180,56 @@
if (Isabelle.continuous_checking && delay_load_activated() &&
PerspectiveManager.isPerspectiveEnabled)
{
- try {
- val view = jEdit.getActiveView()
-
- val buffers = JEdit_Lib.jedit_buffers().toList
- if (buffers.forall(_.isLoaded)) {
- def loaded_buffer(name: String): Boolean =
- buffers.exists(buffer => JEdit_Lib.buffer_name(buffer) == name)
+ if (JEdit_Lib.jedit_buffers().exists(_.isLoading)) delay_load.invoke()
+ else {
+ val required_files =
+ {
+ val models = Document_Model.get_models()
val thys =
- for {
- buffer <- buffers
- model <- Document_Model.get(buffer)
- if model.is_theory
- } yield (model.node_name, Position.none)
+ (for ((node_name, model) <- models.iterator if model.is_theory)
+ yield (node_name, Position.none)).toList
val thy_info = new Thy_Info(PIDE.resources)
- val thy_files = thy_info.dependencies("", thys).deps.map(_.name.node)
+ val thy_files: List[Document.Node.Name] = thy_info.dependencies("", thys).deps.map(_.name)
- val aux_files =
+ val aux_files: List[Document.Node.Name] =
if (PIDE.options.bool("jedit_auto_resolve")) {
- PIDE.editor.stable_tip_version() match {
- case Some(version) => PIDE.resources.undefined_blobs(version.nodes).map(_.node)
+ val stable_tip_version =
+ if (models.forall(p => p._2.is_stable))
+ PIDE.session.current_state().stable_tip_version
+ else None
+ stable_tip_version match {
+ case Some(version) => PIDE.resources.undefined_blobs(version.nodes)
case None => delay_load.invoke(); Nil
}
}
else Nil
- val files =
- (thy_files ::: aux_files).filter(file =>
- !loaded_buffer(file) && PIDE.resources.check_file(file))
-
- if (files.nonEmpty) {
- if (PIDE.options.bool("jedit_auto_load")) {
- files.foreach(file => jEdit.openFile(null: View, file))
- }
- else {
- val files_list = new ListView(files.sorted)
- for (i <- 0 until files.length)
- files_list.selection.indices += i
+ (thy_files ::: aux_files).filterNot(models.isDefinedAt(_))
+ }
+ if (required_files.nonEmpty) {
+ try {
+ Standard_Thread.fork("resolve_dependencies") {
+ val loaded_files =
+ for {
+ name <- required_files
+ text <- PIDE.resources.read_file_content(name)
+ } yield (name, text)
- val answer =
- GUI.confirm_dialog(view,
- "Auto loading of required files",
- JOptionPane.YES_NO_OPTION,
- "The following files are required to resolve theory imports.",
- "Reload selected files now?",
- new ScrollPane(files_list),
- new Isabelle.Continuous_Checking)
- if (answer == 0) {
- files.foreach(file =>
- if (files_list.selection.items.contains(file))
- jEdit.openFile(null: View, file))
+ GUI_Thread.later {
+ try {
+ Document_Model.provide_files(PIDE.session, loaded_files)
+ delay_init.invoke()
+ }
+ finally { delay_load_active.change(_ => false) }
}
}
}
+ catch { case _: Throwable => delay_load_active.change(_ => false) }
}
- else delay_load.invoke()
+ else delay_load_active.change(_ => false)
}
- finally { delay_load_active.change(_ => false) }
}
}