less wasteful consolidation, based on PIDE front-end state and recent changes;
authorwenzelm
Tue Jun 05 16:12:26 2018 +0200 (15 months ago)
changeset 683812fd3a6d6ba2e
parent 68380 f249e1f5623b
child 68382 b10ae73f0bab
less wasteful consolidation, based on PIDE front-end state and recent changes;
etc/options
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.ML
src/Pure/PIDE/document.scala
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/resources.scala
src/Pure/PIDE/session.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/etc/options	Tue Jun 05 14:15:49 2018 +0200
     1.2 +++ b/etc/options	Tue Jun 05 16:12:26 2018 +0200
     1.3 @@ -156,7 +156,7 @@
     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 = 2.5
     1.8 +public option editor_consolidate_delay : real = 2.0
     1.9    -- "delay to consolidate status of command evaluation (execution forks)"
    1.10  
    1.11  public option editor_prune_delay : real = 15
     2.1 --- a/src/Pure/PIDE/command.scala	Tue Jun 05 14:15:49 2018 +0200
     2.2 +++ b/src/Pure/PIDE/command.scala	Tue Jun 05 16:12:26 2018 +0200
     2.3 @@ -263,6 +263,8 @@
     2.4      def initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED)
     2.5      def consolidated: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATED)
     2.6  
     2.7 +    lazy val maybe_consolidated: Boolean = Protocol.maybe_consolidated(status)
     2.8 +
     2.9      lazy val protocol_status: Protocol.Status =
    2.10      {
    2.11        val warnings =
     3.1 --- a/src/Pure/PIDE/document.ML	Tue Jun 05 14:15:49 2018 +0200
     3.2 +++ b/src/Pure/PIDE/document.ML	Tue Jun 05 16:12:26 2018 +0200
     3.3 @@ -24,7 +24,7 @@
     3.4    val command_exec: state -> string -> Document_ID.command -> Command.exec option
     3.5    val remove_versions: Document_ID.version list -> state -> state
     3.6    val start_execution: state -> state
     3.7 -  val update: Document_ID.version -> Document_ID.version -> edit list -> bool -> state ->
     3.8 +  val update: Document_ID.version -> Document_ID.version -> edit list -> string list -> state ->
     3.9      Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
    3.10    val state: unit -> state
    3.11    val change_state: (state -> state) -> unit
    3.12 @@ -768,6 +768,7 @@
    3.13        timeit "Document.edit_nodes"
    3.14          (fn () => old_version |> fold edit_nodes edits |> edit_keywords edits);
    3.15  
    3.16 +    val consolidate = Symtab.defined (Symtab.make_set consolidate);
    3.17      val nodes = nodes_of new_version;
    3.18      val required = make_required nodes;
    3.19      val required0 = make_required (nodes_of old_version);
    3.20 @@ -786,7 +787,7 @@
    3.21                      val root_theory = check_root_theory node;
    3.22                      val keywords = the_default (Session.get_keywords ()) (get_keywords node);
    3.23  
    3.24 -                    val maybe_consolidate = consolidate andalso could_consolidate node;
    3.25 +                    val maybe_consolidate = consolidate name andalso could_consolidate node;
    3.26                      val imports = map (apsnd Future.join) deps;
    3.27                      val imports_result_changed = exists (#4 o #1 o #2) imports;
    3.28                      val node_required = Symtab.defined required name;
     4.1 --- a/src/Pure/PIDE/document.scala	Tue Jun 05 14:15:49 2018 +0200
     4.2 +++ b/src/Pure/PIDE/document.scala	Tue Jun 05 16:12:26 2018 +0200
     4.3 @@ -849,6 +849,18 @@
     4.4          removing_versions = false)
     4.5      }
     4.6  
     4.7 +    def command_state_eval(version: Version, command: Command): Option[Command.State] =
     4.8 +    {
     4.9 +      require(is_assigned(version))
    4.10 +      try {
    4.11 +        the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil) match {
    4.12 +          case eval_id :: _ => Some(the_dynamic_state(eval_id))
    4.13 +          case Nil => None
    4.14 +        }
    4.15 +      }
    4.16 +      catch { case _: State.Fail => None }
    4.17 +    }
    4.18 +
    4.19      private def command_states_self(version: Version, command: Command)
    4.20        : List[(Document_ID.Generic, Command.State)] =
    4.21      {
    4.22 @@ -930,6 +942,16 @@
    4.23          case Some(command) => command_states(version, command).headOption.exists(_.initialized)
    4.24        })
    4.25  
    4.26 +    def node_maybe_consolidated(version: Version, name: Node.Name): Boolean =
    4.27 +      name.is_theory &&
    4.28 +      {
    4.29 +        version.nodes(name).commands.reverse.iterator.forall(command =>
    4.30 +          command_state_eval(version, command) match {
    4.31 +            case None => false
    4.32 +            case Some(st) => st.maybe_consolidated
    4.33 +          })
    4.34 +      }
    4.35 +
    4.36      def node_consolidated(version: Version, name: Node.Name): Boolean =
    4.37        !name.is_theory ||
    4.38        {
     5.1 --- a/src/Pure/PIDE/protocol.ML	Tue Jun 05 14:15:49 2018 +0200
     5.2 +++ b/src/Pure/PIDE/protocol.ML	Tue Jun 05 16:12:26 2018 +0200
     5.3 @@ -74,7 +74,7 @@
     5.4  val _ =
     5.5    Isabelle_Process.protocol_command "Document.update"
     5.6      (Future.task_context "Document.update" (Future.new_group NONE)
     5.7 -      (fn [old_id_string, new_id_string, edits_yxml, consolidate_string] =>
     5.8 +      (fn [old_id_string, new_id_string, edits_yxml, consolidate_yxml] =>
     5.9          Document.change_state (fn state =>
    5.10            let
    5.11              val old_id = Document_ID.parse old_id_string;
    5.12 @@ -100,7 +100,9 @@
    5.13                          Document.Perspective (bool_atom a, map int_atom b,
    5.14                            list (pair int (pair string (list string))) c)]))
    5.15                  end;
    5.16 -            val consolidate = Value.parse_bool consolidate_string;
    5.17 +            val consolidate =
    5.18 +              YXML.parse_body consolidate_yxml |>
    5.19 +                let open XML.Decode in list string end;
    5.20  
    5.21              val _ = Execution.discontinue ();
    5.22  
     6.1 --- a/src/Pure/PIDE/protocol.scala	Tue Jun 05 14:15:49 2018 +0200
     6.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Jun 05 16:12:26 2018 +0200
     6.3 @@ -38,6 +38,26 @@
     6.4    }
     6.5  
     6.6  
     6.7 +  /* consolidation status */
     6.8 +
     6.9 +  def maybe_consolidated(markups: List[Markup]): Boolean =
    6.10 +  {
    6.11 +    var touched = false
    6.12 +    var forks = 0
    6.13 +    var runs = 0
    6.14 +    for (markup <- markups) {
    6.15 +      markup.name match {
    6.16 +        case Markup.FORKED => touched = true; forks += 1
    6.17 +        case Markup.JOINED => forks -= 1
    6.18 +        case Markup.RUNNING => touched = true; runs += 1
    6.19 +        case Markup.FINISHED => runs -= 1
    6.20 +        case _ =>
    6.21 +      }
    6.22 +    }
    6.23 +    touched && forks == 0 && runs == 0
    6.24 +  }
    6.25 +
    6.26 +
    6.27    /* command status */
    6.28  
    6.29    object Status
    6.30 @@ -419,7 +439,7 @@
    6.31    /* document versions */
    6.32  
    6.33    def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
    6.34 -    edits: List[Document.Edit_Command], consolidate: Boolean)
    6.35 +    edits: List[Document.Edit_Command], consolidate: List[Document.Node.Name])
    6.36    {
    6.37      val edits_yxml =
    6.38      {
    6.39 @@ -446,9 +466,17 @@
    6.40          val (name, edit) = node_edit
    6.41          pair(string, encode_edit(name))(name.node, edit)
    6.42        })
    6.43 -      Symbol.encode_yxml(encode_edits(edits)) }
    6.44 +      Symbol.encode_yxml(encode_edits(edits))
    6.45 +    }
    6.46 +
    6.47 +    val consolidate_yxml =
    6.48 +    {
    6.49 +      import XML.Encode._
    6.50 +      Symbol.encode_yxml(list(string)(consolidate.map(_.node)))
    6.51 +    }
    6.52 +
    6.53      protocol_command(
    6.54 -      "Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml, consolidate.toString)
    6.55 +      "Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml, consolidate_yxml)
    6.56    }
    6.57  
    6.58    def remove_versions(versions: List[Document.Version])
     7.1 --- a/src/Pure/PIDE/resources.scala	Tue Jun 05 14:15:49 2018 +0200
     7.2 +++ b/src/Pure/PIDE/resources.scala	Tue Jun 05 16:12:26 2018 +0200
     7.3 @@ -216,7 +216,7 @@
     7.4        previous: Document.Version,
     7.5        doc_blobs: Document.Blobs,
     7.6        edits: List[Document.Edit_Text],
     7.7 -      consolidate: Boolean): Session.Change =
     7.8 +      consolidate: List[Document.Node.Name]): Session.Change =
     7.9      Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits, consolidate)
    7.10  
    7.11    def commit(change: Session.Change) { }
     8.1 --- a/src/Pure/PIDE/session.scala	Tue Jun 05 14:15:49 2018 +0200
     8.2 +++ b/src/Pure/PIDE/session.scala	Tue Jun 05 16:12:26 2018 +0200
     8.3 @@ -50,7 +50,7 @@
     8.4      syntax_changed: List[Document.Node.Name],
     8.5      deps_changed: Boolean,
     8.6      doc_edits: List[Document.Edit_Command],
     8.7 -    consolidate: Boolean,
     8.8 +    consolidate: List[Document.Node.Name],
     8.9      version: Document.Version)
    8.10  
    8.11    case object Change_Flush
    8.12 @@ -231,7 +231,7 @@
    8.13      previous: Future[Document.Version],
    8.14      doc_blobs: Document.Blobs,
    8.15      text_edits: List[Document.Edit_Text],
    8.16 -    consolidate: Boolean,
    8.17 +    consolidate: List[Document.Node.Name],
    8.18      version_result: Promise[Document.Version])
    8.19  
    8.20    private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true)
    8.21 @@ -259,6 +259,7 @@
    8.22      def flush(): Unit = synchronized {
    8.23        if (assignment || nodes.nonEmpty || commands.nonEmpty)
    8.24          commands_changed.post(Session.Commands_Changed(assignment, nodes, commands))
    8.25 +      if (nodes.nonEmpty) consolidation.update(nodes)
    8.26        assignment = false
    8.27        nodes = Set.empty
    8.28        commands = Set.empty
    8.29 @@ -299,6 +300,28 @@
    8.30    }
    8.31  
    8.32  
    8.33 +  /* node consolidation */
    8.34 +
    8.35 +  private object consolidation
    8.36 +  {
    8.37 +    private val delay =
    8.38 +      Standard_Thread.delay_first(consolidate_delay) { manager.send(Consolidate_Execution) }
    8.39 +
    8.40 +    private val changed_nodes = Synchronized(Set.empty[Document.Node.Name])
    8.41 +
    8.42 +    def update(new_nodes: Set[Document.Node.Name] = Set.empty)
    8.43 +    {
    8.44 +      changed_nodes.change(nodes => if (nodes.isEmpty) new_nodes else nodes ++ new_nodes)
    8.45 +      delay.invoke()
    8.46 +    }
    8.47 +
    8.48 +    def flush(): Set[Document.Node.Name] =
    8.49 +      changed_nodes.change_result(nodes => (nodes, Set.empty))
    8.50 +
    8.51 +    def shutdown() { delay.revoke() }
    8.52 +  }
    8.53 +
    8.54 +
    8.55    /* prover process */
    8.56  
    8.57    private object prover
    8.58 @@ -347,7 +370,7 @@
    8.59      def handle_raw_edits(
    8.60        doc_blobs: Document.Blobs = Document.Blobs.empty,
    8.61        edits: List[Document.Edit_Text] = Nil,
    8.62 -      consolidate: Boolean = false)
    8.63 +      consolidate: List[Document.Node.Name] = Nil)
    8.64      //{{{
    8.65      {
    8.66        require(prover.defined)
    8.67 @@ -534,7 +557,19 @@
    8.68              }
    8.69  
    8.70            case Consolidate_Execution =>
    8.71 -            if (prover.defined) handle_raw_edits(consolidate = true)
    8.72 +            if (prover.defined) {
    8.73 +              val state = global_state.value
    8.74 +              state.stable_tip_version match {
    8.75 +                case None => consolidation.update()
    8.76 +                case Some(version) =>
    8.77 +                  val consolidate =
    8.78 +                    consolidation.flush().iterator.filter(name =>
    8.79 +                      !resources.session_base.loaded_theory(name) &&
    8.80 +                      !state.node_consolidated(version, name) &&
    8.81 +                      state.node_maybe_consolidated(version, name)).toList
    8.82 +                  if (consolidate.nonEmpty) handle_raw_edits(consolidate = consolidate)
    8.83 +              }
    8.84 +            }
    8.85  
    8.86            case Prune_History =>
    8.87              if (prover.defined) {
    8.88 @@ -581,28 +616,6 @@
    8.89      }
    8.90    }
    8.91  
    8.92 -  private val consolidator: Thread =
    8.93 -    Standard_Thread.fork("Session.consolidator", daemon = true) {
    8.94 -      try {
    8.95 -        while (true) {
    8.96 -          Thread.sleep(consolidate_delay.ms)
    8.97 -
    8.98 -          val state = global_state.value
    8.99 -          state.stable_tip_version match {
   8.100 -            case None =>
   8.101 -            case Some(version) =>
   8.102 -              val consolidated =
   8.103 -                version.nodes.iterator.forall(
   8.104 -                  { case (name, _) =>
   8.105 -                      resources.session_base.loaded_theory(name) ||
   8.106 -                      state.node_consolidated(version, name) })
   8.107 -              if (!consolidated) manager.send(Consolidate_Execution)
   8.108 -          }
   8.109 -        }
   8.110 -      }
   8.111 -      catch { case Exn.Interrupt() => }
   8.112 -    }
   8.113 -
   8.114  
   8.115    /* main operations */
   8.116  
   8.117 @@ -641,8 +654,7 @@
   8.118  
   8.119      change_parser.shutdown()
   8.120      change_buffer.shutdown()
   8.121 -    consolidator.interrupt
   8.122 -    consolidator.join
   8.123 +    consolidation.shutdown()
   8.124      manager.shutdown()
   8.125      dispatcher.shutdown()
   8.126  
     9.1 --- a/src/Pure/Thy/thy_syntax.scala	Tue Jun 05 14:15:49 2018 +0200
     9.2 +++ b/src/Pure/Thy/thy_syntax.scala	Tue Jun 05 16:12:26 2018 +0200
     9.3 @@ -297,7 +297,7 @@
     9.4        previous: Document.Version,
     9.5        doc_blobs: Document.Blobs,
     9.6        edits: List[Document.Edit_Text],
     9.7 -      consolidate: Boolean): Session.Change =
     9.8 +      consolidate: List[Document.Node.Name]): Session.Change =
     9.9    {
    9.10      val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits)
    9.11