# HG changeset patch # User wenzelm # Date 1483890473 -3600 # Node ID fd1efd6dd385f839120b202e260d56a426ea65f4 # Parent 0a7179ad430de15bea8c23a34bba206d8a3f0e21 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model; diff -r 0a7179ad430d -r fd1efd6dd385 src/Pure/PIDE/resources.scala --- 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 */ diff -r 0a7179ad430d -r fd1efd6dd385 src/Tools/jEdit/etc/options --- 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" diff -r 0a7179ad430d -r fd1efd6dd385 src/Tools/jEdit/src/document_model.scala --- 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] = diff -r 0a7179ad430d -r fd1efd6dd385 src/Tools/jEdit/src/jedit_editor.scala --- 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 diff -r 0a7179ad430d -r fd1efd6dd385 src/Tools/jEdit/src/jedit_resources.scala --- 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 */ diff -r 0a7179ad430d -r fd1efd6dd385 src/Tools/jEdit/src/plugin.scala --- 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) } } }