# HG changeset patch
# User wenzelm
# Date 1313244268 -7200
# Node ID 1de22a7b2a82de15a45e88826cb153124a139714
# Parent  ecb51b4570640af650088152366314ff1091b4c6
tuned signature;

diff -r ecb51b457064 -r 1de22a7b2a82 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Aug 13 15:59:26 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Sat Aug 13 16:04:28 2011 +0200
@@ -53,9 +53,9 @@
     case class Edits[A](edits: List[A]) extends Edit[A]
     case class Header[A](header: Node_Header) extends Edit[A]
 
-    def norm_header[A](f: Path => String, header: Node_Header): Header[A] =
+    def norm_header[A](f: String => String, header: Node_Header): Header[A] =
       header match {
-        case Exn.Res(h) => Header[A](Exn.capture { h.norm_deps(name => f(Path.explode(name))) })
+        case Exn.Res(h) => Header[A](Exn.capture { h.norm_deps(f) })
         case exn => Header[A](exn)
       }
 
diff -r ecb51b457064 -r 1de22a7b2a82 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sat Aug 13 15:59:26 2011 +0200
+++ b/src/Pure/System/session.scala	Sat Aug 13 16:04:28 2011 +0200
@@ -189,7 +189,8 @@
       val syntax = current_syntax()
       val previous = global_state().history.tip.version
       val norm_header =
-        Document.Node.norm_header[Text.Edit](file_store.append(master_dir, _), header)
+        Document.Node.norm_header[Text.Edit](
+          name => file_store.append(master_dir, Path.explode(name)), header)
       val doc_edits = (name, norm_header) :: edits.map(edit => (name, edit))
       val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, doc_edits) }
       val change =