simplified Document.Node.Header -- internalized errors;
authorwenzelm
Tue Aug 07 15:01:48 2012 +0200 (2012-08-07)
changeset 48707ba531af91148
parent 48706 e2b512024eab
child 48708 189ece4b4ff1
simplified Document.Node.Header -- internalized errors;
src/Pure/Isar/outer_syntax.scala
src/Pure/PIDE/document.ML
src/Pure/PIDE/document.scala
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/System/build.scala
src/Pure/System/session.scala
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_info.scala
src/Pure/Thy/thy_load.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/document_model.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Aug 07 13:21:29 2012 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 07 15:01:48 2012 +0200
     1.3 @@ -60,14 +60,10 @@
     1.4    def + (name: String, kind: String): Outer_Syntax = this + (name, kind, name)
     1.5    def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
     1.6  
     1.7 -  def add_keywords(header: Document.Node_Header): Outer_Syntax =
     1.8 -    header match {
     1.9 -      case Exn.Res(deps) =>
    1.10 -        (this /: deps.keywords) {
    1.11 -          case (syntax, ((name, Some((kind, _))))) => syntax + (name, kind)
    1.12 -          case (syntax, ((name, None))) => syntax + name
    1.13 -        }
    1.14 -      case Exn.Exn(_) => this
    1.15 +  def add_keywords(header: Document.Node.Header): Outer_Syntax =
    1.16 +    (this /: header.keywords) {
    1.17 +      case (syntax, ((name, Some((kind, _))))) => syntax + (name, kind)
    1.18 +      case (syntax, ((name, None))) => syntax + name
    1.19      }
    1.20  
    1.21    def is_command(name: String): Boolean =
     2.1 --- a/src/Pure/PIDE/document.ML	Tue Aug 07 13:21:29 2012 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Tue Aug 07 15:01:48 2012 +0200
     2.3 @@ -15,11 +15,11 @@
     2.4    val new_id: unit -> id
     2.5    val parse_id: string -> id
     2.6    val print_id: id -> string
     2.7 -  type node_header = (string * Thy_Header.header) Exn.result
     2.8 +  type node_header = string * Thy_Header.header * string list
     2.9    datatype node_edit =
    2.10      Clear |
    2.11      Edits of (command_id option * command_id option) list |
    2.12 -    Header of node_header |
    2.13 +    Deps of node_header |
    2.14      Perspective of command_id list
    2.15    type edit = string * node_edit
    2.16    type state
    2.17 @@ -59,7 +59,7 @@
    2.18  
    2.19  (** document structure **)
    2.20  
    2.21 -type node_header = (string * Thy_Header.header) Exn.result;
    2.22 +type node_header = string * Thy_Header.header * string list;
    2.23  type perspective = (command_id -> bool) * command_id option;
    2.24  structure Entries = Linear_Set(type key = command_id val ord = int_ord);
    2.25  
    2.26 @@ -67,7 +67,7 @@
    2.27  val no_exec = Command.memo_value (Toplevel.toplevel, Lazy.value ());
    2.28  
    2.29  abstype node = Node of
    2.30 - {header: node_header,
    2.31 + {header: node_header,  (*master directory, theory header, errors*)
    2.32    perspective: perspective,  (*visible commands, last*)
    2.33    entries: (exec_id * exec) option Entries.T,  (*command entries with excecutions*)
    2.34    result: exec option}  (*result of last execution*)
    2.35 @@ -83,7 +83,7 @@
    2.36  fun make_perspective command_ids : perspective =
    2.37    (Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids);
    2.38  
    2.39 -val no_header = Exn.Exn (ERROR "Bad theory header");
    2.40 +val no_header = ("", Thy_Header.make "" [] [] [], ["Bad theory header"]);
    2.41  val no_perspective = make_perspective [];
    2.42  
    2.43  val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
    2.44 @@ -92,7 +92,10 @@
    2.45  
    2.46  (* basic components *)
    2.47  
    2.48 -fun get_header (Node {header, ...}) = header;
    2.49 +fun get_header (Node {header = (master, header, errors), ...}) =
    2.50 +  if null errors then (master, header)
    2.51 +  else error (cat_lines errors);
    2.52 +
    2.53  fun set_header header =
    2.54    map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result));
    2.55  
    2.56 @@ -128,7 +131,7 @@
    2.57  datatype node_edit =
    2.58    Clear |
    2.59    Edits of (command_id option * command_id option) list |
    2.60 -  Header of node_header |
    2.61 +  Deps of node_header |
    2.62    Perspective of command_id list;
    2.63  
    2.64  type edit = string * node_edit;
    2.65 @@ -178,22 +181,21 @@
    2.66      (case node_edit of
    2.67        Clear => update_node name clear_node nodes
    2.68      | Edits edits => update_node name (edit_node edits) nodes
    2.69 -    | Header header =>
    2.70 +    | Deps (master, header, errors) =>
    2.71          let
    2.72 -          val imports = (case header of Exn.Res (_, {imports, ...}) => imports | _ => []);
    2.73 -          val header' =
    2.74 -            ((case header of Exn.Res (_, h) => Thy_Header.define_keywords h | _ => ()); header)
    2.75 -              handle exn as ERROR _ => Exn.Exn exn;
    2.76 +          val errors1 =
    2.77 +            (Thy_Header.define_keywords header; errors)
    2.78 +              handle ERROR msg => errors @ [msg];
    2.79            val nodes1 = nodes
    2.80              |> default_node name
    2.81 -            |> fold default_node imports;
    2.82 +            |> fold default_node (#imports header);
    2.83            val nodes2 = nodes1
    2.84              |> Graph.Keys.fold
    2.85                  (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
    2.86 -          val (header'', nodes3) =
    2.87 -            (header', Graph.add_deps_acyclic (name, imports) nodes2)
    2.88 -              handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
    2.89 -        in Graph.map_node name (set_header header'') nodes3 end
    2.90 +          val (nodes3, errors2) =
    2.91 +            (Graph.add_deps_acyclic (name, #imports header) nodes2, errors1)
    2.92 +              handle Graph.CYCLES cs => (nodes2, errors1 @ map cycle_msg cs);
    2.93 +        in Graph.map_node name (set_header (master, header, errors2)) nodes3 end
    2.94      | Perspective perspective => update_node name (set_perspective perspective) nodes);
    2.95  
    2.96  fun put_node (name, node) (Version nodes) =
    2.97 @@ -374,7 +376,7 @@
    2.98  fun init_theory imports node =
    2.99    let
   2.100      (* FIXME provide files via Scala layer, not master_dir *)
   2.101 -    val (dir, header) = Exn.release (get_header node);
   2.102 +    val (dir, header) = get_header node;
   2.103      val master_dir =
   2.104        (case Url.explode dir of
   2.105          Url.File path => path
   2.106 @@ -393,7 +395,7 @@
   2.107  
   2.108  fun check_theory full name node =
   2.109    is_some (Thy_Info.lookup_theory name) orelse
   2.110 -  is_some (Exn.get_res (get_header node)) andalso (not full orelse is_some (get_result node));
   2.111 +  can get_header node andalso (not full orelse is_some (get_result node));
   2.112  
   2.113  fun last_common state last_visible node0 node =
   2.114    let
     3.1 --- a/src/Pure/PIDE/document.scala	Tue Aug 07 13:21:29 2012 +0200
     3.2 +++ b/src/Pure/PIDE/document.scala	Tue Aug 07 15:01:48 2012 +0200
     3.3 @@ -35,14 +35,18 @@
     3.4    type Edit_Text = Edit[Text.Edit, Text.Perspective]
     3.5    type Edit_Command = Edit[(Option[Command], Option[Command]), Command.Perspective]
     3.6  
     3.7 -  type Node_Header = Exn.Result[Node.Deps]
     3.8 -
     3.9    object Node
    3.10    {
    3.11 -    sealed case class Deps(
    3.12 +    sealed case class Header(
    3.13        imports: List[Name],
    3.14        keywords: Thy_Header.Keywords,
    3.15 -      uses: List[(String, Boolean)])
    3.16 +      uses: List[(String, Boolean)],
    3.17 +      errors: List[String] = Nil)
    3.18 +    {
    3.19 +      def error(msg: String): Header = copy(errors = errors ::: List(msg))
    3.20 +    }
    3.21 +
    3.22 +    def bad_header(msg: String): Header = Header(Nil, Nil, Nil, List(msg))
    3.23  
    3.24      object Name
    3.25      {
    3.26 @@ -83,7 +87,7 @@
    3.27      }
    3.28      case class Clear[A, B]() extends Edit[A, B]
    3.29      case class Edits[A, B](edits: List[A]) extends Edit[A, B]
    3.30 -    case class Header[A, B](header: Node_Header) extends Edit[A, B]
    3.31 +    case class Deps[A, B](header: Header) extends Edit[A, B]
    3.32      case class Perspective[A, B](perspective: B) extends Edit[A, B]
    3.33  
    3.34      def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
    3.35 @@ -103,14 +107,14 @@
    3.36    }
    3.37  
    3.38    final class Node private(
    3.39 -    val header: Node_Header = Exn.Exn(ERROR("Bad theory header")),
    3.40 +    val header: Node.Header = Node.bad_header("Bad theory header"),
    3.41      val perspective: Command.Perspective = Command.Perspective.empty,
    3.42      val blobs: Map[String, Blob] = Map.empty,
    3.43      val commands: Linear_Set[Command] = Linear_Set.empty)
    3.44    {
    3.45      def clear: Node = new Node(header = header)
    3.46  
    3.47 -    def update_header(new_header: Node_Header): Node =
    3.48 +    def update_header(new_header: Node.Header): Node =
    3.49        new Node(new_header, perspective, blobs, commands)
    3.50  
    3.51      def update_perspective(new_perspective: Command.Perspective): Node =
    3.52 @@ -122,12 +126,6 @@
    3.53      def update_commands(new_commands: Linear_Set[Command]): Node =
    3.54        new Node(header, perspective, blobs, new_commands)
    3.55  
    3.56 -    def imports: List[Node.Name] =
    3.57 -      header match { case Exn.Res(deps) => deps.imports case _ => Nil }
    3.58 -
    3.59 -    def keywords: Thy_Header.Keywords =
    3.60 -      header match { case Exn.Res(deps) => deps.keywords case _ => Nil }
    3.61 -
    3.62  
    3.63      /* commands */
    3.64  
    3.65 @@ -190,7 +188,7 @@
    3.66      def + (entry: (Node.Name, Node)): Nodes =
    3.67      {
    3.68        val (name, node) = entry
    3.69 -      val imports = node.imports
    3.70 +      val imports = node.header.imports
    3.71        val graph1 =
    3.72          (graph.default_node(name, Node.empty) /: imports)((g, p) => g.default_node(p, Node.empty))
    3.73        val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name))
     4.1 --- a/src/Pure/PIDE/protocol.ML	Tue Aug 07 13:21:29 2012 +0200
     4.2 +++ b/src/Pure/PIDE/protocol.ML	Tue Aug 07 15:01:48 2012 +0200
     4.3 @@ -37,16 +37,15 @@
     4.4                    fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
     4.5                    fn ([], a) =>
     4.6                      let
     4.7 -                      val ((((master, name), imports), keywords), uses) =
     4.8 -                        pair (pair (pair (pair string string) (list string))
     4.9 -                          (list (pair string (option (pair string (list string))))))
    4.10 -                          (list (pair string bool)) a;
    4.11 -                      val res =
    4.12 -                        Exn.capture (fn () =>
    4.13 -                          (master, Thy_Header.make name imports keywords
    4.14 -                            (map (apfst Path.explode) uses))) ();
    4.15 -                    in Document.Header res end,
    4.16 -                  fn ([a], []) => Document.Header (Exn.Exn (ERROR a)),
    4.17 +                      val (master, (name, (imports, (keywords, (uses, errors))))) =
    4.18 +                        pair string (pair string (pair (list string)
    4.19 +                          (pair (list (pair string (option (pair string (list string)))))
    4.20 +                            (pair (list (pair string bool)) (list string))))) a;
    4.21 +                      val (uses', errors') =
    4.22 +                        (map (apfst Path.explode) uses, errors)
    4.23 +                          handle ERROR msg => ([], errors @ [msg]);
    4.24 +                      val header = Thy_Header.make name imports keywords uses';
    4.25 +                    in Document.Deps (master, header, errors') end,
    4.26                    fn (a, []) => Document.Perspective (map int_atom a)]))
    4.27              end;
    4.28  
     5.1 --- a/src/Pure/PIDE/protocol.scala	Tue Aug 07 13:21:29 2012 +0200
     5.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Aug 07 15:01:48 2012 +0200
     5.3 @@ -215,17 +215,16 @@
     5.4          variant(List(
     5.5            { case Document.Node.Clear() => (Nil, Nil) },
     5.6            { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
     5.7 -          { case Document.Node.Header(Exn.Res(deps)) =>
     5.8 +          { case Document.Node.Deps(header) =>
     5.9                val dir = Isabelle_System.posix_path(name.dir)
    5.10 -              val imports = deps.imports.map(_.node)
    5.11 +              val imports = header.imports.map(_.node)
    5.12                // FIXME val uses = deps.uses.map(p => (Isabelle_System.posix_path(p._1), p._2))
    5.13 -              val uses = deps.uses
    5.14 +              val uses = header.uses
    5.15                (Nil,
    5.16 -                pair(pair(pair(pair(Encode.string, Encode.string), list(Encode.string)),
    5.17 -                  list(pair(Encode.string, option(pair(Encode.string, list(Encode.string)))))),
    5.18 -                    list(pair(Encode.string, bool)))(
    5.19 -                (((dir, name.theory), imports), deps.keywords), uses)) },
    5.20 -          { case Document.Node.Header(Exn.Exn(e)) => (List(encode(Exn.message(e))), Nil) },
    5.21 +                pair(Encode.string, pair(Encode.string, pair(list(Encode.string),
    5.22 +                  pair(list(pair(Encode.string, option(pair(Encode.string, list(Encode.string))))),
    5.23 +                  pair(list(pair(Encode.string, bool)), list(Encode.string))))))(
    5.24 +                (dir, (name.theory, (imports, (header.keywords, (uses, header.errors))))))) },
    5.25            { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))
    5.26        def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
    5.27        {
     6.1 --- a/src/Pure/System/build.scala	Tue Aug 07 13:21:29 2012 +0200
     6.2 +++ b/src/Pure/System/build.scala	Tue Aug 07 15:01:48 2012 +0200
     6.3 @@ -363,12 +363,7 @@
     6.4            val all_files =
     6.5              thy_deps.map({ case (n, h) =>
     6.6                val thy = Path.explode(n.node).expand
     6.7 -              val uses =
     6.8 -                h match {
     6.9 -                  case Exn.Res(d) =>
    6.10 -                    d.uses.map(p => (Path.explode(n.dir) + Path.explode(p._1)).expand)
    6.11 -                  case _ => Nil
    6.12 -                }
    6.13 +              val uses = h.uses.map(p => (Path.explode(n.dir) + Path.explode(p._1)).expand)
    6.14                thy :: uses
    6.15              }).flatten ::: info.files.map(file => info.dir + file)
    6.16            val sources =
     7.1 --- a/src/Pure/System/session.scala	Tue Aug 07 13:21:29 2012 +0200
     7.2 +++ b/src/Pure/System/session.scala	Tue Aug 07 15:01:48 2012 +0200
     7.3 @@ -160,15 +160,13 @@
     7.4  
     7.5    /* theory files */
     7.6  
     7.7 -  def header_edit(name: Document.Node.Name, header: Document.Node_Header): Document.Edit_Text =
     7.8 +  def header_edit(name: Document.Node.Name, header: Document.Node.Header): Document.Edit_Text =
     7.9    {
    7.10 -    val header1: Document.Node_Header =
    7.11 -      header match {
    7.12 -        case Exn.Res(_) if (thy_load.is_loaded(name.theory)) =>
    7.13 -          Exn.Exn(ERROR("Attempt to update loaded theory " + quote(name.theory)))
    7.14 -        case _ => header
    7.15 -      }
    7.16 -    (name, Document.Node.Header(header1))
    7.17 +    val header1 =
    7.18 +      if (thy_load.is_loaded(name.theory))
    7.19 +        header.error("Attempt to update loaded theory " + quote(name.theory))
    7.20 +      else header
    7.21 +    (name, Document.Node.Deps(header1))
    7.22    }
    7.23  
    7.24  
    7.25 @@ -456,7 +454,7 @@
    7.26    { session_actor !? Edit(edits) }
    7.27  
    7.28    def init_node(name: Document.Node.Name,
    7.29 -    header: Document.Node_Header, perspective: Text.Perspective, text: String)
    7.30 +    header: Document.Node.Header, perspective: Text.Perspective, text: String)
    7.31    {
    7.32      edit(List(header_edit(name, header),
    7.33        name -> Document.Node.Clear(),    // FIXME diff wrt. existing node
    7.34 @@ -465,7 +463,7 @@
    7.35    }
    7.36  
    7.37    def edit_node(name: Document.Node.Name,
    7.38 -    header: Document.Node_Header, perspective: Text.Perspective, text_edits: List[Text.Edit])
    7.39 +    header: Document.Node.Header, perspective: Text.Perspective, text_edits: List[Text.Edit])
    7.40    {
    7.41      edit(List(header_edit(name, header),
    7.42        name -> Document.Node.Edits(text_edits),
     8.1 --- a/src/Pure/Thy/thy_header.ML	Tue Aug 07 13:21:29 2012 +0200
     8.2 +++ b/src/Pure/Thy/thy_header.ML	Tue Aug 07 15:01:48 2012 +0200
     8.3 @@ -7,7 +7,8 @@
     8.4  signature THY_HEADER =
     8.5  sig
     8.6    type header =
     8.7 -   {name: string, imports: string list,
     8.8 +   {name: string,
     8.9 +    imports: string list,
    8.10      keywords: (string * Keyword.spec option) list,
    8.11      uses: (Path.T * bool) list}
    8.12    val make: string -> string list -> (string * Keyword.spec option) list ->
    8.13 @@ -23,7 +24,8 @@
    8.14  struct
    8.15  
    8.16  type header =
    8.17 - {name: string, imports: string list,
    8.18 + {name: string,
    8.19 +  imports: string list,
    8.20    keywords: (string * Keyword.spec option) list,
    8.21    uses: (Path.T * bool) list};
    8.22  
     9.1 --- a/src/Pure/Thy/thy_info.scala	Tue Aug 07 13:21:29 2012 +0200
     9.2 +++ b/src/Pure/Thy/thy_info.scala	Tue Aug 07 15:01:48 2012 +0200
     9.3 @@ -24,7 +24,7 @@
     9.4  
     9.5    /* dependencies */
     9.6  
     9.7 -  type Dep = (Document.Node.Name, Document.Node_Header)
     9.8 +  type Dep = (Document.Node.Name, Document.Node.Header)
     9.9    private type Required = (List[Dep], Set[Document.Node.Name])
    9.10  
    9.11    private def require_thys(initiators: List[Document.Node.Name],
    9.12 @@ -40,7 +40,7 @@
    9.13      else {
    9.14        try {
    9.15          if (initiators.contains(name)) error(cycle_msg(initiators))
    9.16 -        val node_deps =
    9.17 +        val header =
    9.18            try { thy_load.check_thy(name) }
    9.19            catch {
    9.20              case ERROR(msg) =>
    9.21 @@ -48,10 +48,13 @@
    9.22                  quote(name.theory) + required_by(initiators))
    9.23            }
    9.24          val (deps1, seen1) =
    9.25 -          require_thys(name :: initiators, (deps, seen + name), node_deps.imports)
    9.26 -        ((name, Exn.Res(node_deps)) :: deps1, seen1)
    9.27 +          require_thys(name :: initiators, (deps, seen + name), header.imports)
    9.28 +        ((name, header) :: deps1, seen1)
    9.29        }
    9.30 -      catch { case e: Throwable => (((name, Exn.Exn(e)): Dep) :: deps, seen + name) }
    9.31 +      catch {
    9.32 +        case e: Throwable =>
    9.33 +          ((name, Document.Node.bad_header(Exn.message(e))) :: deps, seen + name)
    9.34 +      }
    9.35      }
    9.36    }
    9.37  
    10.1 --- a/src/Pure/Thy/thy_load.scala	Tue Aug 07 13:21:29 2012 +0200
    10.2 +++ b/src/Pure/Thy/thy_load.scala	Tue Aug 07 15:01:48 2012 +0200
    10.3 @@ -60,7 +60,7 @@
    10.4      }
    10.5    }
    10.6  
    10.7 -  def check_header(name: Document.Node.Name, header: Thy_Header): Document.Node.Deps =
    10.8 +  def check_header(name: Document.Node.Name, header: Thy_Header): Document.Node.Header =
    10.9    {
   10.10      val name1 = header.name
   10.11      val imports = header.imports.map(import_name(name.dir, _))
   10.12 @@ -69,10 +69,10 @@
   10.13      if (name.theory != name1)
   10.14        error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) +
   10.15          " for theory " + quote(name1))
   10.16 -    Document.Node.Deps(imports, header.keywords, uses)
   10.17 +    Document.Node.Header(imports, header.keywords, uses)
   10.18    }
   10.19  
   10.20 -  def check_thy(name: Document.Node.Name): Document.Node.Deps =
   10.21 +  def check_thy(name: Document.Node.Name): Document.Node.Header =
   10.22      check_header(name, read_header(name))
   10.23  }
   10.24  
    11.1 --- a/src/Pure/Thy/thy_syntax.scala	Tue Aug 07 13:21:29 2012 +0200
    11.2 +++ b/src/Pure/Thy/thy_syntax.scala	Tue Aug 07 15:01:48 2012 +0200
    11.3 @@ -134,19 +134,16 @@
    11.4      val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
    11.5  
    11.6      edits foreach {
    11.7 -      case (name, Document.Node.Header(header)) =>
    11.8 +      case (name, Document.Node.Deps(header)) =>
    11.9          val node = nodes(name)
   11.10          val update_header =
   11.11 -          (node.header, header) match {
   11.12 -            case (Exn.Res(deps0), Exn.Res(deps)) => deps0 != deps
   11.13 -            case _ => true
   11.14 -          }
   11.15 +          !node.header.errors.isEmpty || !header.errors.isEmpty || node.header != header
   11.16          if (update_header) {
   11.17            val node1 = node.update_header(header)
   11.18 -          updated_imports = updated_imports || (node.imports != node1.imports)
   11.19 -          updated_keywords = updated_keywords || (node.keywords != node1.keywords)
   11.20 +          updated_imports = updated_imports || (node.header.imports != node1.header.imports)
   11.21 +          updated_keywords = updated_keywords || (node.header.keywords != node1.header.keywords)
   11.22            nodes += (name -> node1)
   11.23 -          doc_edits += (name -> Document.Node.Header(header))
   11.24 +          doc_edits += (name -> Document.Node.Deps(header))
   11.25          }
   11.26        case _ =>
   11.27      }
   11.28 @@ -289,7 +286,7 @@
   11.29          doc_edits += (name -> Document.Node.Edits(cmd_edits))
   11.30          nodes += (name -> node.update_commands(commands3))
   11.31  
   11.32 -      case (name, Document.Node.Header(_)) =>
   11.33 +      case (name, Document.Node.Deps(_)) =>
   11.34  
   11.35        case (name, Document.Node.Perspective(text_perspective)) =>
   11.36          val node = nodes(name)
    12.1 --- a/src/Tools/jEdit/src/document_model.scala	Tue Aug 07 13:21:29 2012 +0200
    12.2 +++ b/src/Tools/jEdit/src/document_model.scala	Tue Aug 07 15:01:48 2012 +0200
    12.3 @@ -63,13 +63,16 @@
    12.4  {
    12.5    /* header */
    12.6  
    12.7 -  def node_header(): Document.Node_Header =
    12.8 +  def node_header(): Document.Node.Header =
    12.9    {
   12.10      Swing_Thread.require()
   12.11      Isabelle.buffer_lock(buffer) {
   12.12        Exn.capture {
   12.13          Isabelle.thy_load.check_header(name,
   12.14            Thy_Header.read(buffer.getSegment(0, buffer.getLength)))
   12.15 +      } match {
   12.16 +        case Exn.Res(header) => header
   12.17 +        case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
   12.18        }
   12.19      }
   12.20    }