# HG changeset patch # User wenzelm # Date 1751199469 -7200 # Node ID fe8598c92be7b539a52582e76ff323b845b99ab9 # Parent d3f0f72b2c436a2db2f2ef95f9bb66f4329457e0 basic support to reload theory markup from session store; diff -r d3f0f72b2c43 -r fe8598c92be7 src/Pure/Build/build.scala --- a/src/Pure/Build/build.scala Sat Jun 28 17:12:41 2025 +0200 +++ b/src/Pure/Build/build.scala Sun Jun 29 14:17:49 2025 +0200 @@ -707,7 +707,8 @@ def read_theory( theory_context: Export.Theory_Context, - unicode_symbols: Boolean = false + unicode_symbols: Boolean = false, + migrate_file: String => String = identity ): Option[Document.Snapshot] = { def decode(str: String): String = Symbol.output(unicode_symbols, str) @@ -721,19 +722,22 @@ for { id <- theory_context.document_id() - (thy_file, blobs_files) <- theory_context.files(permissive = true) + (thy_file0, blobs_files0) <- theory_context.files(permissive = true) } yield { + val thy_file = migrate_file(thy_file0) + val master_dir = Path.explode(Url.strip_base_name(thy_file).getOrElse( error("Cannot determine theory master directory: " + quote(thy_file)))) val blobs = - blobs_files.map { name => + blobs_files0.map { name0 => + val name = migrate_file(name0) val path = Path.explode(name) val src_path = File.perhaps_relative_path(master_dir, path) - val file = read_source_file(name) + val file = read_source_file(name0) val bytes = file.bytes val text = decode(bytes.text) val chunk = Symbol.Text_Chunk(text) @@ -742,7 +746,7 @@ Document.Blobs.Item(bytes, text, chunk, changed = false) } - val thy_source = decode(read_source_file(thy_file).bytes.text) + val thy_source = decode(read_source_file(thy_file0).bytes.text) val thy_xml = read_xml(Export.MARKUP) val blobs_xml = for (i <- (1 to blobs.length).toList) diff -r d3f0f72b2c43 -r fe8598c92be7 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Sat Jun 28 17:12:41 2025 +0200 +++ b/src/Pure/PIDE/session.scala Sun Jun 29 14:17:49 2025 +0200 @@ -12,6 +12,9 @@ import scala.collection.mutable import scala.annotation.tailrec +import java.util.{Collections, WeakHashMap, Map => JMap} +import java.lang.ref.WeakReference + object Session { /* outlets */ @@ -152,6 +155,28 @@ store, resources.session_background, document_snapshot = document_snapshot) } + private val read_theory_cache = new WeakHashMap[String, WeakReference[Command]] + + def read_theory(name: String): Command = + read_theory_cache.synchronized { + Option(read_theory_cache.get(name)).map(_.get) match { + case Some(command: Command) => command + case _ => + val snapshot = + using(open_session_context()) { session_context => + Build.read_theory(session_context.theory(name), + unicode_symbols = true, + migrate_file = (a: String) => session.resources.append_path("", Path.explode(a))) + } + snapshot.map(_.snippet_commands) match { + case Some(List(command)) => + read_theory_cache.put(name, new WeakReference(command)) + command + case _ => error("Failed to load theory " + quote(name) + " from session database") + } + } + } + /* global flags */ @@ -452,7 +477,7 @@ } } - if (!global_state.value.defined_command(command.id)) { + if (!command.span.is_theory && !global_state.value.defined_command(command.id)) { global_state.change(_.define_command(command)) id_commands += command } diff -r d3f0f72b2c43 -r fe8598c92be7 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Sat Jun 28 17:12:41 2025 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Sun Jun 29 14:17:49 2025 +0200 @@ -76,7 +76,7 @@ val doc_edits = new mutable.ListBuffer[Document.Edit_Command] edits foreach { - case (name, Document.Node.Deps(header)) => + case (name, Document.Node.Deps(header)) if !session_base.loaded_theory(name) => val node = nodes(name) val update_header = node.header.errors.nonEmpty || header.errors.nonEmpty || node.header != header @@ -149,6 +149,33 @@ } + /* reload theory from session store */ + + def reload_theory( + session: Session, + doc_blobs: Document.Blobs, + theory_name: String, + theory_node: Document.Node, + ): Document.Node = { + val command = session.read_theory(theory_name) // FIXME handle errors + + val thy_ok = command.source == theory_node.source + val blobs_changed = + for { + case Exn.Res(blob) <- command.blobs + (digest, _) <- blob.content + doc_blob <- doc_blobs.get(blob.name) + if digest != doc_blob.bytes.sha1_digest + } yield blob.name + + val command1 = + if (thy_ok && blobs_changed.isEmpty) command + else command // FIXME errors as markup + + theory_node.update_commands(Linear_Set(command1)) + } + + /* reparse range of command spans */ @tailrec private def chop_common( @@ -172,6 +199,8 @@ first: Command, last: Command ): Linear_Set[Command] = { + require(!resources.session_base.loaded_theory(node_name)) + val cmds0 = commands.iterator(first, last).toList val blobs_spans0 = syntax.parse_spans(cmds0.iterator.map(_.source).mkString).map(span => @@ -219,6 +248,8 @@ node: Document.Node, edit: Document.Edit_Text ): Document.Node = { + val session_base = resources.session_base + /* recover command spans after edits */ // FIXME somewhat slow def recover_spans( @@ -250,13 +281,17 @@ case (name, Document.Node.Edits(text_edits)) => if (name.is_theory) { val commands1 = edit_text(text_edits, node.commands) - val commands2 = recover_spans(name, node.perspective.visible, commands1) + val commands2 = + if (session_base.loaded_theory(name)) commands1 + else recover_spans(name, node.perspective.visible, commands1) node.update_commands(commands2) } else node case (_, Document.Node.Deps(_)) => node + case (name, Document.Node.Perspective(_, _, _)) if session_base.loaded_theory(name) => node + case (name, Document.Node.Perspective(required, text_perspective, overlays)) => val (visible, visible_overlay) = command_perspective(node, text_perspective, overlays) val perspective: Document.Node.Perspective_Command.T = @@ -336,17 +371,20 @@ val commands = node.commands val node1 = - if (reparse_set(name) && commands.nonEmpty) { + if (!session_base.loaded_theory(name) && reparse_set(name) && commands.nonEmpty) { node.update_commands( reparse_spans(resources, syntax, get_blob, can_import, name, - commands, commands.head, commands.last)) + commands, commands.head, commands.last)) } else node val node2 = edits.foldLeft(node1)( text_edit(resources, syntax, get_blob, can_import, reparse_limit, _, _)) val node3 = - if (reparse_set(name)) { + if (session_base.loaded_theory(name)) { + reload_theory(session, doc_blobs, name.theory, node) + } + else if (reparse_set(name)) { text_edit(resources, syntax, get_blob, can_import, reparse_limit, node2, (name, node2.edit_perspective)) } @@ -356,7 +394,9 @@ doc_edits += (name -> node3.perspective) } - doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node3.commands))) + if (!session_base.loaded_theory(name)) { + doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node3.commands))) + } nodes += (name -> node3) }