src/Pure/PIDE/headless.scala

 
 
 import java.io.{File => JFile}
 
 import scala.annotation.tailrec
+import scala.collection.mutable
 
 
 object Headless
 {
   /** session **/

       // commit: must not block, must not fail
       commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None,
       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())
 
       def check_result(beyond_limit: Boolean = false)
       {

         }
       }
 
       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
       }
       finally {
         session.commands_changed -= consumer

         if (required == node_required) this
         else new Theory(node_name, node_header, text, required)
     }
 
     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 =
           for ((name, theory) <- theories.toList)
           yield ((name, ()), theory.node_header.imports.map(_._1).filter(theories.isDefinedAt(_)))

           yield {
             val theory1 = theory.required(st1.is_required(node_name))
             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))
       }
 
       def purge_theories(session: Session, nodes: List[Document.Node.Name])
         : ((List[Document.Node.Name], List[Document.Node.Name]), State) =

 
         val retain = theory_graph.all_preds(all_nodes.filterNot(purge)).toSet
         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))
       }
 
       def frontier_theories(clean: Set[Document.Node.Name]): Set[Document.Node.Name] =

 
     def load_theories(
       session: Session,
       id: UUID.T,
       dep_theories: List[Document.Node.Name],
+      dep_files: List[Document.Node.Name],
       progress: Progress)
     {
       val loaded_theories =
         for (node_name <- dep_theories)
         yield {

       val loaded = loaded_theories.length
       if (loaded > 1) progress.echo("Loading " + loaded + " theories ...")
 
       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 {
               val node_name = theory.node_name
               val theory1 = theory.required(st1.is_required(node_name))
               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))
         })
     }
 
     def unload_theories(session: Session, id: UUID.T, dep_theories: List[Document.Node.Name])