src/Pure/PIDE/document.ML
changeset 59715 4f0d0e4ad68d
parent 59702 58dfaa369c11
child 59716 8c56b34a88b0
     1.1 --- a/src/Pure/PIDE/document.ML	Mon Mar 16 11:30:54 2015 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon Mar 16 13:32:31 2015 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  signature DOCUMENT =
     1.5  sig
     1.6    val timing: bool Unsynchronized.ref
     1.7 -  type node_header = string * Thy_Header.header * string list
     1.8 +  type node_header = {master: string, header: Thy_Header.header, errors: string list}
     1.9    type overlay = Document_ID.command * (string * string list)
    1.10    datatype node_edit =
    1.11      Edits of (Document_ID.command option * Document_ID.command option) list |
    1.12 @@ -42,7 +42,8 @@
    1.13  fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document_ID.print id);
    1.14  fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document_ID.print id);
    1.15  
    1.16 -type node_header = string * Thy_Header.header * string list;
    1.17 +type node_header =
    1.18 +  {master: string, header: Thy_Header.header, errors: string list};
    1.19  
    1.20  type perspective =
    1.21   {required: bool,  (*required node*)
    1.22 @@ -74,7 +75,8 @@
    1.23    visible_last = try List.last command_ids,
    1.24    overlays = Inttab.make_list overlays};
    1.25  
    1.26 -val no_header: node_header = ("", Thy_Header.make ("", Position.none) [] [], []);
    1.27 +val no_header: node_header =
    1.28 +  {master = "", header = Thy_Header.make ("", Position.none) [] [], errors = []};
    1.29  val no_perspective = make_perspective (false, [], []);
    1.30  
    1.31  val empty_node = make_node (no_header, NONE, no_perspective, Entries.empty, NONE);
    1.32 @@ -95,20 +97,16 @@
    1.33  
    1.34  (* basic components *)
    1.35  
    1.36 -fun master_directory (Node {header = (master, _, _), ...}) =
    1.37 +fun master_directory (Node {header = {master, ...}, ...}) =
    1.38    (case try Url.explode master of
    1.39      SOME (Url.File path) => path
    1.40    | _ => Path.current);
    1.41  
    1.42 -fun set_header header =
    1.43 +fun set_header master header errors =
    1.44    map_node (fn (_, keywords, perspective, entries, result) =>
    1.45 -    (header, keywords, perspective, entries, result));
    1.46 +    ({master = master, header = header, errors = errors}, keywords, perspective, entries, result));
    1.47  
    1.48 -fun get_header_raw (Node {header, ...}) = header;
    1.49 -
    1.50 -fun get_header (Node {header = (master, header, errors), ...}) =
    1.51 -  if null errors then (master, header)
    1.52 -  else error (cat_lines errors);
    1.53 +fun get_header (Node {header, ...}) = header;
    1.54  
    1.55  fun set_keywords keywords =
    1.56    map_node (fn (header, _, perspective, entries, result) =>
    1.57 @@ -118,7 +116,16 @@
    1.58  
    1.59  fun read_header node span =
    1.60    let
    1.61 -    val {name = (name, _), imports, keywords} = #2 (get_header node);
    1.62 +    val {header, errors, ...} = get_header node;
    1.63 +    val _ =
    1.64 +      if null errors then ()
    1.65 +      else
    1.66 +        cat_lines errors |>
    1.67 +        (case Position.get_id (Position.thread_data ()) of
    1.68 +          NONE => I
    1.69 +        | SOME id => Protocol_Message.command_positions_yxml id)
    1.70 +        |> error;
    1.71 +    val {name = (name, _), imports, keywords} = header;
    1.72      val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span;
    1.73    in Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords end;
    1.74  
    1.75 @@ -232,7 +239,7 @@
    1.76    Version
    1.77      (case node_edit of
    1.78        Edits edits => update_node name (edit_node edits) nodes
    1.79 -    | Deps (master, header, errors) =>
    1.80 +    | Deps {master, header, errors} =>
    1.81          let
    1.82            val imports = map fst (#imports header);
    1.83            val nodes1 = nodes
    1.84 @@ -244,7 +251,7 @@
    1.85            val (nodes3, errors1) =
    1.86              (String_Graph.add_deps_acyclic (name, imports) nodes2, errors)
    1.87                handle String_Graph.CYCLES cs => (nodes2, errors @ map cycle_msg cs);
    1.88 -        in String_Graph.map_node name (set_header (master, header, errors1)) nodes3 end
    1.89 +        in String_Graph.map_node name (set_header master header errors1) nodes3 end
    1.90      | Perspective perspective => update_node name (set_perspective perspective) nodes);
    1.91  
    1.92  fun update_keywords name nodes =
    1.93 @@ -252,7 +259,7 @@
    1.94      if is_empty_node node then node
    1.95      else
    1.96        let
    1.97 -        val (master, header, errors) = get_header_raw node;
    1.98 +        val {master, header, errors} = get_header node;
    1.99          val imports_keywords = map_filter (get_keywords o get_node nodes o #1) (#imports header);
   1.100          val keywords =
   1.101            Library.foldl Keyword.merge_keywords (Session.get_keywords (), imports_keywords);
   1.102 @@ -262,7 +269,7 @@
   1.103                (keywords, if member (op =) errors msg then errors else errors @ [msg]);
   1.104        in
   1.105          node
   1.106 -        |> set_header (master, header, errors')
   1.107 +        |> set_header master header errors'
   1.108          |> set_keywords (SOME keywords')
   1.109        end);
   1.110  
   1.111 @@ -527,7 +534,7 @@
   1.112  
   1.113  fun check_theory full name node =
   1.114    is_some (loaded_theory name) orelse
   1.115 -  can get_header node andalso (not full orelse is_some (get_result node));
   1.116 +  null (#errors (get_header node)) andalso (not full orelse is_some (get_result node));
   1.117  
   1.118  fun last_common keywords state node_required node0 node =
   1.119    let