node-specific keywords, with session base syntax as default;
authorwenzelm
Wed Dec 03 22:34:28 2014 +0100 (2014-12-03)
changeset 5908694b2690ad494
parent 59085 08a6901eb035
child 59087 8535cfcfa493
node-specific keywords, with session base syntax as default;
src/Pure/PIDE/document.ML
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/session.ML
src/Pure/PIDE/session.scala
src/Pure/ROOT.ML
src/Pure/Thy/thy_syntax.scala
     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;
     2.1 --- a/src/Pure/PIDE/protocol.ML	Wed Dec 03 20:45:20 2014 +0100
     2.2 +++ b/src/Pure/PIDE/protocol.ML	Wed Dec 03 22:34:28 2014 +0100
     2.3 @@ -23,10 +23,6 @@
     2.4        end);
     2.5  
     2.6  val _ =
     2.7 -  Isabelle_Process.protocol_command "Document.init_keywords"
     2.8 -    (fn [] => Document.init_keywords ());
     2.9 -
    2.10 -val _ =
    2.11    Isabelle_Process.protocol_command "Document.define_blob"
    2.12      (fn [digest, content] => Document.change_state (Document.define_blob digest content));
    2.13  
     3.1 --- a/src/Pure/PIDE/session.ML	Wed Dec 03 20:45:20 2014 +0100
     3.2 +++ b/src/Pure/PIDE/session.ML	Wed Dec 03 22:34:28 2014 +0100
     3.3 @@ -8,6 +8,7 @@
     3.4  sig
     3.5    val name: unit -> string
     3.6    val welcome: unit -> string
     3.7 +  val get_keywords: unit -> Keyword.keywords
     3.8    val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
     3.9      (Path.T * Path.T) list -> string -> string * string -> bool -> unit
    3.10    val finish: unit -> unit
    3.11 @@ -31,6 +32,12 @@
    3.12    else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")";
    3.13  
    3.14  
    3.15 +(* base syntax *)
    3.16 +
    3.17 +val keywords = Unsynchronized.ref Keyword.empty_keywords;
    3.18 +fun get_keywords () = ! keywords;
    3.19 +
    3.20 +
    3.21  (* init *)
    3.22  
    3.23  fun init build info info_path doc doc_graph doc_output doc_variants doc_files
    3.24 @@ -57,6 +64,9 @@
    3.25    Future.shutdown ();
    3.26    Event_Timer.shutdown ();
    3.27    Future.shutdown ();
    3.28 +  keywords :=
    3.29 +    fold (curry Keyword.merge_keywords o Thy_Header.get_keywords o Thy_Info.get_theory)
    3.30 +      (Thy_Info.get_names ()) Keyword.empty_keywords;
    3.31    session_finished := true);
    3.32  
    3.33  
     4.1 --- a/src/Pure/PIDE/session.scala	Wed Dec 03 20:45:20 2014 +0100
     4.2 +++ b/src/Pure/PIDE/session.scala	Wed Dec 03 22:34:28 2014 +0100
     4.3 @@ -611,7 +611,6 @@
     4.4    def init_options(options: Options)
     4.5    {
     4.6      update_options(options)
     4.7 -    protocol_command("Document.init_keywords")
     4.8    }
     4.9  
    4.10    def dialog_result(id: Document_ID.Generic, serial: Long, result: String)
     5.1 --- a/src/Pure/ROOT.ML	Wed Dec 03 20:45:20 2014 +0100
     5.2 +++ b/src/Pure/ROOT.ML	Wed Dec 03 22:34:28 2014 +0100
     5.3 @@ -315,6 +315,7 @@
     5.4  use "PIDE/query_operation.ML";
     5.5  use "PIDE/resources.ML";
     5.6  use "Thy/thy_info.ML";
     5.7 +use "PIDE/session.ML";
     5.8  use "PIDE/document.ML";
     5.9  
    5.10  (*theory and proof operations*)
    5.11 @@ -325,7 +326,6 @@
    5.12  
    5.13  (* Isabelle/Isar system *)
    5.14  
    5.15 -use "PIDE/session.ML";
    5.16  use "System/command_line.ML";
    5.17  use "System/system_channel.ML";
    5.18  use "System/message_channel.ML";
     6.1 --- a/src/Pure/Thy/thy_syntax.scala	Wed Dec 03 20:45:20 2014 +0100
     6.2 +++ b/src/Pure/Thy/thy_syntax.scala	Wed Dec 03 22:34:28 2014 +0100
     6.3 @@ -97,8 +97,9 @@
     6.4        val syntax =
     6.5          if (node.is_empty) None
     6.6          else {
     6.7 -          val imports_syntax = node.header.imports.flatMap(a => nodes(a).syntax)
     6.8 -          Some((resources.base_syntax /: imports_syntax)(_ ++ _).add_keywords(node.header.keywords))
     6.9 +          val header = node.header
    6.10 +          val imports_syntax = header.imports.flatMap(a => nodes(a).syntax)
    6.11 +          Some((resources.base_syntax /: imports_syntax)(_ ++ _).add_keywords(header.keywords))
    6.12          }
    6.13        nodes += (name -> node.update_syntax(syntax))
    6.14      }