--- a/src/Pure/PIDE/document.scala Fri Aug 12 12:03:17 2011 +0200
+++ b/src/Pure/PIDE/document.scala Fri Aug 12 15:28:30 2011 +0200
@@ -51,8 +51,8 @@
case class Edits[A](edits: List[A]) extends Edit[A]
case class Update_Header[A](header: Header) extends Edit[A]
- sealed case class Header(val master_dir: Path, val thy_header: Exn.Result[Thy_Header])
- val empty_header = Header(Path.current, Exn.Exn(ERROR("Bad theory header")))
+ sealed case class Header(val master_dir: String, val thy_header: Exn.Result[Thy_Header])
+ val empty_header = Header("", Exn.Exn(ERROR("Bad theory header")))
val empty: Node = Node(empty_header, Map(), Linear_Set())