src/Pure/PIDE/document.ML
changeset 58928 23d0ffd48006
parent 58923 cb9b69cca999
child 58934 385a4cc7426f
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Nov 07 16:22:25 2014 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Nov 07 16:36:55 2014 +0100
     1.3 @@ -8,6 +8,7 @@
     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 @@ -37,6 +38,20 @@
    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  (** document structure **)
    1.30  
    1.31  fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document_ID.print id);
    1.32 @@ -208,7 +223,7 @@
    1.33          let
    1.34            val imports = map fst (#imports header);
    1.35            val errors1 =
    1.36 -            (Thy_Header.define_keywords (#keywords header); errors)
    1.37 +            (Synchronized.change global_keywords (Keyword.add_keywords (#keywords header)); errors)
    1.38                handle ERROR msg => errors @ [msg];
    1.39            val nodes1 = nodes
    1.40              |> default_node name
    1.41 @@ -318,7 +333,7 @@
    1.42        val span =
    1.43          Lazy.lazy (fn () =>
    1.44            Position.setmp_thread_data (Position.id_only id)
    1.45 -            (fn () => Outer_Syntax.scan (Keyword.get_keywords ()) (Position.id id) text) ());
    1.46 +            (fn () => Outer_Syntax.scan (get_keywords ()) (Position.id id) text) ());
    1.47        val _ =
    1.48          Position.setmp_thread_data (Position.id_only id)
    1.49            (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
    1.50 @@ -529,7 +544,7 @@
    1.51        val span = Lazy.force span0;
    1.52  
    1.53        val eval' =
    1.54 -        Command.eval keywords (master_directory node)
    1.55 +        Command.eval (master_directory node)
    1.56            (fn () => the_default illegal_init init span) blobs span eval;
    1.57        val prints' =
    1.58          perhaps (Command.print command_visible command_overlays keywords command_name eval') [];
    1.59 @@ -562,7 +577,7 @@
    1.60                deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
    1.61              (fn () => timeit ("Document.update " ^ name) (fn () =>
    1.62                let
    1.63 -                val keywords = Keyword.get_keywords ();
    1.64 +                val keywords = get_keywords ();
    1.65                  val imports = map (apsnd Future.join) deps;
    1.66                  val imports_result_changed = exists (#4 o #1 o #2) imports;
    1.67                  val node_required = Symtab.defined required name;