scheduling/next_task: PrintMode.closure;
authorwenzelm
Thu Dec 20 21:12:03 2007 +0100 (2007-12-20 ago)
changeset 2573668834086f910
parent 25735 4d147263f71f
child 25737 84c92fc48e36
scheduling/next_task: PrintMode.closure;
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Thy/thy_info.ML	Thu Dec 20 21:12:02 2007 +0100
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Thu Dec 20 21:12:03 2007 +0100
     1.3 @@ -365,7 +365,8 @@
     1.4        (case fold max_task tasks NONE of
     1.5          NONE => (Multithreading.Wait, G)
     1.6        | SOME (name, (body, _)) =>
     1.7 -         (Multithreading.Task {body = body, cont = Graph.del_nodes [name], fail = K Graph.empty},
     1.8 +         (Multithreading.Task {body = PrintMode.closure body,
     1.9 +           cont = Graph.del_nodes [name], fail = K Graph.empty},
    1.10            Graph.map_node name (K Running) G))
    1.11    end;
    1.12