# HG changeset patch # User wenzelm # Date 1528207946 -7200 # Node ID 2fd3a6d6ba2e455601fd80a4d66e2d6b9a0315e3 # Parent f249e1f5623b34b3421e3451017d9e71a755446f less wasteful consolidation, based on PIDE front-end state and recent changes; diff -r f249e1f5623b -r 2fd3a6d6ba2e etc/options --- a/etc/options Tue Jun 05 14:15:49 2018 +0200 +++ b/etc/options Tue Jun 05 16:12:26 2018 +0200 @@ -156,7 +156,7 @@ public option editor_output_delay : real = 0.1 -- "delay for prover output (markup, common messages etc.)" -public option editor_consolidate_delay : real = 2.5 +public option editor_consolidate_delay : real = 2.0 -- "delay to consolidate status of command evaluation (execution forks)" public option editor_prune_delay : real = 15 diff -r f249e1f5623b -r 2fd3a6d6ba2e src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Tue Jun 05 14:15:49 2018 +0200 +++ b/src/Pure/PIDE/command.scala Tue Jun 05 16:12:26 2018 +0200 @@ -263,6 +263,8 @@ def initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED) def consolidated: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATED) + lazy val maybe_consolidated: Boolean = Protocol.maybe_consolidated(status) + lazy val protocol_status: Protocol.Status = { val warnings = diff -r f249e1f5623b -r 2fd3a6d6ba2e src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Tue Jun 05 14:15:49 2018 +0200 +++ b/src/Pure/PIDE/document.ML Tue Jun 05 16:12:26 2018 +0200 @@ -24,7 +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 update: Document_ID.version -> Document_ID.version -> edit list -> bool -> state -> + val update: Document_ID.version -> Document_ID.version -> edit list -> string list -> state -> Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state val state: unit -> state val change_state: (state -> state) -> unit @@ -768,6 +768,7 @@ timeit "Document.edit_nodes" (fn () => old_version |> fold edit_nodes edits |> edit_keywords edits); + val consolidate = Symtab.defined (Symtab.make_set consolidate); val nodes = nodes_of new_version; val required = make_required nodes; val required0 = make_required (nodes_of old_version); @@ -786,7 +787,7 @@ val root_theory = check_root_theory node; val keywords = the_default (Session.get_keywords ()) (get_keywords node); - val maybe_consolidate = consolidate andalso could_consolidate node; + val maybe_consolidate = consolidate name andalso could_consolidate node; val imports = map (apsnd Future.join) deps; val imports_result_changed = exists (#4 o #1 o #2) imports; val node_required = Symtab.defined required name; diff -r f249e1f5623b -r 2fd3a6d6ba2e src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Tue Jun 05 14:15:49 2018 +0200 +++ b/src/Pure/PIDE/document.scala Tue Jun 05 16:12:26 2018 +0200 @@ -849,6 +849,18 @@ removing_versions = false) } + def command_state_eval(version: Version, command: Command): Option[Command.State] = + { + require(is_assigned(version)) + try { + the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil) match { + case eval_id :: _ => Some(the_dynamic_state(eval_id)) + case Nil => None + } + } + catch { case _: State.Fail => None } + } + private def command_states_self(version: Version, command: Command) : List[(Document_ID.Generic, Command.State)] = { @@ -930,6 +942,16 @@ case Some(command) => command_states(version, command).headOption.exists(_.initialized) }) + def node_maybe_consolidated(version: Version, name: Node.Name): Boolean = + name.is_theory && + { + version.nodes(name).commands.reverse.iterator.forall(command => + command_state_eval(version, command) match { + case None => false + case Some(st) => st.maybe_consolidated + }) + } + def node_consolidated(version: Version, name: Node.Name): Boolean = !name.is_theory || { diff -r f249e1f5623b -r 2fd3a6d6ba2e src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Tue Jun 05 14:15:49 2018 +0200 +++ b/src/Pure/PIDE/protocol.ML Tue Jun 05 16:12:26 2018 +0200 @@ -74,7 +74,7 @@ val _ = Isabelle_Process.protocol_command "Document.update" (Future.task_context "Document.update" (Future.new_group NONE) - (fn [old_id_string, new_id_string, edits_yxml, consolidate_string] => + (fn [old_id_string, new_id_string, edits_yxml, consolidate_yxml] => Document.change_state (fn state => let val old_id = Document_ID.parse old_id_string; @@ -100,7 +100,9 @@ Document.Perspective (bool_atom a, map int_atom b, list (pair int (pair string (list string))) c)])) end; - val consolidate = Value.parse_bool consolidate_string; + val consolidate = + YXML.parse_body consolidate_yxml |> + let open XML.Decode in list string end; val _ = Execution.discontinue (); diff -r f249e1f5623b -r 2fd3a6d6ba2e src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Tue Jun 05 14:15:49 2018 +0200 +++ b/src/Pure/PIDE/protocol.scala Tue Jun 05 16:12:26 2018 +0200 @@ -38,6 +38,26 @@ } + /* consolidation status */ + + def maybe_consolidated(markups: List[Markup]): Boolean = + { + var touched = false + var forks = 0 + var runs = 0 + for (markup <- markups) { + markup.name match { + case Markup.FORKED => touched = true; forks += 1 + case Markup.JOINED => forks -= 1 + case Markup.RUNNING => touched = true; runs += 1 + case Markup.FINISHED => runs -= 1 + case _ => + } + } + touched && forks == 0 && runs == 0 + } + + /* command status */ object Status @@ -419,7 +439,7 @@ /* document versions */ def update(old_id: Document_ID.Version, new_id: Document_ID.Version, - edits: List[Document.Edit_Command], consolidate: Boolean) + edits: List[Document.Edit_Command], consolidate: List[Document.Node.Name]) { val edits_yxml = { @@ -446,9 +466,17 @@ val (name, edit) = node_edit pair(string, encode_edit(name))(name.node, edit) }) - Symbol.encode_yxml(encode_edits(edits)) } + Symbol.encode_yxml(encode_edits(edits)) + } + + val consolidate_yxml = + { + import XML.Encode._ + Symbol.encode_yxml(list(string)(consolidate.map(_.node))) + } + protocol_command( - "Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml, consolidate.toString) + "Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml, consolidate_yxml) } def remove_versions(versions: List[Document.Version]) diff -r f249e1f5623b -r 2fd3a6d6ba2e src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Tue Jun 05 14:15:49 2018 +0200 +++ b/src/Pure/PIDE/resources.scala Tue Jun 05 16:12:26 2018 +0200 @@ -216,7 +216,7 @@ previous: Document.Version, doc_blobs: Document.Blobs, edits: List[Document.Edit_Text], - consolidate: Boolean): Session.Change = + consolidate: List[Document.Node.Name]): Session.Change = Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits, consolidate) def commit(change: Session.Change) { } diff -r f249e1f5623b -r 2fd3a6d6ba2e src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Tue Jun 05 14:15:49 2018 +0200 +++ b/src/Pure/PIDE/session.scala Tue Jun 05 16:12:26 2018 +0200 @@ -50,7 +50,7 @@ syntax_changed: List[Document.Node.Name], deps_changed: Boolean, doc_edits: List[Document.Edit_Command], - consolidate: Boolean, + consolidate: List[Document.Node.Name], version: Document.Version) case object Change_Flush @@ -231,7 +231,7 @@ previous: Future[Document.Version], doc_blobs: Document.Blobs, text_edits: List[Document.Edit_Text], - consolidate: Boolean, + consolidate: List[Document.Node.Name], version_result: Promise[Document.Version]) private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true) @@ -259,6 +259,7 @@ def flush(): Unit = synchronized { if (assignment || nodes.nonEmpty || commands.nonEmpty) commands_changed.post(Session.Commands_Changed(assignment, nodes, commands)) + if (nodes.nonEmpty) consolidation.update(nodes) assignment = false nodes = Set.empty commands = Set.empty @@ -299,6 +300,28 @@ } + /* node consolidation */ + + private object consolidation + { + private val delay = + Standard_Thread.delay_first(consolidate_delay) { manager.send(Consolidate_Execution) } + + private val changed_nodes = Synchronized(Set.empty[Document.Node.Name]) + + def update(new_nodes: Set[Document.Node.Name] = Set.empty) + { + changed_nodes.change(nodes => if (nodes.isEmpty) new_nodes else nodes ++ new_nodes) + delay.invoke() + } + + def flush(): Set[Document.Node.Name] = + changed_nodes.change_result(nodes => (nodes, Set.empty)) + + def shutdown() { delay.revoke() } + } + + /* prover process */ private object prover @@ -347,7 +370,7 @@ def handle_raw_edits( doc_blobs: Document.Blobs = Document.Blobs.empty, edits: List[Document.Edit_Text] = Nil, - consolidate: Boolean = false) + consolidate: List[Document.Node.Name] = Nil) //{{{ { require(prover.defined) @@ -534,7 +557,19 @@ } case Consolidate_Execution => - if (prover.defined) handle_raw_edits(consolidate = true) + if (prover.defined) { + val state = global_state.value + state.stable_tip_version match { + case None => consolidation.update() + case Some(version) => + val consolidate = + consolidation.flush().iterator.filter(name => + !resources.session_base.loaded_theory(name) && + !state.node_consolidated(version, name) && + state.node_maybe_consolidated(version, name)).toList + if (consolidate.nonEmpty) handle_raw_edits(consolidate = consolidate) + } + } case Prune_History => if (prover.defined) { @@ -581,28 +616,6 @@ } } - 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 */ @@ -641,8 +654,7 @@ change_parser.shutdown() change_buffer.shutdown() - consolidator.interrupt - consolidator.join + consolidation.shutdown() manager.shutdown() dispatcher.shutdown() diff -r f249e1f5623b -r 2fd3a6d6ba2e src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Tue Jun 05 14:15:49 2018 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Tue Jun 05 16:12:26 2018 +0200 @@ -297,7 +297,7 @@ previous: Document.Version, doc_blobs: Document.Blobs, edits: List[Document.Edit_Text], - consolidate: Boolean): Session.Change = + consolidate: List[Document.Node.Name]): Session.Change = { val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits)