# HG changeset patch # User wenzelm # Date 1502223185 -7200 # Node ID 6392766f3c253d03f7665632bf9c868365edf462 # Parent 53a6c5d4d03e0fe36a3035d8096cfa736f31ed42 maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports); diff -r 53a6c5d4d03e -r 6392766f3c25 etc/options --- a/etc/options Tue Aug 08 12:21:29 2017 +0200 +++ b/etc/options Tue Aug 08 22:13:05 2017 +0200 @@ -155,6 +155,9 @@ public option editor_output_delay : real = 0.1 -- "delay for prover output (markup, common messages etc.)" +public option editor_consolidate_delay : real = 1.0 + -- "delay to consolidate status of command evaluation (execution forks)" + public option editor_prune_delay : real = 15 -- "delay to prune history (delete old versions)" diff -r 53a6c5d4d03e -r 6392766f3c25 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Tue Aug 08 12:21:29 2017 +0200 +++ b/src/Pure/PIDE/command.ML Tue Aug 08 22:13:05 2017 +0200 @@ -12,6 +12,7 @@ val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) -> blob list * int -> Token.T list -> Toplevel.transition type eval + val eval_exec_id: eval -> Document_ID.exec val eval_eq: eval * eval -> bool val eval_running: eval -> bool val eval_finished: eval -> bool diff -r 53a6c5d4d03e -r 6392766f3c25 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Tue Aug 08 12:21:29 2017 +0200 +++ b/src/Pure/PIDE/command.scala Tue Aug 08 22:13:05 2017 +0200 @@ -213,6 +213,9 @@ results: Results = Results.empty, markups: Markups = Markups.empty) { + lazy val consolidated: Boolean = + status.exists(markup => markup.name == Markup.CONSOLIDATED) + lazy val protocol_status: Protocol.Status = { val warnings = diff -r 53a6c5d4d03e -r 6392766f3c25 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Tue Aug 08 12:21:29 2017 +0200 +++ b/src/Pure/PIDE/document.ML Tue Aug 08 22:13:05 2017 +0200 @@ -24,6 +24,7 @@ val command_exec: state -> string -> Document_ID.command -> Command.exec option val remove_versions: Document_ID.version list -> state -> state val start_execution: state -> state + val consolidate_execution: state -> unit val update: Document_ID.version -> Document_ID.version -> edit list -> state -> Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state val state: unit -> state @@ -59,16 +60,17 @@ keywords: Keyword.keywords option, (*outer syntax keywords*) perspective: perspective, (*command perspective*) entries: Command.exec option Entries.T, (*command entries with executions*) - result: Command.eval option} (*result of last execution*) + result: Command.eval option, (*result of last execution*) + consolidated: unit lazy} (*consolidation status of eval forks*) and version = Version of node String_Graph.T (*development graph wrt. static imports*) with -fun make_node (header, keywords, perspective, entries, result) = +fun make_node (header, keywords, perspective, entries, result, consolidated) = Node {header = header, keywords = keywords, perspective = perspective, - entries = entries, result = result}; + entries = entries, result = result, consolidated = consolidated}; -fun map_node f (Node {header, keywords, perspective, entries, result}) = - make_node (f (header, keywords, perspective, entries, result)); +fun map_node f (Node {header, keywords, perspective, entries, result, consolidated}) = + make_node (f (header, keywords, perspective, entries, result, consolidated)); fun make_perspective (required, command_ids, overlays) : perspective = {required = required, @@ -80,7 +82,7 @@ {master = "", header = Thy_Header.make ("", Position.none) [] [], errors = []}; val no_perspective = make_perspective (false, [], []); -val empty_node = make_node (no_header, NONE, no_perspective, Entries.empty, NONE); +val empty_node = make_node (no_header, NONE, no_perspective, Entries.empty, NONE, Lazy.value ()); fun is_no_perspective ({required, visible, visible_last, overlays}: perspective) = not required andalso @@ -88,12 +90,13 @@ is_none visible_last andalso Inttab.is_empty overlays; -fun is_empty_node (Node {header, keywords, perspective, entries, result}) = +fun is_empty_node (Node {header, keywords, perspective, entries, result, consolidated}) = header = no_header andalso is_none keywords andalso is_no_perspective perspective andalso Entries.is_empty entries andalso - is_none result; + is_none result andalso + Lazy.is_finished consolidated; (* basic components *) @@ -104,14 +107,15 @@ | _ => Path.current); fun set_header master header errors = - map_node (fn (_, keywords, perspective, entries, result) => - ({master = master, header = header, errors = errors}, keywords, perspective, entries, result)); + map_node (fn (_, keywords, perspective, entries, result, consolidated) => + ({master = master, header = header, errors = errors}, + keywords, perspective, entries, result, consolidated)); fun get_header (Node {header, ...}) = header; fun set_keywords keywords = - map_node (fn (header, _, perspective, entries, result) => - (header, keywords, perspective, entries, result)); + map_node (fn (header, _, perspective, entries, result, consolidated) => + (header, keywords, perspective, entries, result, consolidated)); fun get_keywords (Node {keywords, ...}) = keywords; @@ -134,8 +138,8 @@ fun get_perspective (Node {perspective, ...}) = perspective; fun set_perspective args = - map_node (fn (header, keywords, _, entries, result) => - (header, keywords, make_perspective args, entries, result)); + map_node (fn (header, keywords, _, entries, result, consolidated) => + (header, keywords, make_perspective args, entries, result, consolidated)); val required_node = #required o get_perspective; val visible_command = Inttab.defined o #visible o get_perspective; @@ -144,8 +148,8 @@ val overlays = Inttab.lookup_list o #overlays o get_perspective; fun map_entries f = - map_node (fn (header, keywords, perspective, entries, result) => - (header, keywords, perspective, f entries, result)); + map_node (fn (header, keywords, perspective, entries, result, consolidated) => + (header, keywords, perspective, f entries, result, consolidated)); fun get_entries (Node {entries, ...}) = entries; @@ -158,14 +162,8 @@ fun get_result (Node {result, ...}) = result; fun set_result result = - map_node (fn (header, keywords, perspective, entries, _) => - (header, keywords, perspective, entries, result)); - -fun changed_result node node' = - (case (get_result node, get_result node') of - (SOME eval, SOME eval') => not (Command.eval_eq (eval, eval')) - | (NONE, NONE) => false - | _ => true); + map_node (fn (header, keywords, perspective, entries, _, consolidated) => + (header, keywords, perspective, entries, result, consolidated)); fun pending_result node = (case get_result node of @@ -177,6 +175,35 @@ SOME eval => Command.eval_finished eval | NONE => false); +fun finished_result_theory node = + finished_result node andalso + let val st = Command.eval_result_state (the (get_result node)) + in (Toplevel.end_theory Position.none st; true) handle ERROR _ => false end; + +val reset_consolidated = + map_node (fn (header, keywords, perspective, entries, result, _) => + (header, keywords, perspective, entries, result, Lazy.lazy I)); + +fun check_consolidated (node as Node {consolidated, ...}) = + Lazy.is_finished consolidated orelse + finished_result_theory node andalso + let + val result_id = Command.eval_exec_id (the (get_result node)); + val eval_ids = + iterate_entries (fn (_, opt_exec) => fn eval_ids => + (case opt_exec of + SOME (eval, _) => SOME (cons (Command.eval_exec_id eval) eval_ids) + | NONE => NONE)) node []; + in + (case Execution.snapshot eval_ids of + [] => + (Lazy.force consolidated; + Position.setmp_thread_data (Position.id_only (Document_ID.print result_id)) + (fn () => Output.status (Markup.markup_only Markup.consolidated)) (); + true) + | _ => false) + end; + fun get_node nodes name = String_Graph.get_node nodes name handle String_Graph.UNDEF _ => empty_node; fun default_node name = String_Graph.default_node (name, empty_node); @@ -400,10 +427,16 @@ val the_command_name = #1 oo the_command; + +(* execution *) + +fun get_execution (State {execution, ...}) = execution; +fun get_execution_version state = the_version state (#version_id (get_execution state)); + fun command_exec state node_name command_id = let - val State {execution = {version_id, ...}, ...} = state; - val node = get_node (nodes_of (the_version state version_id)) node_name; + val version = get_execution_version state; + val node = get_node (nodes_of version) node_name; in the_entry node command_id end; end; @@ -492,6 +525,10 @@ {version_id = version_id, execution_id = execution_id, delay_request = delay_request'}; in (versions, blobs, commands, execution') end)); +fun consolidate_execution state = + String_Graph.fold (fn (_, (node, _)) => fn () => ignore (check_consolidated node)) + (nodes_of (get_execution_version state)) (); + (** document update **) @@ -702,11 +739,13 @@ val removed = maps (removed_execs node0) assign_update; val _ = List.app Execution.cancel removed; + val result_changed = + not (eq_option Command.eval_eq (get_result node0, result)); val node' = node |> assign_update_apply assigned_execs - |> set_result result; + |> set_result result + |> result_changed ? reset_consolidated; val assigned_node = SOME (name, node'); - val result_changed = changed_result node0 node'; in ((removed, assign_update, assigned_node, result_changed), node') end else (([], [], NONE, false), node) end)))) diff -r 53a6c5d4d03e -r 6392766f3c25 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Tue Aug 08 12:21:29 2017 +0200 +++ b/src/Pure/PIDE/document.scala Tue Aug 08 22:13:05 2017 +0200 @@ -453,6 +453,7 @@ def node_name: Node.Name def node: Node + def node_consolidated: Boolean def commands_loading: List[Command] def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range] @@ -791,6 +792,11 @@ } yield tree).toList } + def node_consolidated(version: Version, name: Node.Name): Boolean = + !name.is_theory || + version.nodes(name).commands.reverse.iterator. + flatMap(command_states(version, _)).exists(_.consolidated) + // persistent user-view def snapshot(name: Node.Name = Node.Name.empty, pending_edits: List[Text.Edit] = Nil) : Snapshot = @@ -835,6 +841,8 @@ val node_name: Node.Name = name val node: Node = version.nodes(name) + def node_consolidated: Boolean = state.node_consolidated(version, node_name) + val commands_loading: List[Command] = if (node_name.is_theory) Nil else version.nodes.commands_loading(node_name) diff -r 53a6c5d4d03e -r 6392766f3c25 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Tue Aug 08 12:21:29 2017 +0200 +++ b/src/Pure/PIDE/markup.ML Tue Aug 08 22:13:05 2017 +0200 @@ -159,6 +159,7 @@ val runningN: string val running: T val finishedN: string val finished: T val failedN: string val failed: T + val consolidatedN: string val consolidated: T val exec_idN: string val initN: string val statusN: string val status: T @@ -555,6 +556,7 @@ val (runningN, running) = markup_elem "running"; val (finishedN, finished) = markup_elem "finished"; val (failedN, failed) = markup_elem "failed"; +val (consolidatedN, consolidated) = markup_elem "consolidated"; (* messages *) diff -r 53a6c5d4d03e -r 6392766f3c25 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Tue Aug 08 12:21:29 2017 +0200 +++ b/src/Pure/PIDE/markup.scala Tue Aug 08 22:13:05 2017 +0200 @@ -423,6 +423,7 @@ val RUNNING = "running" val FINISHED = "finished" val FAILED = "failed" + val CONSOLIDATED = "consolidated" /* interactive documents */ diff -r 53a6c5d4d03e -r 6392766f3c25 src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Tue Aug 08 12:21:29 2017 +0200 +++ b/src/Pure/PIDE/protocol.ML Tue Aug 08 22:13:05 2017 +0200 @@ -58,6 +58,10 @@ end); val _ = + Isabelle_Process.protocol_command "Document.consolidate_execution" + (fn [] => Document.consolidate_execution (Document.state ())); + +val _ = Isabelle_Process.protocol_command "Document.discontinue_execution" (fn [] => Execution.discontinue ()); diff -r 53a6c5d4d03e -r 6392766f3c25 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Tue Aug 08 12:21:29 2017 +0200 +++ b/src/Pure/PIDE/protocol.scala Tue Aug 08 22:13:05 2017 +0200 @@ -352,6 +352,9 @@ /* execution */ + def consolidate_execution(): Unit = + protocol_command("Document.consolidate_execution") + def discontinue_execution(): Unit = protocol_command("Document.discontinue_execution") diff -r 53a6c5d4d03e -r 6392766f3c25 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Tue Aug 08 12:21:29 2017 +0200 +++ b/src/Pure/PIDE/session.scala Tue Aug 08 22:13:05 2017 +0200 @@ -130,6 +130,7 @@ /* dynamic session options */ def output_delay: Time = session_options.seconds("editor_output_delay") + def consolidate_delay: Time = session_options.seconds("editor_consolidate_delay") def prune_delay: Time = session_options.seconds("editor_prune_delay") def prune_size: Int = session_options.int("editor_prune_size") def syslog_limit: Int = session_options.int("editor_syslog_limit") @@ -191,6 +192,7 @@ private case class Cancel_Exec(exec_id: Document_ID.Exec) private case class Protocol_Command(name: String, args: List[String]) private case class Update_Options(options: Options) + private case object Consolidate_Execution private case object Prune_History @@ -519,6 +521,9 @@ prover.get.terminate } + case Consolidate_Execution => + if (prover.defined) prover.get.consolidate_execution() + case Prune_History => if (prover.defined) { val old_versions = global_state.change_result(_.remove_versions(prune_size)) @@ -564,6 +569,28 @@ } } + private val consolidator: Thread = + Standard_Thread.fork("Session.consolidator", daemon = true) { + try { + while (true) { + Thread.sleep(consolidate_delay.ms) + + val state = global_state.value + state.stable_tip_version match { + case None => + case Some(version) => + val consolidated = + version.nodes.iterator.forall( + { case (name, _) => + resources.session_base.loaded_theory(name) || + state.node_consolidated(version, name) }) + if (!consolidated) manager.send(Consolidate_Execution) + } + } + } + catch { case Exn.Interrupt() => } + } + /* main operations */ @@ -602,6 +629,8 @@ change_parser.shutdown() change_buffer.shutdown() + consolidator.interrupt + consolidator.join manager.shutdown() dispatcher.shutdown()