src/Pure/PIDE/document.scala
changeset 44182 ecb51b457064
parent 44163 32e0c150c010
child 44183 1de22a7b2a82
     1.1 --- a/src/Pure/PIDE/document.scala	Sat Aug 13 13:48:26 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Sat Aug 13 15:59:26 2011 +0200
     1.3 @@ -36,6 +36,8 @@
     1.4    type Edit_Command = Edit[(Option[Command], Option[Command])]
     1.5    type Edit_Command_ID = Edit[(Option[Command_ID], Option[Command_ID])]
     1.6  
     1.7 +  type Node_Header = Exn.Result[Thy_Header]
     1.8 +
     1.9    object Node
    1.10    {
    1.11      sealed abstract class Edit[A]
    1.12 @@ -44,26 +46,20 @@
    1.13          this match {
    1.14            case Remove() => Remove()
    1.15            case Edits(es) => Edits(es.map(f))
    1.16 -          case Update_Header(header: Header) => Update_Header(header)
    1.17 +          case Header(header) => Header(header)
    1.18          }
    1.19      }
    1.20      case class Remove[A]() extends Edit[A]
    1.21      case class Edits[A](edits: List[A]) extends Edit[A]
    1.22 -    case class Update_Header[A](header: Header) extends Edit[A]
    1.23 +    case class Header[A](header: Node_Header) extends Edit[A]
    1.24  
    1.25 -    sealed case class Header(val master_dir: String, val thy_header: Exn.Result[Thy_Header])
    1.26 -    {
    1.27 -      def norm_deps(f: (String, Path) => String): Header =
    1.28 -        copy(thy_header =
    1.29 -          thy_header match {
    1.30 -            case Exn.Res(header) =>
    1.31 -              Exn.capture { header.norm_deps(name => f(master_dir, Path.explode(name))) }
    1.32 -            case exn => exn
    1.33 -          })
    1.34 -    }
    1.35 -    val empty_header = Header("", Exn.Exn(ERROR("Bad theory header")))
    1.36 +    def norm_header[A](f: Path => String, header: Node_Header): Header[A] =
    1.37 +      header match {
    1.38 +        case Exn.Res(h) => Header[A](Exn.capture { h.norm_deps(name => f(Path.explode(name))) })
    1.39 +        case exn => Header[A](exn)
    1.40 +      }
    1.41  
    1.42 -    val empty: Node = Node(empty_header, Map(), Linear_Set())
    1.43 +    val empty: Node = Node(Exn.Exn(ERROR("Bad theory header")), Map(), Linear_Set())
    1.44  
    1.45      def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
    1.46        : Iterator[(Command, Text.Offset)] =
    1.47 @@ -80,7 +76,7 @@
    1.48    private val block_size = 1024
    1.49  
    1.50    sealed case class Node(
    1.51 -    val header: Node.Header,
    1.52 +    val header: Node_Header,
    1.53      val blobs: Map[String, Blob],
    1.54      val commands: Linear_Set[Command])
    1.55    {