# HG changeset patch # User wenzelm # Date 1417642468 -3600 # Node ID 94b2690ad4944a7a22dd479a9085b6fd40c28ede # Parent 08a6901eb035854dbac1a21cca2b5eb4005602e5 node-specific keywords, with session base syntax as default; diff -r 08a6901eb035 -r 94b2690ad494 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Wed Dec 03 20:45:20 2014 +0100 +++ b/src/Pure/PIDE/document.ML Wed Dec 03 22:34:28 2014 +0100 @@ -8,7 +8,6 @@ signature DOCUMENT = sig val timing: bool Unsynchronized.ref - val init_keywords: unit -> unit type node_header = string * Thy_Header.header * string list type overlay = Document_ID.command * (string * string list) datatype node_edit = @@ -38,17 +37,6 @@ -(** global keywords **) - -val global_keywords = Synchronized.var "global_keywords" Keyword.empty_keywords; - -fun init_keywords () = - Synchronized.change global_keywords - (fn _ => - fold (curry Keyword.merge_keywords o Thy_Header.get_keywords o Thy_Info.get_theory) - (Thy_Info.get_names ()) Keyword.empty_keywords); - -fun get_keywords () = Synchronized.value global_keywords; @@ -69,17 +57,19 @@ abstype node = Node of {header: node_header, (*master directory, theory header, errors*) + keywords: Keyword.keywords option, (*outer syntax keywords*) perspective: perspective, (*command perspective*) entries: Command.exec option Entries.T, (*command entries with excecutions*) result: Command.eval option} (*result of last execution*) and version = Version of node String_Graph.T (*development graph wrt. static imports*) with -fun make_node (header, perspective, entries, result) = - Node {header = header, perspective = perspective, entries = entries, result = result}; +fun make_node (header, keywords, perspective, entries, result) = + Node {header = header, keywords = keywords, perspective = perspective, + entries = entries, result = result}; -fun map_node f (Node {header, perspective, entries, result}) = - make_node (f (header, perspective, entries, result)); +fun map_node f (Node {header, keywords, perspective, entries, result}) = + make_node (f (header, keywords, perspective, entries, result)); fun make_perspective (required, command_ids, overlays) : perspective = {required = required, @@ -90,7 +80,7 @@ val no_header: node_header = ("", Thy_Header.make ("", Position.none) [] [], []); val no_perspective = make_perspective (false, [], []); -val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE); +val empty_node = make_node (no_header, NONE, no_perspective, Entries.empty, NONE); fun is_no_perspective ({required, visible, visible_last, overlays}: perspective) = not required andalso @@ -98,8 +88,9 @@ is_none visible_last andalso Inttab.is_empty overlays; -fun is_empty_node (Node {header, perspective, entries, result}) = +fun is_empty_node (Node {header, keywords, perspective, entries, result}) = header = no_header andalso + is_none keywords andalso is_no_perspective perspective andalso Entries.is_empty entries andalso is_none result; @@ -113,12 +104,21 @@ | _ => Path.current); fun set_header header = - map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result)); + map_node (fn (_, keywords, perspective, entries, result) => + (header, keywords, perspective, entries, result)); + +fun get_header_raw (Node {header, ...}) = header; fun get_header (Node {header = (master, header, errors), ...}) = if null errors then (master, header) else error (cat_lines errors); +fun set_keywords keywords = + map_node (fn (header, _, perspective, entries, result) => + (header, keywords, perspective, entries, result)); + +fun get_keywords (Node {keywords, ...}) = keywords; + fun read_header node span = let val {name = (name, _), imports, keywords} = #2 (get_header node); @@ -126,8 +126,10 @@ in Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords end; fun get_perspective (Node {perspective, ...}) = perspective; + fun set_perspective args = - map_node (fn (header, _, entries, result) => (header, make_perspective args, entries, result)); + map_node (fn (header, keywords, _, entries, result) => + (header, keywords, make_perspective args, entries, result)); val required_node = #required o get_perspective; val visible_command = Inttab.defined o #visible o get_perspective; @@ -136,7 +138,9 @@ val overlays = Inttab.lookup_list o #overlays o get_perspective; fun map_entries f = - map_node (fn (header, perspective, entries, result) => (header, perspective, f entries, result)); + map_node (fn (header, keywords, perspective, entries, result) => + (header, keywords, perspective, f entries, result)); + fun get_entries (Node {entries, ...}) = entries; fun iterate_entries f = Entries.iterate NONE f o get_entries; @@ -146,8 +150,10 @@ | SOME id => Entries.iterate (SOME id) f entries); fun get_result (Node {result, ...}) = result; + fun set_result result = - map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result)); + map_node (fn (header, keywords, perspective, entries, _) => + (header, keywords, perspective, entries, result)); fun changed_result node node' = (case (get_result node, get_result node') of @@ -222,21 +228,43 @@ | Deps (master, header, errors) => let val imports = map fst (#imports header); - val errors1 = - (Synchronized.change global_keywords (Keyword.add_keywords (#keywords header)); errors) - handle ERROR msg => errors @ [msg]; val nodes1 = nodes |> default_node name |> fold default_node imports; val nodes2 = nodes1 |> String_Graph.Keys.fold (fn dep => String_Graph.del_edge (dep, name)) (String_Graph.imm_preds nodes1 name); - val (nodes3, errors2) = - (String_Graph.add_deps_acyclic (name, imports) nodes2, errors1) - handle String_Graph.CYCLES cs => (nodes2, errors1 @ map cycle_msg cs); - in String_Graph.map_node name (set_header (master, header, errors2)) nodes3 end + val (nodes3, errors1) = + (String_Graph.add_deps_acyclic (name, imports) nodes2, errors) + handle String_Graph.CYCLES cs => (nodes2, errors @ map cycle_msg cs); + in String_Graph.map_node name (set_header (master, header, errors1)) nodes3 end | Perspective perspective => update_node name (set_perspective perspective) nodes); +fun update_keywords name nodes = + nodes |> String_Graph.map_node name (fn node => + if is_empty_node node then node + else + let + val (master, header, errors) = get_header_raw node; + val imports_keywords = map_filter (get_keywords o get_node nodes o #1) (#imports header); + val keywords = + Library.foldl Keyword.merge_keywords (Session.get_keywords (), imports_keywords); + val (keywords', errors') = + (Keyword.add_keywords (#keywords header) keywords, errors) + handle ERROR msg => + (keywords, if member (op =) errors msg then errors else errors @ [msg]); + in + node + |> set_header (master, header, errors') + |> set_keywords (SOME keywords') + end); + +fun edit_keywords edits (Version nodes) = + Version + (fold update_keywords + (String_Graph.all_succs nodes (map_filter (fn (a, Deps _) => SOME a | _ => NONE) edits)) + nodes); + fun put_node (name, node) (Version nodes) = let val nodes1 = update_node name (K node) nodes; @@ -562,7 +590,9 @@ fun update old_version_id new_version_id edits state = Runtime.exn_trace_system (fn () => let val old_version = the_version state old_version_id; - val new_version = timeit "Document.edit_nodes" (fn () => fold edit_nodes edits old_version); + val new_version = + timeit "Document.edit_nodes" + (fn () => old_version |> fold edit_nodes edits |> edit_keywords edits); val nodes = nodes_of new_version; val required = make_required nodes; @@ -579,7 +609,7 @@ timeit ("Document.update " ^ name) (fn () => Runtime.exn_trace_system (fn () => let - val keywords = get_keywords (); + val keywords = the_default (Session.get_keywords ()) (get_keywords node); val imports = map (apsnd Future.join) deps; val imports_result_changed = exists (#4 o #1 o #2) imports; val node_required = Symtab.defined required name; diff -r 08a6901eb035 -r 94b2690ad494 src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Wed Dec 03 20:45:20 2014 +0100 +++ b/src/Pure/PIDE/protocol.ML Wed Dec 03 22:34:28 2014 +0100 @@ -23,10 +23,6 @@ end); val _ = - Isabelle_Process.protocol_command "Document.init_keywords" - (fn [] => Document.init_keywords ()); - -val _ = Isabelle_Process.protocol_command "Document.define_blob" (fn [digest, content] => Document.change_state (Document.define_blob digest content)); diff -r 08a6901eb035 -r 94b2690ad494 src/Pure/PIDE/session.ML --- a/src/Pure/PIDE/session.ML Wed Dec 03 20:45:20 2014 +0100 +++ b/src/Pure/PIDE/session.ML Wed Dec 03 22:34:28 2014 +0100 @@ -8,6 +8,7 @@ sig val name: unit -> string val welcome: unit -> string + val get_keywords: unit -> Keyword.keywords val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list -> (Path.T * Path.T) list -> string -> string * string -> bool -> unit val finish: unit -> unit @@ -31,6 +32,12 @@ else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")"; +(* base syntax *) + +val keywords = Unsynchronized.ref Keyword.empty_keywords; +fun get_keywords () = ! keywords; + + (* init *) fun init build info info_path doc doc_graph doc_output doc_variants doc_files @@ -57,6 +64,9 @@ Future.shutdown (); Event_Timer.shutdown (); Future.shutdown (); + keywords := + fold (curry Keyword.merge_keywords o Thy_Header.get_keywords o Thy_Info.get_theory) + (Thy_Info.get_names ()) Keyword.empty_keywords; session_finished := true); diff -r 08a6901eb035 -r 94b2690ad494 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Wed Dec 03 20:45:20 2014 +0100 +++ b/src/Pure/PIDE/session.scala Wed Dec 03 22:34:28 2014 +0100 @@ -611,7 +611,6 @@ def init_options(options: Options) { update_options(options) - protocol_command("Document.init_keywords") } def dialog_result(id: Document_ID.Generic, serial: Long, result: String) diff -r 08a6901eb035 -r 94b2690ad494 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Dec 03 20:45:20 2014 +0100 +++ b/src/Pure/ROOT.ML Wed Dec 03 22:34:28 2014 +0100 @@ -315,6 +315,7 @@ use "PIDE/query_operation.ML"; use "PIDE/resources.ML"; use "Thy/thy_info.ML"; +use "PIDE/session.ML"; use "PIDE/document.ML"; (*theory and proof operations*) @@ -325,7 +326,6 @@ (* Isabelle/Isar system *) -use "PIDE/session.ML"; use "System/command_line.ML"; use "System/system_channel.ML"; use "System/message_channel.ML"; diff -r 08a6901eb035 -r 94b2690ad494 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Wed Dec 03 20:45:20 2014 +0100 +++ b/src/Pure/Thy/thy_syntax.scala Wed Dec 03 22:34:28 2014 +0100 @@ -97,8 +97,9 @@ val syntax = if (node.is_empty) None else { - val imports_syntax = node.header.imports.flatMap(a => nodes(a).syntax) - Some((resources.base_syntax /: imports_syntax)(_ ++ _).add_keywords(node.header.keywords)) + val header = node.header + val imports_syntax = header.imports.flatMap(a => nodes(a).syntax) + Some((resources.base_syntax /: imports_syntax)(_ ++ _).add_keywords(header.keywords)) } nodes += (name -> node.update_syntax(syntax)) }