# HG changeset patch
# User wenzelm
# Date 1372881315 -7200
# Node ID 8dd8ab81f1d7d9c6a1ad98d6f5bdeface7a8a67e
# Parent  04210c1bcb90f3ff0c381097d76969f17f217835
tuned;

diff -r 04210c1bcb90 -r 8dd8ab81f1d7 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Jul 03 21:38:10 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Jul 03 21:55:15 2013 +0200
@@ -437,13 +437,12 @@
     else (common, flags)
   end;
 
-fun illegal_init _ = error "Illegal theory header after end of theory";
-
 fun new_exec state proper_init command_id' (execs, command_exec, init) =
   if not proper_init andalso is_none init then NONE
   else
     let
       val (name, span) = the_command state command_id' ||> Lazy.force;
+      fun illegal_init _ = error "Illegal theory header after end of theory";
       val (modify_init, init') =
         if Keyword.is_theory_begin name then
           (Toplevel.modify_init (fn () => the_default illegal_init init span), NONE)
@@ -488,7 +487,7 @@
               let
                 val imports = map (apsnd Future.join) deps;
                 val updated_imports = exists (is_some o #3 o #1 o #2) imports;
-                val required = is_required name;
+                val node_required = is_required name;
               in
                 if updated_imports orelse AList.defined (op =) edits name orelse
                   not (stable_entries node) orelse not (finished_theory node)
@@ -501,17 +500,17 @@
                       forall (fn (name, (_, node)) => check_theory true name node) imports;
 
                     val last_visible = visible_last node;
-                    val (common, (visible, initial)) =
+                    val (common, (still_visible, initial)) =
                       if updated_imports then (NONE, (true, true))
                       else last_common state last_visible node0 node;
                     val common_command_exec = the_default_entry node common;
 
                     val (new_execs, (command_id', (_, exec')), _) =
                       ([], common_command_exec, if initial then SOME init else NONE) |>
-                      (visible orelse required) ?
+                      (still_visible orelse node_required) ?
                         iterate_entries_after common
                           (fn ((prev, id), _) => fn res =>
-                            if not required andalso prev = last_visible then NONE
+                            if not node_required andalso prev = last_visible then NONE
                             else new_exec state proper_init id res) node;
 
                     val no_execs =