src/Pure/PIDE/document.ML
changeset 52775 e0169f13bd37
parent 52774 627fb639a2d9
child 52776 fd81d51460b7
     1.1 --- a/src/Pure/PIDE/document.ML	Mon Jul 29 16:52:04 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon Jul 29 18:59:58 2013 +0200
     1.3 @@ -303,19 +303,20 @@
     1.4              if visible_node node orelse pending_result node then
     1.5                let
     1.6                  val former_task = Symtab.lookup frontier name;
     1.7 +                fun body () =
     1.8 +                  iterate_entries (fn (_, opt_exec) => fn () =>
     1.9 +                    (case opt_exec of
    1.10 +                      SOME exec =>
    1.11 +                        if Execution.is_running execution_id
    1.12 +                        then SOME (Command.exec execution_id exec)
    1.13 +                        else NONE
    1.14 +                    | NONE => NONE)) node ()
    1.15 +                  handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn;
    1.16                  val future =
    1.17                    (singleton o Future.forks)
    1.18                      {name = "theory:" ^ name, group = SOME (Future.new_group NONE),
    1.19                        deps = the_list former_task @ map #2 (maps #2 deps),
    1.20 -                      pri = pri, interrupts = false}
    1.21 -                    (fn () =>
    1.22 -                      iterate_entries (fn (_, opt_exec) => fn () =>
    1.23 -                        (case opt_exec of
    1.24 -                          SOME exec =>
    1.25 -                            if Execution.is_running execution_id
    1.26 -                            then SOME (Command.exec execution_id exec)
    1.27 -                            else NONE
    1.28 -                        | NONE => NONE)) node ());
    1.29 +                      pri = pri, interrupts = false} body;
    1.30                in [(name, Future.task_of future)] end
    1.31              else [])
    1.32        else [];