tuned;
authorwenzelm
Wed Jul 03 21:55:15 2013 +0200 (2013-07-03 ago)
changeset 525148dd8ab81f1d7
parent 52513 04210c1bcb90
child 52515 0dcadc90550b
tuned;
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/PIDE/document.ML	Wed Jul 03 21:38:10 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Wed Jul 03 21:55:15 2013 +0200
     1.3 @@ -437,13 +437,12 @@
     1.4      else (common, flags)
     1.5    end;
     1.6  
     1.7 -fun illegal_init _ = error "Illegal theory header after end of theory";
     1.8 -
     1.9  fun new_exec state proper_init command_id' (execs, command_exec, init) =
    1.10    if not proper_init andalso is_none init then NONE
    1.11    else
    1.12      let
    1.13        val (name, span) = the_command state command_id' ||> Lazy.force;
    1.14 +      fun illegal_init _ = error "Illegal theory header after end of theory";
    1.15        val (modify_init, init') =
    1.16          if Keyword.is_theory_begin name then
    1.17            (Toplevel.modify_init (fn () => the_default illegal_init init span), NONE)
    1.18 @@ -488,7 +487,7 @@
    1.19                let
    1.20                  val imports = map (apsnd Future.join) deps;
    1.21                  val updated_imports = exists (is_some o #3 o #1 o #2) imports;
    1.22 -                val required = is_required name;
    1.23 +                val node_required = is_required name;
    1.24                in
    1.25                  if updated_imports orelse AList.defined (op =) edits name orelse
    1.26                    not (stable_entries node) orelse not (finished_theory node)
    1.27 @@ -501,17 +500,17 @@
    1.28                        forall (fn (name, (_, node)) => check_theory true name node) imports;
    1.29  
    1.30                      val last_visible = visible_last node;
    1.31 -                    val (common, (visible, initial)) =
    1.32 +                    val (common, (still_visible, initial)) =
    1.33                        if updated_imports then (NONE, (true, true))
    1.34                        else last_common state last_visible node0 node;
    1.35                      val common_command_exec = the_default_entry node common;
    1.36  
    1.37                      val (new_execs, (command_id', (_, exec')), _) =
    1.38                        ([], common_command_exec, if initial then SOME init else NONE) |>
    1.39 -                      (visible orelse required) ?
    1.40 +                      (still_visible orelse node_required) ?
    1.41                          iterate_entries_after common
    1.42                            (fn ((prev, id), _) => fn res =>
    1.43 -                            if not required andalso prev = last_visible then NONE
    1.44 +                            if not node_required andalso prev = last_visible then NONE
    1.45                              else new_exec state proper_init id res) node;
    1.46  
    1.47                      val no_execs =