--- 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)
}
--- 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 =