src/Pure/Syntax/syntax.ML
changeset 44113 0baa8bbd355a
parent 44069 d7c7ec248ef0
child 44802 65c397cc44ec
--- a/src/Pure/Syntax/syntax.ML	Wed Aug 10 15:17:24 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Wed Aug 10 16:05:14 2011 +0200
@@ -489,7 +489,7 @@
 fun future_gram deps e =
   singleton
     (Future.cond_forks {name = "Syntax.gram", group = NONE,
-      deps = map Future.task_of deps, pri = 0}) e;
+      deps = map Future.task_of deps, pri = 0, interrupts = true}) e;
 
 datatype syntax =
   Syntax of {