src/Pure/PIDE/document.ML
changeset 48707 ba531af91148
parent 47633 e5c5e73f3e30
child 48735 35c47932584c
     1.1 --- a/src/Pure/PIDE/document.ML	Tue Aug 07 13:21:29 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Tue Aug 07 15:01:48 2012 +0200
     1.3 @@ -15,11 +15,11 @@
     1.4    val new_id: unit -> id
     1.5    val parse_id: string -> id
     1.6    val print_id: id -> string
     1.7 -  type node_header = (string * Thy_Header.header) Exn.result
     1.8 +  type node_header = string * Thy_Header.header * string list
     1.9    datatype node_edit =
    1.10      Clear |
    1.11      Edits of (command_id option * command_id option) list |
    1.12 -    Header of node_header |
    1.13 +    Deps of node_header |
    1.14      Perspective of command_id list
    1.15    type edit = string * node_edit
    1.16    type state
    1.17 @@ -59,7 +59,7 @@
    1.18  
    1.19  (** document structure **)
    1.20  
    1.21 -type node_header = (string * Thy_Header.header) Exn.result;
    1.22 +type node_header = string * Thy_Header.header * string list;
    1.23  type perspective = (command_id -> bool) * command_id option;
    1.24  structure Entries = Linear_Set(type key = command_id val ord = int_ord);
    1.25  
    1.26 @@ -67,7 +67,7 @@
    1.27  val no_exec = Command.memo_value (Toplevel.toplevel, Lazy.value ());
    1.28  
    1.29  abstype node = Node of
    1.30 - {header: node_header,
    1.31 + {header: node_header,  (*master directory, theory header, errors*)
    1.32    perspective: perspective,  (*visible commands, last*)
    1.33    entries: (exec_id * exec) option Entries.T,  (*command entries with excecutions*)
    1.34    result: exec option}  (*result of last execution*)
    1.35 @@ -83,7 +83,7 @@
    1.36  fun make_perspective command_ids : perspective =
    1.37    (Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids);
    1.38  
    1.39 -val no_header = Exn.Exn (ERROR "Bad theory header");
    1.40 +val no_header = ("", Thy_Header.make "" [] [] [], ["Bad theory header"]);
    1.41  val no_perspective = make_perspective [];
    1.42  
    1.43  val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
    1.44 @@ -92,7 +92,10 @@
    1.45  
    1.46  (* basic components *)
    1.47  
    1.48 -fun get_header (Node {header, ...}) = header;
    1.49 +fun get_header (Node {header = (master, header, errors), ...}) =
    1.50 +  if null errors then (master, header)
    1.51 +  else error (cat_lines errors);
    1.52 +
    1.53  fun set_header header =
    1.54    map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result));
    1.55  
    1.56 @@ -128,7 +131,7 @@
    1.57  datatype node_edit =
    1.58    Clear |
    1.59    Edits of (command_id option * command_id option) list |
    1.60 -  Header of node_header |
    1.61 +  Deps of node_header |
    1.62    Perspective of command_id list;
    1.63  
    1.64  type edit = string * node_edit;
    1.65 @@ -178,22 +181,21 @@
    1.66      (case node_edit of
    1.67        Clear => update_node name clear_node nodes
    1.68      | Edits edits => update_node name (edit_node edits) nodes
    1.69 -    | Header header =>
    1.70 +    | Deps (master, header, errors) =>
    1.71          let
    1.72 -          val imports = (case header of Exn.Res (_, {imports, ...}) => imports | _ => []);
    1.73 -          val header' =
    1.74 -            ((case header of Exn.Res (_, h) => Thy_Header.define_keywords h | _ => ()); header)
    1.75 -              handle exn as ERROR _ => Exn.Exn exn;
    1.76 +          val errors1 =
    1.77 +            (Thy_Header.define_keywords header; errors)
    1.78 +              handle ERROR msg => errors @ [msg];
    1.79            val nodes1 = nodes
    1.80              |> default_node name
    1.81 -            |> fold default_node imports;
    1.82 +            |> fold default_node (#imports header);
    1.83            val nodes2 = nodes1
    1.84              |> Graph.Keys.fold
    1.85                  (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
    1.86 -          val (header'', nodes3) =
    1.87 -            (header', Graph.add_deps_acyclic (name, imports) nodes2)
    1.88 -              handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
    1.89 -        in Graph.map_node name (set_header header'') nodes3 end
    1.90 +          val (nodes3, errors2) =
    1.91 +            (Graph.add_deps_acyclic (name, #imports header) nodes2, errors1)
    1.92 +              handle Graph.CYCLES cs => (nodes2, errors1 @ map cycle_msg cs);
    1.93 +        in Graph.map_node name (set_header (master, header, errors2)) nodes3 end
    1.94      | Perspective perspective => update_node name (set_perspective perspective) nodes);
    1.95  
    1.96  fun put_node (name, node) (Version nodes) =
    1.97 @@ -374,7 +376,7 @@
    1.98  fun init_theory imports node =
    1.99    let
   1.100      (* FIXME provide files via Scala layer, not master_dir *)
   1.101 -    val (dir, header) = Exn.release (get_header node);
   1.102 +    val (dir, header) = get_header node;
   1.103      val master_dir =
   1.104        (case Url.explode dir of
   1.105          Url.File path => path
   1.106 @@ -393,7 +395,7 @@
   1.107  
   1.108  fun check_theory full name node =
   1.109    is_some (Thy_Info.lookup_theory name) orelse
   1.110 -  is_some (Exn.get_res (get_header node)) andalso (not full orelse is_some (get_result node));
   1.111 +  can get_header node andalso (not full orelse is_some (get_result node));
   1.112  
   1.113  fun last_common state last_visible node0 node =
   1.114    let