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 {