src/Pure/PIDE/document.ML
changeset 59086 94b2690ad494
parent 59085 08a6901eb035
child 59193 59f1591a11cb
     1.1 --- a/src/Pure/PIDE/document.ML	Wed Dec 03 20:45:20 2014 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Wed Dec 03 22:34:28 2014 +0100
     1.3 @@ -8,7 +8,6 @@
     1.4  signature DOCUMENT =
     1.5  sig
     1.6    val timing: bool Unsynchronized.ref
     1.7 -  val init_keywords: unit -> unit
     1.8    type node_header = string * Thy_Header.header * string list
     1.9    type overlay = Document_ID.command * (string * string list)
    1.10    datatype node_edit =
    1.11 @@ -38,17 +37,6 @@
    1.12  
    1.13  
    1.14  
    1.15 -(** global keywords **)
    1.16 -
    1.17 -val global_keywords = Synchronized.var "global_keywords" Keyword.empty_keywords;
    1.18 -
    1.19 -fun init_keywords () =
    1.20 -  Synchronized.change global_keywords
    1.21 -    (fn _ =>
    1.22 -      fold (curry Keyword.merge_keywords o Thy_Header.get_keywords o Thy_Info.get_theory)
    1.23 -        (Thy_Info.get_names ()) Keyword.empty_keywords);
    1.24 -
    1.25 -fun get_keywords () = Synchronized.value global_keywords;
    1.26  
    1.27  
    1.28  
    1.29 @@ -69,17 +57,19 @@
    1.30  
    1.31  abstype node = Node of
    1.32   {header: node_header,  (*master directory, theory header, errors*)
    1.33 +  keywords: Keyword.keywords option,  (*outer syntax keywords*)
    1.34    perspective: perspective,  (*command perspective*)
    1.35    entries: Command.exec option Entries.T,  (*command entries with excecutions*)
    1.36    result: Command.eval option}  (*result of last execution*)
    1.37  and version = Version of node String_Graph.T  (*development graph wrt. static imports*)
    1.38  with
    1.39  
    1.40 -fun make_node (header, perspective, entries, result) =
    1.41 -  Node {header = header, perspective = perspective, entries = entries, result = result};
    1.42 +fun make_node (header, keywords, perspective, entries, result) =
    1.43 +  Node {header = header, keywords = keywords, perspective = perspective,
    1.44 +    entries = entries, result = result};
    1.45  
    1.46 -fun map_node f (Node {header, perspective, entries, result}) =
    1.47 -  make_node (f (header, perspective, entries, result));
    1.48 +fun map_node f (Node {header, keywords, perspective, entries, result}) =
    1.49 +  make_node (f (header, keywords, perspective, entries, result));
    1.50  
    1.51  fun make_perspective (required, command_ids, overlays) : perspective =
    1.52   {required = required,
    1.53 @@ -90,7 +80,7 @@
    1.54  val no_header: node_header = ("", Thy_Header.make ("", Position.none) [] [], []);
    1.55  val no_perspective = make_perspective (false, [], []);
    1.56  
    1.57 -val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
    1.58 +val empty_node = make_node (no_header, NONE, no_perspective, Entries.empty, NONE);
    1.59  
    1.60  fun is_no_perspective ({required, visible, visible_last, overlays}: perspective) =
    1.61    not required andalso
    1.62 @@ -98,8 +88,9 @@
    1.63    is_none visible_last andalso
    1.64    Inttab.is_empty overlays;
    1.65  
    1.66 -fun is_empty_node (Node {header, perspective, entries, result}) =
    1.67 +fun is_empty_node (Node {header, keywords, perspective, entries, result}) =
    1.68    header = no_header andalso
    1.69 +  is_none keywords andalso
    1.70    is_no_perspective perspective andalso
    1.71    Entries.is_empty entries andalso
    1.72    is_none result;
    1.73 @@ -113,12 +104,21 @@
    1.74    | _ => Path.current);
    1.75  
    1.76  fun set_header header =
    1.77 -  map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result));
    1.78 +  map_node (fn (_, keywords, perspective, entries, result) =>
    1.79 +    (header, keywords, perspective, entries, result));
    1.80 +
    1.81 +fun get_header_raw (Node {header, ...}) = header;
    1.82  
    1.83  fun get_header (Node {header = (master, header, errors), ...}) =
    1.84    if null errors then (master, header)
    1.85    else error (cat_lines errors);
    1.86  
    1.87 +fun set_keywords keywords =
    1.88 +  map_node (fn (header, _, perspective, entries, result) =>
    1.89 +    (header, keywords, perspective, entries, result));
    1.90 +
    1.91 +fun get_keywords (Node {keywords, ...}) = keywords;
    1.92 +
    1.93  fun read_header node span =
    1.94    let
    1.95      val {name = (name, _), imports, keywords} = #2 (get_header node);
    1.96 @@ -126,8 +126,10 @@
    1.97    in Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords end;
    1.98  
    1.99  fun get_perspective (Node {perspective, ...}) = perspective;
   1.100 +
   1.101  fun set_perspective args =
   1.102 -  map_node (fn (header, _, entries, result) => (header, make_perspective args, entries, result));
   1.103 +  map_node (fn (header, keywords, _, entries, result) =>
   1.104 +    (header, keywords, make_perspective args, entries, result));
   1.105  
   1.106  val required_node = #required o get_perspective;
   1.107  val visible_command = Inttab.defined o #visible o get_perspective;
   1.108 @@ -136,7 +138,9 @@
   1.109  val overlays = Inttab.lookup_list o #overlays o get_perspective;
   1.110  
   1.111  fun map_entries f =
   1.112 -  map_node (fn (header, perspective, entries, result) => (header, perspective, f entries, result));
   1.113 +  map_node (fn (header, keywords, perspective, entries, result) =>
   1.114 +    (header, keywords, perspective, f entries, result));
   1.115 +
   1.116  fun get_entries (Node {entries, ...}) = entries;
   1.117  
   1.118  fun iterate_entries f = Entries.iterate NONE f o get_entries;
   1.119 @@ -146,8 +150,10 @@
   1.120    | SOME id => Entries.iterate (SOME id) f entries);
   1.121  
   1.122  fun get_result (Node {result, ...}) = result;
   1.123 +
   1.124  fun set_result result =
   1.125 -  map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
   1.126 +  map_node (fn (header, keywords, perspective, entries, _) =>
   1.127 +    (header, keywords, perspective, entries, result));
   1.128  
   1.129  fun changed_result node node' =
   1.130    (case (get_result node, get_result node') of
   1.131 @@ -222,21 +228,43 @@
   1.132      | Deps (master, header, errors) =>
   1.133          let
   1.134            val imports = map fst (#imports header);
   1.135 -          val errors1 =
   1.136 -            (Synchronized.change global_keywords (Keyword.add_keywords (#keywords header)); errors)
   1.137 -              handle ERROR msg => errors @ [msg];
   1.138            val nodes1 = nodes
   1.139              |> default_node name
   1.140              |> fold default_node imports;
   1.141            val nodes2 = nodes1
   1.142              |> String_Graph.Keys.fold
   1.143                  (fn dep => String_Graph.del_edge (dep, name)) (String_Graph.imm_preds nodes1 name);
   1.144 -          val (nodes3, errors2) =
   1.145 -            (String_Graph.add_deps_acyclic (name, imports) nodes2, errors1)
   1.146 -              handle String_Graph.CYCLES cs => (nodes2, errors1 @ map cycle_msg cs);
   1.147 -        in String_Graph.map_node name (set_header (master, header, errors2)) nodes3 end
   1.148 +          val (nodes3, errors1) =
   1.149 +            (String_Graph.add_deps_acyclic (name, imports) nodes2, errors)
   1.150 +              handle String_Graph.CYCLES cs => (nodes2, errors @ map cycle_msg cs);
   1.151 +        in String_Graph.map_node name (set_header (master, header, errors1)) nodes3 end
   1.152      | Perspective perspective => update_node name (set_perspective perspective) nodes);
   1.153  
   1.154 +fun update_keywords name nodes =
   1.155 +  nodes |> String_Graph.map_node name (fn node =>
   1.156 +    if is_empty_node node then node
   1.157 +    else
   1.158 +      let
   1.159 +        val (master, header, errors) = get_header_raw node;
   1.160 +        val imports_keywords = map_filter (get_keywords o get_node nodes o #1) (#imports header);
   1.161 +        val keywords =
   1.162 +          Library.foldl Keyword.merge_keywords (Session.get_keywords (), imports_keywords);
   1.163 +        val (keywords', errors') =
   1.164 +          (Keyword.add_keywords (#keywords header) keywords, errors)
   1.165 +            handle ERROR msg =>
   1.166 +              (keywords, if member (op =) errors msg then errors else errors @ [msg]);
   1.167 +      in
   1.168 +        node
   1.169 +        |> set_header (master, header, errors')
   1.170 +        |> set_keywords (SOME keywords')
   1.171 +      end);
   1.172 +
   1.173 +fun edit_keywords edits (Version nodes) =
   1.174 +  Version
   1.175 +    (fold update_keywords
   1.176 +      (String_Graph.all_succs nodes (map_filter (fn (a, Deps _) => SOME a | _ => NONE) edits))
   1.177 +      nodes);
   1.178 +
   1.179  fun put_node (name, node) (Version nodes) =
   1.180    let
   1.181      val nodes1 = update_node name (K node) nodes;
   1.182 @@ -562,7 +590,9 @@
   1.183  fun update old_version_id new_version_id edits state = Runtime.exn_trace_system (fn () =>
   1.184    let
   1.185      val old_version = the_version state old_version_id;
   1.186 -    val new_version = timeit "Document.edit_nodes" (fn () => fold edit_nodes edits old_version);
   1.187 +    val new_version =
   1.188 +      timeit "Document.edit_nodes"
   1.189 +        (fn () => old_version |> fold edit_nodes edits |> edit_keywords edits);
   1.190  
   1.191      val nodes = nodes_of new_version;
   1.192      val required = make_required nodes;
   1.193 @@ -579,7 +609,7 @@
   1.194                timeit ("Document.update " ^ name) (fn () =>
   1.195                  Runtime.exn_trace_system (fn () =>
   1.196                    let
   1.197 -                    val keywords = get_keywords ();
   1.198 +                    val keywords = the_default (Session.get_keywords ()) (get_keywords node);
   1.199                      val imports = map (apsnd Future.join) deps;
   1.200                      val imports_result_changed = exists (#4 o #1 o #2) imports;
   1.201                      val node_required = Symtab.defined required name;