src/Pure/PIDE/document.scala
changeset 44163 32e0c150c010
parent 44160 8848867501fb
child 44182 ecb51b457064
     1.1 --- a/src/Pure/PIDE/document.scala	Fri Aug 12 20:32:25 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Fri Aug 12 22:10:49 2011 +0200
     1.3 @@ -52,6 +52,15 @@
     1.4      case class Update_Header[A](header: Header) extends Edit[A]
     1.5  
     1.6      sealed case class Header(val master_dir: String, val thy_header: Exn.Result[Thy_Header])
     1.7 +    {
     1.8 +      def norm_deps(f: (String, Path) => String): Header =
     1.9 +        copy(thy_header =
    1.10 +          thy_header match {
    1.11 +            case Exn.Res(header) =>
    1.12 +              Exn.capture { header.norm_deps(name => f(master_dir, Path.explode(name))) }
    1.13 +            case exn => exn
    1.14 +          })
    1.15 +    }
    1.16      val empty_header = Header("", Exn.Exn(ERROR("Bad theory header")))
    1.17  
    1.18      val empty: Node = Node(empty_header, Map(), Linear_Set())