less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
authorwenzelm
Thu Apr 05 14:14:51 2012 +0200 (2012-04-05 ago)
changeset 47343b8aeab386414
parent 47342 7828c7b3c143
child 47344 ca5eb90cc84a
less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
src/Pure/PIDE/document.ML
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/System/session.scala
     1.1 --- a/src/Pure/PIDE/document.ML	Thu Apr 05 13:01:54 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Apr 05 14:14:51 2012 +0200
     1.3 @@ -25,6 +25,7 @@
     1.4    type state
     1.5    val init_state: state
     1.6    val define_command: command_id -> string -> string -> state -> state
     1.7 +  val discontinue_execution: state -> unit
     1.8    val cancel_execution: state -> Future.task list
     1.9    val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
    1.10    val update: version_id -> version_id -> edit list -> state ->
    1.11 @@ -242,7 +243,7 @@
    1.12  abstype state = State of
    1.13   {versions: version Inttab.table,  (*version_id -> document content*)
    1.14    commands: (string * Token.T list lazy) Inttab.table,  (*command_id -> named span*)
    1.15 -  execution: version_id * Future.group}  (*current execution process*)
    1.16 +  execution: version_id * Future.group * bool Unsynchronized.ref}  (*current execution process*)
    1.17  with
    1.18  
    1.19  fun make_state (versions, commands, execution) =
    1.20 @@ -252,7 +253,8 @@
    1.21    make_state (f (versions, commands, execution));
    1.22  
    1.23  val init_state =
    1.24 -  make_state (Inttab.make [(no_id, empty_version)], Inttab.empty, (no_id, Future.new_group NONE));
    1.25 +  make_state (Inttab.make [(no_id, empty_version)], Inttab.empty,
    1.26 +    (no_id, Future.new_group NONE, Unsynchronized.ref false));
    1.27  
    1.28  
    1.29  (* document versions *)
    1.30 @@ -291,7 +293,9 @@
    1.31  
    1.32  (* document execution *)
    1.33  
    1.34 -fun cancel_execution (State {execution, ...}) = Future.cancel_group (#2 execution);
    1.35 +fun discontinue_execution  (State {execution = (_, _, running), ...}) = running := false;
    1.36 +
    1.37 +fun cancel_execution (State {execution = (_, group, _), ...}) = Future.cancel_group group;
    1.38  
    1.39  end;
    1.40  
    1.41 @@ -483,8 +487,11 @@
    1.42      let
    1.43        val version = the_version state version_id;
    1.44  
    1.45 -      fun force_exec _ _ NONE = ()
    1.46 -        | force_exec node command_id (SOME (_, exec)) =
    1.47 +      val group = Future.new_group NONE;
    1.48 +      val running = Unsynchronized.ref true;
    1.49 +
    1.50 +      fun run _ _ NONE = ()
    1.51 +        | run node command_id (SOME (_, exec)) =
    1.52              let
    1.53                val (_, print) = Command.memo_eval exec;
    1.54                val _ =
    1.55 @@ -493,17 +500,17 @@
    1.56                  else ();
    1.57              in () end;
    1.58  
    1.59 -      val group = Future.new_group NONE;
    1.60        val _ =
    1.61          nodes_of version |> Graph.schedule
    1.62            (fn deps => fn (name, node) =>
    1.63              (singleton o Future.forks)
    1.64                {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
    1.65                  deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
    1.66 -              (iterate_entries (fn ((_, id), exec) => fn () =>
    1.67 -                SOME (force_exec node id exec)) node));
    1.68 +              (fn () =>
    1.69 +                iterate_entries (fn ((_, id), exec) => fn () =>
    1.70 +                  if ! running then SOME (run node id exec) else NONE) node ()));
    1.71  
    1.72 -    in (versions, commands, (version_id, group)) end);
    1.73 +    in (versions, commands, (version_id, group, running)) end);
    1.74  
    1.75  
    1.76  (* remove versions *)
     2.1 --- a/src/Pure/PIDE/protocol.ML	Thu Apr 05 13:01:54 2012 +0200
     2.2 +++ b/src/Pure/PIDE/protocol.ML	Thu Apr 05 14:14:51 2012 +0200
     2.3 @@ -13,6 +13,10 @@
     2.4        Document.change_state (Document.define_command (Document.parse_id id) name text));
     2.5  
     2.6  val _ =
     2.7 +  Isabelle_Process.protocol_command "Document.discontinue_execution"
     2.8 +    (fn [] => Document.discontinue_execution (Document.state ()));
     2.9 +
    2.10 +val _ =
    2.11    Isabelle_Process.protocol_command "Document.cancel_execution"
    2.12      (fn [] => ignore (Document.cancel_execution (Document.state ())));
    2.13  
     3.1 --- a/src/Pure/PIDE/protocol.scala	Thu Apr 05 13:01:54 2012 +0200
     3.2 +++ b/src/Pure/PIDE/protocol.scala	Thu Apr 05 14:14:51 2012 +0200
     3.3 @@ -191,10 +191,9 @@
     3.4  
     3.5    /* document versions */
     3.6  
     3.7 -  def cancel_execution()
     3.8 -  {
     3.9 -    input("Document.cancel_execution")
    3.10 -  }
    3.11 +  def discontinue_execution() { input("Document.discontinue_execution") }
    3.12 +
    3.13 +  def cancel_execution() { input("Document.cancel_execution") }
    3.14  
    3.15    def update_perspective(old_id: Document.Version_ID, new_id: Document.Version_ID,
    3.16      name: Document.Node.Name, perspective: Command.Perspective)
     4.1 --- a/src/Pure/System/session.scala	Thu Apr 05 13:01:54 2012 +0200
     4.2 +++ b/src/Pure/System/session.scala	Thu Apr 05 14:14:51 2012 +0200
     4.3 @@ -296,7 +296,7 @@
     4.4      {
     4.5        val previous = global_state().history.tip.version
     4.6  
     4.7 -      prover.get.cancel_execution()
     4.8 +      prover.get.discontinue_execution()
     4.9  
    4.10        val text_edits = header_edit(name, header) :: edits.map(edit => (name, edit))
    4.11        val version = Future.promise[Document.Version]