src/Pure/PIDE/document.ML
changeset 47347 af937661e4a1
parent 47346 cd3ab7625519
child 47388 fe4b245af74c
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Apr 06 11:49:08 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Apr 06 12:02:24 2012 +0200
     1.3 @@ -241,7 +241,7 @@
     1.4  
     1.5  
     1.6  
     1.7 -(** global state -- document structure and execution process **)
     1.8 +(** document state -- content structure and execution process **)
     1.9  
    1.10  abstype state = State of
    1.11   {versions: version Inttab.table,  (*version_id -> document content*)
    1.12 @@ -316,19 +316,18 @@
    1.13      let
    1.14        val version = the_version state version_id;
    1.15  
    1.16 +      fun run node command_id exec =
    1.17 +        let
    1.18 +          val (_, print) = Command.memo_eval exec;
    1.19 +          val _ =
    1.20 +            if visible_command node command_id
    1.21 +            then ignore (Lazy.future Future.default_params print)
    1.22 +            else ();
    1.23 +        in () end;
    1.24 +
    1.25        val group = Future.new_group NONE;
    1.26        val running = Unsynchronized.ref true;
    1.27  
    1.28 -      fun run _ _ NONE = ()
    1.29 -        | run node command_id (SOME (_, exec)) =
    1.30 -            let
    1.31 -              val (_, print) = Command.memo_eval exec;
    1.32 -              val _ =
    1.33 -                if visible_command node command_id
    1.34 -                then ignore (Lazy.future Future.default_params print)
    1.35 -                else ();
    1.36 -            in () end;
    1.37 -
    1.38        val _ =
    1.39          nodes_of version |> Graph.schedule
    1.40            (fn deps => fn (name, node) =>
    1.41 @@ -339,8 +338,10 @@
    1.42                  {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
    1.43                    deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
    1.44                  (fn () =>
    1.45 -                  iterate_entries (fn ((_, id), exec) => fn () =>
    1.46 -                    if ! running then SOME (run node id exec) else NONE) node ()));
    1.47 +                  iterate_entries (fn ((_, id), opt_exec) => fn () =>
    1.48 +                    (case opt_exec of
    1.49 +                      SOME (_, exec) => if ! running then SOME (run node id exec) else NONE
    1.50 +                    | NONE => NONE)) node ()));
    1.51  
    1.52      in (versions, commands, (version_id, group, running)) end);
    1.53