src/Pure/PIDE/document.ML
changeset 58923 cb9b69cca999
parent 58918 8d36bc5eaed3
child 58928 23d0ffd48006
     1.1 --- a/src/Pure/PIDE/document.ML	Thu Nov 06 15:42:34 2014 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Nov 06 15:47:04 2014 +0100
     1.3 @@ -466,7 +466,7 @@
     1.4    is_some (loaded_theory name) orelse
     1.5    can get_header node andalso (not full orelse is_some (get_result node));
     1.6  
     1.7 -fun last_common state node_required node0 node =
     1.8 +fun last_common keywords state node_required node0 node =
     1.9    let
    1.10      fun update_flags prev (visible, initial) =
    1.11        let
    1.12 @@ -474,7 +474,8 @@
    1.13          val initial' = initial andalso
    1.14            (case prev of
    1.15              NONE => true
    1.16 -          | SOME command_id => not (Keyword.is_theory_begin (the_command_name state command_id)));
    1.17 +          | SOME command_id =>
    1.18 +              not (Keyword.is_theory_begin keywords (the_command_name state command_id)));
    1.19        in (visible', initial') end;
    1.20  
    1.21      fun get_common ((prev, command_id), opt_exec) (_, ok, flags, assign_update) =
    1.22 @@ -495,7 +496,9 @@
    1.23                    val command_overlays = overlays node command_id;
    1.24                    val command_name = the_command_name state command_id;
    1.25                  in
    1.26 -                  (case Command.print command_visible command_overlays command_name eval prints of
    1.27 +                  (case
    1.28 +                    Command.print command_visible command_overlays keywords command_name eval prints
    1.29 +                   of
    1.30                      SOME prints' => assign_update_new (command_id, SOME (eval, prints'))
    1.31                    | NONE => I)
    1.32                  end
    1.33 @@ -513,7 +516,7 @@
    1.34  
    1.35  fun illegal_init _ = error "Illegal theory header after end of theory";
    1.36  
    1.37 -fun new_exec state node proper_init command_id' (assign_update, command_exec, init) =
    1.38 +fun new_exec keywords state node proper_init command_id' (assign_update, command_exec, init) =
    1.39    if not proper_init andalso is_none init then NONE
    1.40    else
    1.41      let
    1.42 @@ -526,13 +529,14 @@
    1.43        val span = Lazy.force span0;
    1.44  
    1.45        val eval' =
    1.46 -        Command.eval (fn () => the_default illegal_init init span)
    1.47 -          (master_directory node) blobs span eval;
    1.48 -      val prints' = perhaps (Command.print command_visible command_overlays command_name eval') [];
    1.49 +        Command.eval keywords (master_directory node)
    1.50 +          (fn () => the_default illegal_init init span) blobs span eval;
    1.51 +      val prints' =
    1.52 +        perhaps (Command.print command_visible command_overlays keywords command_name eval') [];
    1.53        val exec' = (eval', prints');
    1.54  
    1.55        val assign_update' = assign_update_new (command_id', SOME exec') assign_update;
    1.56 -      val init' = if Keyword.is_theory_begin command_name then NONE else init;
    1.57 +      val init' = if Keyword.is_theory_begin keywords command_name then NONE else init;
    1.58      in SOME (assign_update', (command_id', (eval', prints')), init') end;
    1.59  
    1.60  fun removed_execs node0 (command_id, exec_ids) =
    1.61 @@ -558,6 +562,7 @@
    1.62                deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
    1.63              (fn () => timeit ("Document.update " ^ name) (fn () =>
    1.64                let
    1.65 +                val keywords = Keyword.get_keywords ();
    1.66                  val imports = map (apsnd Future.join) deps;
    1.67                  val imports_result_changed = exists (#4 o #1 o #2) imports;
    1.68                  val node_required = Symtab.defined required name;
    1.69 @@ -574,7 +579,7 @@
    1.70  
    1.71                      val (print_execs, common, (still_visible, initial)) =
    1.72                        if imports_result_changed then (assign_update_empty, NONE, (true, true))
    1.73 -                      else last_common state node_required node0 node;
    1.74 +                      else last_common keywords state node_required node0 node;
    1.75                      val common_command_exec = the_default_entry node common;
    1.76  
    1.77                      val (updated_execs, (command_id', (eval', _)), _) =
    1.78 @@ -583,7 +588,7 @@
    1.79                          iterate_entries_after common
    1.80                            (fn ((prev, id), _) => fn res =>
    1.81                              if not node_required andalso prev = visible_last node then NONE
    1.82 -                            else new_exec state node proper_init id res) node;
    1.83 +                            else new_exec keywords state node proper_init id res) node;
    1.84  
    1.85                      val assigned_execs =
    1.86                        (node0, updated_execs) |-> iterate_entries_after common