# HG changeset patch # User wenzelm # Date 1546291262 -3600 # Node ID 636b3c03a61af6bd04a1b70cd8c81ffec7f92475 # Parent f71eb0cf8da72687ec0873acf1914dc2c6069f88 include loaded_files as doc_blobs (without purging); diff -r f71eb0cf8da7 -r 636b3c03a61a src/Pure/PIDE/headless.scala --- a/src/Pure/PIDE/headless.scala Mon Dec 31 21:12:22 2018 +0100 +++ b/src/Pure/PIDE/headless.scala Mon Dec 31 22:21:02 2018 +0100 @@ -10,6 +10,7 @@ import java.io.{File => JFile} import scala.annotation.tailrec +import scala.collection.mutable object Headless @@ -161,13 +162,17 @@ commit_cleanup_delay: Time = default_commit_cleanup_delay, progress: Progress = No_Progress): Use_Theories_Result = { - val dep_theories = + val dependencies = { val import_names = theories.map(thy => resources.import_name(qualifier, master_directory(master_dir), thy) -> Position.none) - resources.dependencies(import_names, progress = progress).check_errors.theories + resources.dependencies(import_names, progress = progress).check_errors } + val dep_theories = dependencies.theories + val dep_files = + dependencies.loaded_files(false).flatMap(_._2). + map(path => Document.Node.Name(resources.append("", path))) val use_theories_state = Synchronized(Use_Theories_State()) @@ -258,7 +263,7 @@ try { session.commands_changed += consumer - resources.load_theories(session, id, dep_theories, progress) + resources.load_theories(session, id, dep_theories, dep_files, progress) use_theories_state.value.await_result check_progress.cancel } @@ -341,9 +346,51 @@ } sealed case class State( - required: Multi_Map[Document.Node.Name, UUID.T] = Multi_Map.empty, - theories: Map[Document.Node.Name, Theory] = Map.empty) + blobs: Map[Document.Node.Name, Document.Blob] = Map.empty, + theories: Map[Document.Node.Name, Theory] = Map.empty, + required: Multi_Map[Document.Node.Name, UUID.T] = Multi_Map.empty) { + /* blobs */ + + def doc_blobs: Document.Blobs = Document.Blobs(blobs) + + def update_blobs(names: List[Document.Node.Name]): (Document.Blobs, State) = + { + val new_blobs = + names.flatMap(name => + { + val bytes = Bytes.read(name.path) + def new_blob: Document.Blob = + { + val text = bytes.text + Document.Blob(bytes, text, Symbol.Text_Chunk(text), changed = true) + } + blobs.get(name) match { + case Some(blob) => if (blob.bytes == bytes) None else Some(name -> new_blob) + case None => Some(name -> new_blob) + } + }) + val blobs1 = (blobs /: new_blobs)(_ + _) + val blobs2 = (blobs /: new_blobs)({ case (map, (a, b)) => map + (a -> b.unchanged) }) + (Document.Blobs(blobs1), copy(blobs = blobs2)) + } + + def blob_edits(name: Document.Node.Name, old_blob: Option[Document.Blob]) + : List[Document.Edit_Text] = + { + val blob = blobs.getOrElse(name, error("Missing blob " + quote(name.toString))) + val text_edits = + old_blob match { + case None => List(Text.Edit.insert(0, blob.source)) + case Some(blob0) => Text.Edit.replace(0, blob0.source, blob.source) + } + if (text_edits.isEmpty) Nil + else List(name -> Document.Node.Blob(blob), name -> Document.Node.Edits(text_edits)) + } + + + /* theories */ + lazy val theory_graph: Graph[Document.Node.Name, Unit] = { val entries = @@ -389,7 +436,7 @@ val edits = theory1.node_edits(Some(theory)) (edits, (node_name, theory1)) } - session.update(Document.Blobs.empty, theory_edits.flatMap(_._1)) + session.update(doc_blobs, theory_edits.flatMap(_._1)) st1.update_theories(theory_edits.map(_._2)) } @@ -403,7 +450,7 @@ val (retained, purged) = all_nodes.partition(retain) val purge_edits = purged.flatMap(name => theories(name).purge_edits) - session.update(Document.Blobs.empty, purge_edits) + session.update(doc_blobs, purge_edits) ((purged, retained), remove_theories(purged)) } @@ -475,6 +522,7 @@ session: Session, id: UUID.T, dep_theories: List[Document.Node.Name], + dep_files: List[Document.Node.Name], progress: Progress) { val loaded_theories = @@ -494,7 +542,7 @@ state.change(st => { - val st1 = st.insert_required(id, dep_theories) + val (doc_blobs1, st1) = st.insert_required(id, dep_theories).update_blobs(dep_files) val theory_edits = for (theory <- loaded_theories) yield { @@ -503,7 +551,11 @@ val edits = theory1.node_edits(st1.theories.get(node_name)) (edits, (node_name, theory1)) } - session.update(Document.Blobs.empty, theory_edits.flatMap(_._1)) + val file_edits = + for { node_name <- dep_files if doc_blobs1.changed(node_name) } + yield st1.blob_edits(node_name, st.blobs.get(node_name)) + + session.update(doc_blobs1, theory_edits.flatMap(_._1) ::: file_edits.flatten) st1.update_theories(theory_edits.map(_._2)) }) }