src/Pure/System/session.scala

--- a/src/Pure/System/session.scala	Fri Aug 12 20:32:25 2011 +0200
+++ b/src/Pure/System/session.scala	Fri Aug 12 22:10:49 2011 +0200
@@ -20,7 +20,8 @@
 
   abstract class File_Store
   {
-    def read(path: Path): String
+    def append(master_dir: String, path: Path): String
+    def require(file: String): Unit
   }
 
 
@@ -186,7 +187,8 @@
       val syntax = current_syntax()
       val previous = global_state().history.tip.version
       val doc_edits =
-        (name, Document.Node.Update_Header[Text.Edit](header)) :: edits.map(edit => (name, edit))
+        (name, Document.Node.Update_Header[Text.Edit](header.norm_deps(file_store.append))) ::
+          edits.map(edit => (name, edit))
       val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, doc_edits) }
       val change =
         global_state.change_yield(_.extend_history(previous, doc_edits, result.map(_._2)))