--- a/src/Pure/PIDE/document.scala Thu Aug 11 18:01:28 2011 +0200
+++ b/src/Pure/PIDE/document.scala Thu Aug 11 20:32:44 2011 +0200
@@ -44,10 +44,12 @@
this match {
case Remove() => Remove()
case Edits(es) => Edits(es.map(f))
+ case Update_Header(header: Header) => Update_Header(header)
}
}
case class Remove[A]() extends Edit[A]
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.Header])
val empty_header = Header(Path.current, Exn.Exn(ERROR("Bad theory header")))