# HG changeset patch # User wenzelm # Date 1333706544 -7200 # Node ID af937661e4a1ac9b40c66a38f78dbf6b2d159520 # Parent cd3ab7625519bd3406071f80647a2ba188460408 stop node execution at first unassigned exec; diff -r cd3ab7625519 -r af937661e4a1 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Fri Apr 06 11:49:08 2012 +0200 +++ b/src/Pure/PIDE/document.ML Fri Apr 06 12:02:24 2012 +0200 @@ -241,7 +241,7 @@ -(** global state -- document structure and execution process **) +(** document state -- content structure and execution process **) abstype state = State of {versions: version Inttab.table, (*version_id -> document content*) @@ -316,19 +316,18 @@ let val version = the_version state version_id; + fun run node command_id exec = + let + val (_, print) = Command.memo_eval exec; + val _ = + if visible_command node command_id + then ignore (Lazy.future Future.default_params print) + else (); + in () end; + val group = Future.new_group NONE; val running = Unsynchronized.ref true; - fun run _ _ NONE = () - | run node command_id (SOME (_, exec)) = - let - val (_, print) = Command.memo_eval exec; - val _ = - if visible_command node command_id - then ignore (Lazy.future Future.default_params print) - else (); - in () end; - val _ = nodes_of version |> Graph.schedule (fn deps => fn (name, node) => @@ -339,8 +338,10 @@ {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)), deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false} (fn () => - iterate_entries (fn ((_, id), exec) => fn () => - if ! running then SOME (run node id exec) else NONE) node ())); + iterate_entries (fn ((_, id), opt_exec) => fn () => + (case opt_exec of + SOME (_, exec) => if ! running then SOME (run node id exec) else NONE + | NONE => NONE)) node ())); in (versions, commands, (version_id, group, running)) end);