src/Pure/PIDE/document.ML
changeset 52606 0d68d108d7e0
parent 52605 a2a805549c74
child 52607 33a133d50616
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Jul 12 11:07:02 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Jul 12 11:28:03 2013 +0200
     1.3 @@ -18,8 +18,6 @@
     1.4    val init_state: state
     1.5    val define_command: Document_ID.command -> string -> string -> state -> state
     1.6    val remove_versions: Document_ID.version list -> state -> state
     1.7 -  val discontinue_execution: state -> unit
     1.8 -  val cancel_execution: state -> unit
     1.9    val start_execution: state -> unit
    1.10    val timing: bool Unsynchronized.ref
    1.11    val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
    1.12 @@ -205,10 +203,10 @@
    1.13  
    1.14  (** main state -- document structure and execution process **)
    1.15  
    1.16 -type execution = {version_id: Document_ID.version, context: Execution.context};
    1.17 +type execution = {version_id: Document_ID.version, execution_id: Document_ID.execution};
    1.18  
    1.19 -val no_execution = {version_id = Document_ID.none, context = Execution.no_context};
    1.20 -fun make_execution version_id = {version_id = version_id, context = Execution.fresh_context ()};
    1.21 +val no_execution = {version_id = Document_ID.none, execution_id = Document_ID.none};
    1.22 +fun next_execution version_id = {version_id = version_id, execution_id = Execution.start ()};
    1.23  
    1.24  abstype state = State of
    1.25   {versions: version Inttab.table,  (*version id -> document content*)
    1.26 @@ -235,7 +233,7 @@
    1.27      let
    1.28        val versions' = Inttab.update_new (version_id, version) versions
    1.29          handle Inttab.DUP dup => err_dup "document version" dup;
    1.30 -      val execution' = make_execution version_id;
    1.31 +      val execution' = next_execution version_id;
    1.32      in (versions', commands, execution') end);
    1.33  
    1.34  fun the_version (State {versions, ...}) version_id =
    1.35 @@ -296,17 +294,11 @@
    1.36  
    1.37  (* document execution *)
    1.38  
    1.39 -fun discontinue_execution state =
    1.40 -  Execution.drop_context (#context (execution_of state));
    1.41 -
    1.42 -fun cancel_execution state =
    1.43 -  (Execution.drop_context (#context (execution_of state)); Execution.terminate_all ());
    1.44 -
    1.45  fun start_execution state =
    1.46    let
    1.47 -    val {version_id, context} = execution_of state;
    1.48 +    val {version_id, execution_id} = execution_of state;
    1.49      val _ =
    1.50 -      if Execution.is_running context then
    1.51 +      if Execution.is_running execution_id then
    1.52          nodes_of (the_version state version_id) |> String_Graph.schedule
    1.53            (fn deps => fn (name, node) =>
    1.54              if not (visible_node node) andalso finished_theory node then
    1.55 @@ -319,7 +311,8 @@
    1.56                    iterate_entries (fn (_, opt_exec) => fn () =>
    1.57                      (case opt_exec of
    1.58                        SOME exec =>
    1.59 -                        if Execution.is_running context then SOME (Command.exec context exec)
    1.60 +                        if Execution.is_running execution_id
    1.61 +                        then SOME (Command.exec execution_id exec)
    1.62                          else NONE
    1.63                      | NONE => NONE)) node ()))
    1.64        else [];