# HG changeset patch # User wenzelm # Date 1672933455 -3600 # Node ID ca872f20cf5bc4173d88d3cf5ff8c6735763a9d5 # Parent 80ff0ce76b5e851fb6033d7f6ed847a5ed64e3e4 clarified session sources: theory and blobs are read from database, instead of physical file-system; diff -r 80ff0ce76b5e -r ca872f20cf5b src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Thu Jan 05 12:43:05 2023 +0100 +++ b/src/Pure/PIDE/command.scala Thu Jan 05 16:44:15 2023 +0100 @@ -19,8 +19,6 @@ src_path: Path, content: Option[(SHA1.Digest, Symbol.Text_Chunk)] ) { - def read_file: Bytes = Bytes.read(name.path) - def chunk_file: Symbol.Text_Chunk.File = Symbol.Text_Chunk.File(name.node) } @@ -111,6 +109,7 @@ object Markup_Index { val markup: Markup_Index = Markup_Index(false, Symbol.Text_Chunk.Default) def blob(blob: Blob): Markup_Index = Markup_Index(false, blob.chunk_file) + def make(blobs: List[Blob]): List[Markup_Index] = markup :: blobs.map(blob) } sealed case class Markup_Index(status: Boolean, chunk_name: Symbol.Text_Chunk.Name) diff -r 80ff0ce76b5e -r ca872f20cf5b src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Thu Jan 05 12:43:05 2023 +0100 +++ b/src/Pure/PIDE/document.scala Thu Jan 05 16:44:15 2023 +0100 @@ -603,7 +603,7 @@ /* command as add-on snippet */ - def snippet(command: Command): Snapshot = { + def snippet(command: Command, doc_blobs: Blobs): Snapshot = { val node_name = command.node_name val nodes0 = version.nodes @@ -611,7 +611,9 @@ val version1 = Version.make(nodes1) val edits: List[Edit_Text] = - List(node_name -> Node.Edits(List(Text.Edit.insert(0, command.source)))) + List(node_name -> Node.Edits(List(Text.Edit.insert(0, command.source)))) ::: + (for (blob_name <- command.blobs_names; blob <- doc_blobs.get(blob_name)) + yield blob_name -> Node.Blob(blob)) val state0 = state.define_command(command) val state1 = @@ -638,15 +640,9 @@ case Some(command) => for (Exn.Res(blob) <- command.blobs) yield { - val bytes = blob.read_file - val text = bytes.text - val xml = - if (Bytes(text) == bytes) { - val markup = command.init_markups(Command.Markup_Index.blob(blob)) - markup.to_XML(Text.Range.length(text), text, elements) - } - else Nil - blob -> xml + val text = get_node(blob.name).source + val markup = command.init_markups(Command.Markup_Index.blob(blob)) + blob -> markup.to_XML(Text.Range.length(text), text, elements) } } } @@ -1003,17 +999,18 @@ } } - def end_theory(id: Document_ID.Exec): (Snapshot, State) = + def end_theory(id: Document_ID.Exec, document_blobs: Node.Name => Blobs): (Snapshot, State) = theories.get(id) match { case None => fail case Some(st) => val command = st.command val node_name = command.node_name + val doc_blobs = document_blobs(node_name) val command1 = Command.unparsed(command.source, theory = true, id = id, node_name = node_name, blobs_info = command.blobs_info, results = st.results, markups = st.markups) val state1 = copy(theories = theories - id) - (state1.snippet(command1), state1) + (state1.snippet(command1, doc_blobs), state1) } def assign( @@ -1250,7 +1247,7 @@ new Snapshot(this, version, node_name, pending_edits1, snippet_command) } - def snippet(command: Command): Snapshot = - snapshot().snippet(command) + def snippet(command: Command, doc_blobs: Blobs): Snapshot = + snapshot().snippet(command, doc_blobs) } } diff -r 80ff0ce76b5e -r ca872f20cf5b src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Thu Jan 05 12:43:05 2023 +0100 +++ b/src/Pure/PIDE/session.scala Thu Jan 05 16:44:15 2023 +0100 @@ -125,8 +125,8 @@ val cache: Term.Cache = Term.Cache.make() - def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = - Command.Blobs_Info.none + def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = Command.Blobs_Info.none + def build_blobs(name: Document.Node.Name): Document.Blobs = Document.Blobs.empty /* global flags */ @@ -560,7 +560,7 @@ case Markup.Process_Result(result) if output.is_exit => if (prover.defined) protocol_handlers.exit() for (id <- global_state.value.theories.keys) { - val snapshot = global_state.change_result(_.end_theory(id)) + val snapshot = global_state.change_result(_.end_theory(id, build_blobs)) finished_theories.post(snapshot) } file_formats.stop_session() diff -r 80ff0ce76b5e -r ca872f20cf5b src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Thu Jan 05 12:43:05 2023 +0100 +++ b/src/Pure/Tools/build_job.scala Thu Jan 05 16:44:15 2023 +0100 @@ -25,6 +25,9 @@ Symbol.output(unicode_symbols, UTF8.decode_permissive(read(name).bytes)), cache = theory_context.cache) + def read_source_file(name: String): Sessions.Source_File = + theory_context.session_context.source_file(name) + for { id <- theory_context.document_id() (thy_file, blobs_files) <- theory_context.files(permissive = true) @@ -35,31 +38,26 @@ error("Cannot determine theory master directory: " + quote(thy_file)))) val blobs = - blobs_files.map { file => - val name = Document.Node.Name(file) - val path = Path.explode(file) + blobs_files.map { name => + val path = Path.explode(name) val src_path = File.relative_path(master_dir, path).getOrElse(path) - Command.Blob(name, src_path, None) + + val file = read_source_file(name) + val bytes = file.bytes + val text = bytes.text + val chunk = Symbol.Text_Chunk(text) + + Command.Blob(Document.Node.Name(name), src_path, Some((file.digest, chunk))) -> + Document.Blobs.Item(bytes, text, chunk, changed = false) } + + val thy_source = read_source_file(thy_file).text + val thy_xml = read_xml(Export.MARKUP) val blobs_xml = for (i <- (1 to blobs.length).toList) yield read_xml(Export.MARKUP + i) - val blobs_info = - Command.Blobs_Info( - for { (Command.Blob(name, src_path, _), xml) <- blobs zip blobs_xml } - yield { - val text = XML.content(xml) - val chunk = Symbol.Text_Chunk(text) - val digest = SHA1.digest(Symbol.encode(text)) - Exn.Res(Command.Blob(name, src_path, Some((digest, chunk)))) - }) - - val thy_xml = read_xml(Export.MARKUP) - val thy_source = XML.content(thy_xml) - - val markups_index = - Command.Markup_Index.markup :: blobs.map(Command.Markup_Index.blob) + val markups_index = Command.Markup_Index.make(blobs.map(_._1)) val markups = Command.Markups.make( for ((index, xml) <- markups_index.zip(thy_xml :: blobs_xml)) @@ -73,9 +71,12 @@ val command = Command.unparsed(thy_source, theory = true, id = id, node_name = Document.Node.Name(thy_file, theory = theory_context.theory), - blobs_info = blobs_info, markups = markups, results = results) + blobs_info = Command.Blobs_Info(for ((a, _) <- blobs) yield Exn.Res(a)), + markups = markups, results = results) - Document.State.init.snippet(command) + val doc_blobs = Document.Blobs((for ((a, b) <- blobs.iterator) yield a.name -> b).toMap) + + Document.State.init.snippet(command, doc_blobs) } } @@ -269,32 +270,44 @@ } else Nil + def session_blobs(node_name: Document.Node.Name): List[(Command.Blob, Document.Blobs.Item)] = + session_background.base.theory_load_commands.get(node_name.theory) match { + case None => Nil + case Some(spans) => + val syntax = session_background.base.theory_syntax(node_name) + val master_dir = Path.explode(node_name.master_dir) + for (span <- spans; file <- span.loaded_files(syntax).files) + yield { + val src_path = Path.explode(file) + val blob_name = Document.Node.Name(File.symbolic_path(master_dir + src_path)) + + val bytes = session_sources(blob_name.node).bytes + val text = bytes.text + val chunk = Symbol.Text_Chunk(text) + + Command.Blob(blob_name, src_path, Some((SHA1.digest(bytes), chunk))) -> + Document.Blobs.Item(bytes, text, chunk, changed = false) + } + } + val resources = new Resources(session_background, log = log, command_timings = command_timings0) + val session = new Session(options, resources) { override val cache: Term.Cache = store.cache - override def build_blobs_info(node_name: Document.Node.Name): Command.Blobs_Info = { - session_background.base.theory_load_commands.get(node_name.theory) match { - case Some(spans) => - val syntax = session_background.base.theory_syntax(node_name) - val blobs = - for (span <- spans; file <- span.loaded_files(syntax).files) - yield { - (Exn.capture { - val master_dir = Path.explode(node_name.master_dir) - val src_path = Path.explode(file) - val node = File.symbolic_path(master_dir + src_path) - val bytes = session_sources(node).bytes - val content = (SHA1.digest(bytes), Symbol.Text_Chunk(bytes.text)) - Command.Blob(Document.Node.Name(node), src_path, Some(content)) - }).user_error - } - Command.Blobs_Info(blobs) - case None => Command.Blobs_Info.none + override def build_blobs_info(node_name: Document.Node.Name): Command.Blobs_Info = + session_blobs(node_name) match { + case Nil => Command.Blobs_Info.none + case blobs => Command.Blobs_Info(for ((a, _) <- blobs) yield Exn.Res(a)) } - } + + override def build_blobs(node_name: Document.Node.Name): Document.Blobs = + session_blobs(node_name) match { + case Nil => Document.Blobs.empty + case blobs => Document.Blobs((for ((a, b) <- blobs.iterator) yield a.name -> b).toMap) + } } object Build_Session_Errors { diff -r 80ff0ce76b5e -r ca872f20cf5b src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Thu Jan 05 12:43:05 2023 +0100 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Thu Jan 05 16:44:15 2023 +0100 @@ -31,7 +31,7 @@ results: Command.Results = Command.Results.empty ): (String, JEdit_Rendering) = { val command = Command.rich_text(Document_ID.make(), results, formatted_body) - val snippet = snapshot.snippet(command) + val snippet = snapshot.snippet(command, Document.Blobs.empty) val model = File_Model.init(PIDE.session) val rendering = apply(snippet, model, PIDE.options.value) (command.source, rendering)