# HG changeset patch
# User wenzelm
# Date 1198181523 -3600
# Node ID 68834086f910c63bce47b0d3732fec27606a82b0
# Parent  4d147263f71fcc9b456d4fab9e0762a9031d8ff5
scheduling/next_task: PrintMode.closure;

diff -r 4d147263f71f -r 68834086f910 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Thu Dec 20 21:12:02 2007 +0100
+++ b/src/Pure/Thy/thy_info.ML	Thu Dec 20 21:12:03 2007 +0100
@@ -365,7 +365,8 @@
       (case fold max_task tasks NONE of
         NONE => (Multithreading.Wait, G)
       | SOME (name, (body, _)) =>
-         (Multithreading.Task {body = body, cont = Graph.del_nodes [name], fail = K Graph.empty},
+         (Multithreading.Task {body = PrintMode.closure body,
+           cont = Graph.del_nodes [name], fail = K Graph.empty},
           Graph.map_node name (K Running) G))
   end;