maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
authorwenzelm
Tue Aug 08 22:13:05 2017 +0200 (22 months ago)
changeset 663796392766f3c25
parent 66378 53a6c5d4d03e
child 66380 96ff0eb8294a
maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
etc/options
src/Pure/PIDE/command.ML
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.ML
src/Pure/PIDE/document.scala
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/session.scala
     1.1 --- a/etc/options	Tue Aug 08 12:21:29 2017 +0200
     1.2 +++ b/etc/options	Tue Aug 08 22:13:05 2017 +0200
     1.3 @@ -155,6 +155,9 @@
     1.4  public option editor_output_delay : real = 0.1
     1.5    -- "delay for prover output (markup, common messages etc.)"
     1.6  
     1.7 +public option editor_consolidate_delay : real = 1.0
     1.8 +  -- "delay to consolidate status of command evaluation (execution forks)"
     1.9 +
    1.10  public option editor_prune_delay : real = 15
    1.11    -- "delay to prune history (delete old versions)"
    1.12  
     2.1 --- a/src/Pure/PIDE/command.ML	Tue Aug 08 12:21:29 2017 +0200
     2.2 +++ b/src/Pure/PIDE/command.ML	Tue Aug 08 22:13:05 2017 +0200
     2.3 @@ -12,6 +12,7 @@
     2.4    val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) ->
     2.5      blob list * int -> Token.T list -> Toplevel.transition
     2.6    type eval
     2.7 +  val eval_exec_id: eval -> Document_ID.exec
     2.8    val eval_eq: eval * eval -> bool
     2.9    val eval_running: eval -> bool
    2.10    val eval_finished: eval -> bool
     3.1 --- a/src/Pure/PIDE/command.scala	Tue Aug 08 12:21:29 2017 +0200
     3.2 +++ b/src/Pure/PIDE/command.scala	Tue Aug 08 22:13:05 2017 +0200
     3.3 @@ -213,6 +213,9 @@
     3.4      results: Results = Results.empty,
     3.5      markups: Markups = Markups.empty)
     3.6    {
     3.7 +    lazy val consolidated: Boolean =
     3.8 +      status.exists(markup => markup.name == Markup.CONSOLIDATED)
     3.9 +
    3.10      lazy val protocol_status: Protocol.Status =
    3.11      {
    3.12        val warnings =
     4.1 --- a/src/Pure/PIDE/document.ML	Tue Aug 08 12:21:29 2017 +0200
     4.2 +++ b/src/Pure/PIDE/document.ML	Tue Aug 08 22:13:05 2017 +0200
     4.3 @@ -24,6 +24,7 @@
     4.4    val command_exec: state -> string -> Document_ID.command -> Command.exec option
     4.5    val remove_versions: Document_ID.version list -> state -> state
     4.6    val start_execution: state -> state
     4.7 +  val consolidate_execution: state -> unit
     4.8    val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
     4.9      Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
    4.10    val state: unit -> state
    4.11 @@ -59,16 +60,17 @@
    4.12    keywords: Keyword.keywords option,  (*outer syntax keywords*)
    4.13    perspective: perspective,  (*command perspective*)
    4.14    entries: Command.exec option Entries.T,  (*command entries with executions*)
    4.15 -  result: Command.eval option}  (*result of last execution*)
    4.16 +  result: Command.eval option,  (*result of last execution*)
    4.17 +  consolidated: unit lazy}  (*consolidation status of eval forks*)
    4.18  and version = Version of node String_Graph.T  (*development graph wrt. static imports*)
    4.19  with
    4.20  
    4.21 -fun make_node (header, keywords, perspective, entries, result) =
    4.22 +fun make_node (header, keywords, perspective, entries, result, consolidated) =
    4.23    Node {header = header, keywords = keywords, perspective = perspective,
    4.24 -    entries = entries, result = result};
    4.25 +    entries = entries, result = result, consolidated = consolidated};
    4.26  
    4.27 -fun map_node f (Node {header, keywords, perspective, entries, result}) =
    4.28 -  make_node (f (header, keywords, perspective, entries, result));
    4.29 +fun map_node f (Node {header, keywords, perspective, entries, result, consolidated}) =
    4.30 +  make_node (f (header, keywords, perspective, entries, result, consolidated));
    4.31  
    4.32  fun make_perspective (required, command_ids, overlays) : perspective =
    4.33   {required = required,
    4.34 @@ -80,7 +82,7 @@
    4.35    {master = "", header = Thy_Header.make ("", Position.none) [] [], errors = []};
    4.36  val no_perspective = make_perspective (false, [], []);
    4.37  
    4.38 -val empty_node = make_node (no_header, NONE, no_perspective, Entries.empty, NONE);
    4.39 +val empty_node = make_node (no_header, NONE, no_perspective, Entries.empty, NONE, Lazy.value ());
    4.40  
    4.41  fun is_no_perspective ({required, visible, visible_last, overlays}: perspective) =
    4.42    not required andalso
    4.43 @@ -88,12 +90,13 @@
    4.44    is_none visible_last andalso
    4.45    Inttab.is_empty overlays;
    4.46  
    4.47 -fun is_empty_node (Node {header, keywords, perspective, entries, result}) =
    4.48 +fun is_empty_node (Node {header, keywords, perspective, entries, result, consolidated}) =
    4.49    header = no_header andalso
    4.50    is_none keywords andalso
    4.51    is_no_perspective perspective andalso
    4.52    Entries.is_empty entries andalso
    4.53 -  is_none result;
    4.54 +  is_none result andalso
    4.55 +  Lazy.is_finished consolidated;
    4.56  
    4.57  
    4.58  (* basic components *)
    4.59 @@ -104,14 +107,15 @@
    4.60    | _ => Path.current);
    4.61  
    4.62  fun set_header master header errors =
    4.63 -  map_node (fn (_, keywords, perspective, entries, result) =>
    4.64 -    ({master = master, header = header, errors = errors}, keywords, perspective, entries, result));
    4.65 +  map_node (fn (_, keywords, perspective, entries, result, consolidated) =>
    4.66 +    ({master = master, header = header, errors = errors},
    4.67 +      keywords, perspective, entries, result, consolidated));
    4.68  
    4.69  fun get_header (Node {header, ...}) = header;
    4.70  
    4.71  fun set_keywords keywords =
    4.72 -  map_node (fn (header, _, perspective, entries, result) =>
    4.73 -    (header, keywords, perspective, entries, result));
    4.74 +  map_node (fn (header, _, perspective, entries, result, consolidated) =>
    4.75 +    (header, keywords, perspective, entries, result, consolidated));
    4.76  
    4.77  fun get_keywords (Node {keywords, ...}) = keywords;
    4.78  
    4.79 @@ -134,8 +138,8 @@
    4.80  fun get_perspective (Node {perspective, ...}) = perspective;
    4.81  
    4.82  fun set_perspective args =
    4.83 -  map_node (fn (header, keywords, _, entries, result) =>
    4.84 -    (header, keywords, make_perspective args, entries, result));
    4.85 +  map_node (fn (header, keywords, _, entries, result, consolidated) =>
    4.86 +    (header, keywords, make_perspective args, entries, result, consolidated));
    4.87  
    4.88  val required_node = #required o get_perspective;
    4.89  val visible_command = Inttab.defined o #visible o get_perspective;
    4.90 @@ -144,8 +148,8 @@
    4.91  val overlays = Inttab.lookup_list o #overlays o get_perspective;
    4.92  
    4.93  fun map_entries f =
    4.94 -  map_node (fn (header, keywords, perspective, entries, result) =>
    4.95 -    (header, keywords, perspective, f entries, result));
    4.96 +  map_node (fn (header, keywords, perspective, entries, result, consolidated) =>
    4.97 +    (header, keywords, perspective, f entries, result, consolidated));
    4.98  
    4.99  fun get_entries (Node {entries, ...}) = entries;
   4.100  
   4.101 @@ -158,14 +162,8 @@
   4.102  fun get_result (Node {result, ...}) = result;
   4.103  
   4.104  fun set_result result =
   4.105 -  map_node (fn (header, keywords, perspective, entries, _) =>
   4.106 -    (header, keywords, perspective, entries, result));
   4.107 -
   4.108 -fun changed_result node node' =
   4.109 -  (case (get_result node, get_result node') of
   4.110 -    (SOME eval, SOME eval') => not (Command.eval_eq (eval, eval'))
   4.111 -  | (NONE, NONE) => false
   4.112 -  | _ => true);
   4.113 +  map_node (fn (header, keywords, perspective, entries, _, consolidated) =>
   4.114 +    (header, keywords, perspective, entries, result, consolidated));
   4.115  
   4.116  fun pending_result node =
   4.117    (case get_result node of
   4.118 @@ -177,6 +175,35 @@
   4.119      SOME eval => Command.eval_finished eval
   4.120    | NONE => false);
   4.121  
   4.122 +fun finished_result_theory node =
   4.123 +  finished_result node andalso
   4.124 +    let val st = Command.eval_result_state (the (get_result node))
   4.125 +    in (Toplevel.end_theory Position.none st; true) handle ERROR _ => false end;
   4.126 +
   4.127 +val reset_consolidated =
   4.128 +  map_node (fn (header, keywords, perspective, entries, result, _) =>
   4.129 +    (header, keywords, perspective, entries, result, Lazy.lazy I));
   4.130 +
   4.131 +fun check_consolidated (node as Node {consolidated, ...}) =
   4.132 +  Lazy.is_finished consolidated orelse
   4.133 +  finished_result_theory node andalso
   4.134 +    let
   4.135 +      val result_id = Command.eval_exec_id (the (get_result node));
   4.136 +      val eval_ids =
   4.137 +        iterate_entries (fn (_, opt_exec) => fn eval_ids =>
   4.138 +          (case opt_exec of
   4.139 +            SOME (eval, _) => SOME (cons (Command.eval_exec_id eval) eval_ids)
   4.140 +          | NONE => NONE)) node [];
   4.141 +    in
   4.142 +      (case Execution.snapshot eval_ids of
   4.143 +        [] =>
   4.144 +         (Lazy.force consolidated;
   4.145 +          Position.setmp_thread_data (Position.id_only (Document_ID.print result_id))
   4.146 +            (fn () => Output.status (Markup.markup_only Markup.consolidated)) ();
   4.147 +          true)
   4.148 +      | _ => false)
   4.149 +    end;
   4.150 +
   4.151  fun get_node nodes name = String_Graph.get_node nodes name
   4.152    handle String_Graph.UNDEF _ => empty_node;
   4.153  fun default_node name = String_Graph.default_node (name, empty_node);
   4.154 @@ -400,10 +427,16 @@
   4.155  
   4.156  val the_command_name = #1 oo the_command;
   4.157  
   4.158 +
   4.159 +(* execution *)
   4.160 +
   4.161 +fun get_execution (State {execution, ...}) = execution;
   4.162 +fun get_execution_version state = the_version state (#version_id (get_execution state));
   4.163 +
   4.164  fun command_exec state node_name command_id =
   4.165    let
   4.166 -    val State {execution = {version_id, ...}, ...} = state;
   4.167 -    val node = get_node (nodes_of (the_version state version_id)) node_name;
   4.168 +    val version = get_execution_version state;
   4.169 +    val node = get_node (nodes_of version) node_name;
   4.170    in the_entry node command_id end;
   4.171  
   4.172  end;
   4.173 @@ -492,6 +525,10 @@
   4.174          {version_id = version_id, execution_id = execution_id, delay_request = delay_request'};
   4.175      in (versions, blobs, commands, execution') end));
   4.176  
   4.177 +fun consolidate_execution state =
   4.178 +  String_Graph.fold (fn (_, (node, _)) => fn () => ignore (check_consolidated node))
   4.179 +    (nodes_of (get_execution_version state)) ();
   4.180 +
   4.181  
   4.182  
   4.183  (** document update **)
   4.184 @@ -702,11 +739,13 @@
   4.185                          val removed = maps (removed_execs node0) assign_update;
   4.186                          val _ = List.app Execution.cancel removed;
   4.187  
   4.188 +                        val result_changed =
   4.189 +                          not (eq_option Command.eval_eq (get_result node0, result));
   4.190                          val node' = node
   4.191                            |> assign_update_apply assigned_execs
   4.192 -                          |> set_result result;
   4.193 +                          |> set_result result
   4.194 +                          |> result_changed ? reset_consolidated;
   4.195                          val assigned_node = SOME (name, node');
   4.196 -                        val result_changed = changed_result node0 node';
   4.197                        in ((removed, assign_update, assigned_node, result_changed), node') end
   4.198                      else (([], [], NONE, false), node)
   4.199                    end))))
     5.1 --- a/src/Pure/PIDE/document.scala	Tue Aug 08 12:21:29 2017 +0200
     5.2 +++ b/src/Pure/PIDE/document.scala	Tue Aug 08 22:13:05 2017 +0200
     5.3 @@ -453,6 +453,7 @@
     5.4  
     5.5      def node_name: Node.Name
     5.6      def node: Node
     5.7 +    def node_consolidated: Boolean
     5.8  
     5.9      def commands_loading: List[Command]
    5.10      def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range]
    5.11 @@ -791,6 +792,11 @@
    5.12        } yield tree).toList
    5.13      }
    5.14  
    5.15 +    def node_consolidated(version: Version, name: Node.Name): Boolean =
    5.16 +      !name.is_theory ||
    5.17 +        version.nodes(name).commands.reverse.iterator.
    5.18 +          flatMap(command_states(version, _)).exists(_.consolidated)
    5.19 +
    5.20      // persistent user-view
    5.21      def snapshot(name: Node.Name = Node.Name.empty, pending_edits: List[Text.Edit] = Nil)
    5.22        : Snapshot =
    5.23 @@ -835,6 +841,8 @@
    5.24          val node_name: Node.Name = name
    5.25          val node: Node = version.nodes(name)
    5.26  
    5.27 +        def node_consolidated: Boolean = state.node_consolidated(version, node_name)
    5.28 +
    5.29          val commands_loading: List[Command] =
    5.30            if (node_name.is_theory) Nil
    5.31            else version.nodes.commands_loading(node_name)
     6.1 --- a/src/Pure/PIDE/markup.ML	Tue Aug 08 12:21:29 2017 +0200
     6.2 +++ b/src/Pure/PIDE/markup.ML	Tue Aug 08 22:13:05 2017 +0200
     6.3 @@ -159,6 +159,7 @@
     6.4    val runningN: string val running: T
     6.5    val finishedN: string val finished: T
     6.6    val failedN: string val failed: T
     6.7 +  val consolidatedN: string val consolidated: T
     6.8    val exec_idN: string
     6.9    val initN: string
    6.10    val statusN: string val status: T
    6.11 @@ -555,6 +556,7 @@
    6.12  val (runningN, running) = markup_elem "running";
    6.13  val (finishedN, finished) = markup_elem "finished";
    6.14  val (failedN, failed) = markup_elem "failed";
    6.15 +val (consolidatedN, consolidated) = markup_elem "consolidated";
    6.16  
    6.17  
    6.18  (* messages *)
     7.1 --- a/src/Pure/PIDE/markup.scala	Tue Aug 08 12:21:29 2017 +0200
     7.2 +++ b/src/Pure/PIDE/markup.scala	Tue Aug 08 22:13:05 2017 +0200
     7.3 @@ -423,6 +423,7 @@
     7.4    val RUNNING = "running"
     7.5    val FINISHED = "finished"
     7.6    val FAILED = "failed"
     7.7 +  val CONSOLIDATED = "consolidated"
     7.8  
     7.9  
    7.10    /* interactive documents */
     8.1 --- a/src/Pure/PIDE/protocol.ML	Tue Aug 08 12:21:29 2017 +0200
     8.2 +++ b/src/Pure/PIDE/protocol.ML	Tue Aug 08 22:13:05 2017 +0200
     8.3 @@ -58,6 +58,10 @@
     8.4        end);
     8.5  
     8.6  val _ =
     8.7 +  Isabelle_Process.protocol_command "Document.consolidate_execution"
     8.8 +    (fn [] => Document.consolidate_execution (Document.state ()));
     8.9 +
    8.10 +val _ =
    8.11    Isabelle_Process.protocol_command "Document.discontinue_execution"
    8.12      (fn [] => Execution.discontinue ());
    8.13  
     9.1 --- a/src/Pure/PIDE/protocol.scala	Tue Aug 08 12:21:29 2017 +0200
     9.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Aug 08 22:13:05 2017 +0200
     9.3 @@ -352,6 +352,9 @@
     9.4  
     9.5    /* execution */
     9.6  
     9.7 +  def consolidate_execution(): Unit =
     9.8 +    protocol_command("Document.consolidate_execution")
     9.9 +
    9.10    def discontinue_execution(): Unit =
    9.11      protocol_command("Document.discontinue_execution")
    9.12  
    10.1 --- a/src/Pure/PIDE/session.scala	Tue Aug 08 12:21:29 2017 +0200
    10.2 +++ b/src/Pure/PIDE/session.scala	Tue Aug 08 22:13:05 2017 +0200
    10.3 @@ -130,6 +130,7 @@
    10.4    /* dynamic session options */
    10.5  
    10.6    def output_delay: Time = session_options.seconds("editor_output_delay")
    10.7 +  def consolidate_delay: Time = session_options.seconds("editor_consolidate_delay")
    10.8    def prune_delay: Time = session_options.seconds("editor_prune_delay")
    10.9    def prune_size: Int = session_options.int("editor_prune_size")
   10.10    def syslog_limit: Int = session_options.int("editor_syslog_limit")
   10.11 @@ -191,6 +192,7 @@
   10.12    private case class Cancel_Exec(exec_id: Document_ID.Exec)
   10.13    private case class Protocol_Command(name: String, args: List[String])
   10.14    private case class Update_Options(options: Options)
   10.15 +  private case object Consolidate_Execution
   10.16    private case object Prune_History
   10.17  
   10.18  
   10.19 @@ -519,6 +521,9 @@
   10.20                prover.get.terminate
   10.21              }
   10.22  
   10.23 +          case Consolidate_Execution =>
   10.24 +            if (prover.defined) prover.get.consolidate_execution()
   10.25 +
   10.26            case Prune_History =>
   10.27              if (prover.defined) {
   10.28                val old_versions = global_state.change_result(_.remove_versions(prune_size))
   10.29 @@ -564,6 +569,28 @@
   10.30      }
   10.31    }
   10.32  
   10.33 +  private val consolidator: Thread =
   10.34 +    Standard_Thread.fork("Session.consolidator", daemon = true) {
   10.35 +      try {
   10.36 +        while (true) {
   10.37 +          Thread.sleep(consolidate_delay.ms)
   10.38 +
   10.39 +          val state = global_state.value
   10.40 +          state.stable_tip_version match {
   10.41 +            case None =>
   10.42 +            case Some(version) =>
   10.43 +              val consolidated =
   10.44 +                version.nodes.iterator.forall(
   10.45 +                  { case (name, _) =>
   10.46 +                      resources.session_base.loaded_theory(name) ||
   10.47 +                      state.node_consolidated(version, name) })
   10.48 +              if (!consolidated) manager.send(Consolidate_Execution)
   10.49 +          }
   10.50 +        }
   10.51 +      }
   10.52 +      catch { case Exn.Interrupt() => }
   10.53 +    }
   10.54 +
   10.55  
   10.56    /* main operations */
   10.57  
   10.58 @@ -602,6 +629,8 @@
   10.59  
   10.60      change_parser.shutdown()
   10.61      change_buffer.shutdown()
   10.62 +    consolidator.interrupt
   10.63 +    consolidator.join
   10.64      manager.shutdown()
   10.65      dispatcher.shutdown()
   10.66