src/Pure/PIDE/document.ML
changeset 47630 8d654975b67d
parent 47628 3275758d274e
child 47631 97d28302445c
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Apr 20 20:29:44 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Apr 20 22:51:06 2012 +0200
     1.3 @@ -400,24 +400,26 @@
     1.4              NONE => true
     1.5            | SOME id => not (Keyword.is_theory_begin (#1 (the_command state id))));
     1.6        in (visible', initial') end;
     1.7 -    fun get_common ((prev, id), opt_exec) (found, (_, flags)) =
     1.8 -      if found then NONE
     1.9 -      else
    1.10 -        let val found' =
    1.11 -          (case opt_exec of
    1.12 -            NONE => true
    1.13 -          | SOME (exec_id, exec) =>
    1.14 -              (case lookup_entry node0 id of
    1.15 -                NONE => true
    1.16 -              | SOME (exec_id0, _) => exec_id <> exec_id0) orelse not (stable_command exec));
    1.17 -        in SOME (found', (prev, update_flags prev flags)) end;
    1.18 -    val (found, (common, flags)) =
    1.19 -      iterate_entries get_common node (false, (NONE, (true, true)));
    1.20 +    fun get_common ((prev, id), opt_exec) (same, (_, flags)) =
    1.21 +      if same then
    1.22 +        let
    1.23 +          val flags' = update_flags prev flags;
    1.24 +          val same' =
    1.25 +            (case opt_exec of
    1.26 +              NONE => false
    1.27 +            | SOME (exec_id, exec) =>
    1.28 +                (case lookup_entry node0 id of
    1.29 +                  NONE => false
    1.30 +                | SOME (exec_id0, _) => exec_id = exec_id0 andalso stable_command exec));
    1.31 +        in SOME (same', (prev, flags')) end
    1.32 +      else NONE;
    1.33 +    val (same, (common, flags)) =
    1.34 +      iterate_entries get_common node (true, (NONE, (true, true)));
    1.35    in
    1.36 -    if found then (common, flags)
    1.37 -    else
    1.38 +    if same then
    1.39        let val last = Entries.get_after (get_entries node) common
    1.40        in (last, update_flags last flags) end
    1.41 +    else (common, flags)
    1.42    end;
    1.43  
    1.44  fun illegal_init () = error "Illegal theory header after end of theory";