src/Pure/PIDE/document.ML
changeset 52605 a2a805549c74
parent 52604 ff2f0818aebc
child 52606 0d68d108d7e0
     1.1 --- a/src/Pure/PIDE/document.ML	Thu Jul 11 23:24:40 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Jul 12 11:07:02 2013 +0200
     1.3 @@ -205,10 +205,10 @@
     1.4  
     1.5  (** main state -- document structure and execution process **)
     1.6  
     1.7 -type execution = {version_id: Document_ID.version, context: Exec.context};
     1.8 +type execution = {version_id: Document_ID.version, context: Execution.context};
     1.9  
    1.10 -val no_execution = {version_id = Document_ID.none, context = Exec.no_context};
    1.11 -fun make_execution version_id = {version_id = version_id, context = Exec.fresh_context ()};
    1.12 +val no_execution = {version_id = Document_ID.none, context = Execution.no_context};
    1.13 +fun make_execution version_id = {version_id = version_id, context = Execution.fresh_context ()};
    1.14  
    1.15  abstype state = State of
    1.16   {versions: version Inttab.table,  (*version id -> document content*)
    1.17 @@ -297,16 +297,16 @@
    1.18  (* document execution *)
    1.19  
    1.20  fun discontinue_execution state =
    1.21 -  Exec.drop_context (#context (execution_of state));
    1.22 +  Execution.drop_context (#context (execution_of state));
    1.23  
    1.24  fun cancel_execution state =
    1.25 -  (Exec.drop_context (#context (execution_of state)); Exec.terminate_all ());
    1.26 +  (Execution.drop_context (#context (execution_of state)); Execution.terminate_all ());
    1.27  
    1.28  fun start_execution state =
    1.29    let
    1.30      val {version_id, context} = execution_of state;
    1.31      val _ =
    1.32 -      if Exec.is_running context then
    1.33 +      if Execution.is_running context then
    1.34          nodes_of (the_version state version_id) |> String_Graph.schedule
    1.35            (fn deps => fn (name, node) =>
    1.36              if not (visible_node node) andalso finished_theory node then
    1.37 @@ -319,7 +319,7 @@
    1.38                    iterate_entries (fn (_, opt_exec) => fn () =>
    1.39                      (case opt_exec of
    1.40                        SOME exec =>
    1.41 -                        if Exec.is_running context then SOME (Command.exec context exec)
    1.42 +                        if Execution.is_running context then SOME (Command.exec context exec)
    1.43                          else NONE
    1.44                      | NONE => NONE)) node ()))
    1.45        else [];
    1.46 @@ -452,7 +452,7 @@
    1.47  
    1.48  fun cancel_old_execs node0 (command_id, exec_ids) =
    1.49    subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id))
    1.50 -  |> map_filter (Exec.peek_running #> Option.map (tap Future.cancel_group));
    1.51 +  |> map_filter (Execution.peek_running #> Option.map (tap Future.cancel_group));
    1.52  
    1.53  in
    1.54