document update at high priority -- important;
authorwenzelm
Sat Jul 20 16:29:06 2013 +0200 (2013-07-20)
changeset 52716ecb46f11c366
parent 52715 8979d830950b
child 52717 da7bf8b3d24a
document update at high priority -- important;
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/PIDE/document.ML	Sat Jul 20 16:27:55 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sat Jul 20 16:29:06 2013 +0200
     1.3 @@ -463,7 +463,7 @@
     1.4          (fn deps => fn (name, node) =>
     1.5            (singleton o Future.forks)
     1.6              {name = "Document.update", group = NONE,
     1.7 -              deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false}
     1.8 +              deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
     1.9              (fn () =>
    1.10                let
    1.11                  val imports = map (apsnd Future.join) deps;