src/Pure/PIDE/document.ML
changeset 59735 24bee1b11fce
parent 59716 8c56b34a88b0
child 59934 b65c4370f831
     1.1 --- a/src/Pure/PIDE/document.ML	Tue Mar 17 09:22:21 2015 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Tue Mar 17 15:21:41 2015 +0100
     1.3 @@ -552,8 +552,7 @@
     1.4          val initial' = initial andalso
     1.5            (case prev of
     1.6              NONE => true
     1.7 -          | SOME command_id =>
     1.8 -              not (Keyword.is_theory_begin keywords (the_command_name state command_id)));
     1.9 +          | SOME command_id => the_command_name state command_id <> Thy_Header.theoryN);
    1.10        in (visible', initial') end;
    1.11  
    1.12      fun get_common ((prev, command_id), opt_exec) (_, ok, flags, assign_update) =
    1.13 @@ -614,7 +613,7 @@
    1.14        val exec' = (eval', prints');
    1.15  
    1.16        val assign_update' = assign_update_new (command_id', SOME exec') assign_update;
    1.17 -      val init' = if Keyword.is_theory_begin keywords command_name then NONE else init;
    1.18 +      val init' = if command_name = Thy_Header.theoryN then NONE else init;
    1.19      in SOME (assign_update', (command_id', (eval', prints')), init') end;
    1.20  
    1.21  fun removed_execs node0 (command_id, exec_ids) =