src/Pure/System/session.scala
changeset 44163 32e0c150c010
parent 44159 9a35e88d9dc9
child 44182 ecb51b457064
     1.1 --- a/src/Pure/System/session.scala	Fri Aug 12 20:32:25 2011 +0200
     1.2 +++ b/src/Pure/System/session.scala	Fri Aug 12 22:10:49 2011 +0200
     1.3 @@ -20,7 +20,8 @@
     1.4  
     1.5    abstract class File_Store
     1.6    {
     1.7 -    def read(path: Path): String
     1.8 +    def append(master_dir: String, path: Path): String
     1.9 +    def require(file: String): Unit
    1.10    }
    1.11  
    1.12  
    1.13 @@ -186,7 +187,8 @@
    1.14        val syntax = current_syntax()
    1.15        val previous = global_state().history.tip.version
    1.16        val doc_edits =
    1.17 -        (name, Document.Node.Update_Header[Text.Edit](header)) :: edits.map(edit => (name, edit))
    1.18 +        (name, Document.Node.Update_Header[Text.Edit](header.norm_deps(file_store.append))) ::
    1.19 +          edits.map(edit => (name, edit))
    1.20        val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, doc_edits) }
    1.21        val change =
    1.22          global_state.change_yield(_.extend_history(previous, doc_edits, result.map(_._2)))