src/Pure/PIDE/document.ML
changeset 66367 b60afdf1177d
parent 66167 1bd268ab885c
child 66369 d003b44674c1
     1.1 --- a/src/Pure/PIDE/document.ML	Sun Aug 06 22:54:17 2017 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon Aug 07 11:20:19 2017 +0200
     1.3 @@ -607,8 +607,6 @@
     1.4    if not proper_init andalso is_none init then NONE
     1.5    else
     1.6      let
     1.7 -      val (_, (eval, _)) = command_exec;
     1.8 -
     1.9        val command_visible = visible_command node command_id';
    1.10        val command_overlays = overlays node command_id';
    1.11        val (command_name, blob_digests, blobs_index, span0) = the_command state command_id';
    1.12 @@ -616,15 +614,15 @@
    1.13        val span = Lazy.force span0;
    1.14  
    1.15        val eval' =
    1.16 -        Command.eval keywords (master_directory node)
    1.17 -          (fn () => the_default illegal_init init span) (blobs, blobs_index) span eval;
    1.18 +        Command.eval keywords (master_directory node) (fn () => the_default illegal_init init span)
    1.19 +          (blobs, blobs_index) span (#1 (#2 command_exec));
    1.20        val prints' =
    1.21          perhaps (Command.print command_visible command_overlays keywords command_name eval') [];
    1.22        val exec' = (eval', prints');
    1.23  
    1.24        val assign_update' = assign_update_new (command_id', SOME exec') assign_update;
    1.25        val init' = if command_name = Thy_Header.theoryN then NONE else init;
    1.26 -    in SOME (assign_update', (command_id', (eval', prints')), init') end;
    1.27 +    in SOME (assign_update', (command_id', exec'), init') end;
    1.28  
    1.29  fun removed_execs node0 (command_id, exec_ids) =
    1.30    subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id));
    1.31 @@ -679,7 +677,7 @@
    1.32                              SOME id => (id, the_default Command.no_exec (the_entry node id))
    1.33                            | NONE => (Document_ID.none, Command.init_exec ml_root));
    1.34  
    1.35 -                        val (updated_execs, (command_id', (eval', _)), _) =
    1.36 +                        val (updated_execs, (command_id', exec'), _) =
    1.37                            (print_execs, common_command_exec, if initial then SOME init else NONE)
    1.38                            |> (still_visible orelse node_required) ?
    1.39                              iterate_entries_after common
    1.40 @@ -698,7 +696,7 @@
    1.41                            if command_id' = Document_ID.none then NONE else SOME command_id';
    1.42                          val result =
    1.43                            if is_none last_exec orelse is_some (after_entry node last_exec) then NONE
    1.44 -                          else SOME eval';
    1.45 +                          else SOME (#1 exec');
    1.46  
    1.47                          val assign_update = assign_update_result assigned_execs;
    1.48                          val removed = maps (removed_execs node0) assign_update;