--- a/src/Pure/PIDE/document.scala Tue Aug 16 12:06:49 2011 +0200
+++ b/src/Pure/PIDE/document.scala Tue Aug 16 21:13:52 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: String => String, header: Node_Header): Header[A] =
+ def norm_header[A](f: String => String, g: String => String, header: Node_Header): Header[A] =
header match {
- case Exn.Res(h) => Header[A](Exn.capture { h.norm_deps(f) })
+ case Exn.Res(h) => Header[A](Exn.capture { h.norm_deps(f, g) })
case exn => Header[A](exn)
}