support dynamic commit of consilidated nodes;
authorwenzelm
Wed Sep 05 21:56:44 2018 +0200 (9 months ago)
changeset 689162a1583baaaa0
parent 68915 634768c0bd22
child 68917 75691a5c8fb6
child 68919 027219002f32
support dynamic commit of consilidated nodes;
tuned signature;
src/Pure/Thy/thy_resources.scala
     1.1 --- a/src/Pure/Thy/thy_resources.scala	Wed Sep 05 20:29:23 2018 +0200
     1.2 +++ b/src/Pure/Thy/thy_resources.scala	Wed Sep 05 21:56:44 2018 +0200
     1.3 @@ -55,6 +55,14 @@
     1.4      }
     1.5    }
     1.6  
     1.7 +  private def stable_snapshot(
     1.8 +    state: Document.State, version: Document.Version, name: Document.Node.Name): Document.Snapshot =
     1.9 +  {
    1.10 +    val snapshot = state.snapshot(name)
    1.11 +    assert(version.id == snapshot.version.id)
    1.12 +    snapshot
    1.13 +  }
    1.14 +
    1.15    class Theories_Result private[Thy_Resources](
    1.16      val state: Document.State,
    1.17      val version: Document.Version,
    1.18 @@ -62,13 +70,7 @@
    1.19    {
    1.20      def node_names: List[Document.Node.Name] = nodes.map(_._1)
    1.21      def ok: Boolean = nodes.forall({ case (_, st) => st.ok })
    1.22 -
    1.23 -    def snapshot(node_name: Document.Node.Name): Document.Snapshot =
    1.24 -    {
    1.25 -      val snapshot = state.snapshot(node_name)
    1.26 -      assert(version.id == snapshot.version.id)
    1.27 -      snapshot
    1.28 -    }
    1.29 +    def snapshot(name: Document.Node.Name): Document.Snapshot = stable_snapshot(state, version, name)
    1.30    }
    1.31  
    1.32    val default_check_delay: Double = 0.5
    1.33 @@ -99,7 +101,9 @@
    1.34      private sealed case class Use_Theories_State(
    1.35        last_update: Time = Time.now(),
    1.36        nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty,
    1.37 -      already_initialized: Set[Document.Node.Name] = Set.empty)
    1.38 +      already_initialized: Set[Document.Node.Name] = Set.empty,
    1.39 +      already_committed: Set[Document.Node.Name] = Set.empty,
    1.40 +      result: Promise[Theories_Result] = Future.promise[Theories_Result])
    1.41      {
    1.42        def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State =
    1.43          copy(last_update = Time.now(), nodes_status = new_nodes_status)
    1.44 @@ -110,16 +114,61 @@
    1.45        def initialized_theories(
    1.46          state: Document.State,
    1.47          version: Document.Version,
    1.48 -        new_theories: List[Document.Node.Name]): (List[Document.Node.Name], Use_Theories_State) =
    1.49 +        theories: List[Document.Node.Name]): (List[Document.Node.Name], Use_Theories_State) =
    1.50        {
    1.51          val initialized =
    1.52            for {
    1.53 -            name <- new_theories
    1.54 +            name <- theories
    1.55              if !already_initialized(name) &&
    1.56                Document_Status.Node_Status.make(state, version, name).initialized
    1.57            } yield name
    1.58          (initialized, copy(already_initialized = already_initialized ++ initialized))
    1.59        }
    1.60 +
    1.61 +      def cancel_result { result.cancel }
    1.62 +      def await_result { result.join_result }
    1.63 +      def join_result: Theories_Result = result.join
    1.64 +      def check_result(
    1.65 +          state: Document.State,
    1.66 +          version: Document.Version,
    1.67 +          theories: List[Document.Node.Name],
    1.68 +          beyond_limit: Boolean,
    1.69 +          watchdog_timeout: Time,
    1.70 +          commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit])
    1.71 +        : Use_Theories_State =
    1.72 +      {
    1.73 +        val st1 =
    1.74 +          if (commit.isDefined) {
    1.75 +            val committed =
    1.76 +              for {
    1.77 +                name <- theories
    1.78 +                if !already_committed(name) && state.node_consolidated(version, name)
    1.79 +              }
    1.80 +              yield {
    1.81 +                val snapshot = stable_snapshot(state, version, name)
    1.82 +                val status = Document_Status.Node_Status.make(state, version, name)
    1.83 +                commit.get.apply(snapshot, status)
    1.84 +                name
    1.85 +              }
    1.86 +            copy(already_committed = already_committed ++ committed)
    1.87 +          }
    1.88 +          else this
    1.89 +
    1.90 +        if (beyond_limit || watchdog(watchdog_timeout) ||
    1.91 +          theories.forall(name =>
    1.92 +            already_committed(name) ||
    1.93 +            state.node_consolidated(version, name) ||
    1.94 +            nodes_status.quasi_consolidated(name)))
    1.95 +        {
    1.96 +          val nodes =
    1.97 +            for (name <- theories)
    1.98 +            yield { (name -> Document_Status.Node_Status.make(state, version, name)) }
    1.99 +          try { result.fulfill(new Theories_Result(state, version, nodes)) }
   1.100 +          catch { case _: IllegalStateException => }
   1.101 +        }
   1.102 +
   1.103 +        st1
   1.104 +      }
   1.105      }
   1.106  
   1.107      def use_theories(
   1.108 @@ -131,6 +180,8 @@
   1.109        watchdog_timeout: Time = Time.zero,
   1.110        nodes_status_delay: Time = Time.seconds(default_nodes_status_delay),
   1.111        id: UUID = UUID(),
   1.112 +      // commit: must not block, must not fail
   1.113 +      commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None,
   1.114        progress: Progress = No_Progress): Theories_Result =
   1.115      {
   1.116        val dep_theories =
   1.117 @@ -143,25 +194,14 @@
   1.118        val dep_theories_set = dep_theories.toSet
   1.119  
   1.120        val use_theories_state = Synchronized(Use_Theories_State())
   1.121 -      val result = Future.promise[Theories_Result]
   1.122  
   1.123 -      def check_state(beyond_limit: Boolean = false)
   1.124 +      def check_result(beyond_limit: Boolean = false)
   1.125        {
   1.126          val state = session.current_state()
   1.127          state.stable_tip_version match {
   1.128            case Some(version) =>
   1.129 -            val st = use_theories_state.value
   1.130 -            if (beyond_limit || st.watchdog(watchdog_timeout) ||
   1.131 -                dep_theories.forall(name =>
   1.132 -                  state.node_consolidated(version, name) ||
   1.133 -                  st.nodes_status.quasi_consolidated(name)))
   1.134 -            {
   1.135 -              val nodes =
   1.136 -                for (name <- dep_theories)
   1.137 -                yield (name -> Document_Status.Node_Status.make(state, version, name))
   1.138 -              try { result.fulfill(new Theories_Result(state, version, nodes)) }
   1.139 -              catch { case _: IllegalStateException => }
   1.140 -            }
   1.141 +            use_theories_state.change(
   1.142 +              _.check_result(state, version, dep_theories, beyond_limit, watchdog_timeout, commit))
   1.143            case None =>
   1.144          }
   1.145        }
   1.146 @@ -171,10 +211,10 @@
   1.147          var check_count = 0
   1.148          Event_Timer.request(Time.now(), repeat = Some(check_delay))
   1.149            {
   1.150 -            if (progress.stopped) result.cancel
   1.151 +            if (progress.stopped) use_theories_state.value.cancel_result
   1.152              else {
   1.153                check_count += 1
   1.154 -              check_state(check_limit > 0 && check_count > check_limit)
   1.155 +              check_result(check_limit > 0 && check_count > check_limit)
   1.156              }
   1.157            }
   1.158        }
   1.159 @@ -235,7 +275,7 @@
   1.160                for ((theory, percentage) <- theory_percentages)
   1.161                  progress.theory_percentage("", theory, percentage)
   1.162  
   1.163 -              check_state()
   1.164 +              check_result()
   1.165              }
   1.166          }
   1.167        }
   1.168 @@ -243,7 +283,7 @@
   1.169        try {
   1.170          session.commands_changed += consumer
   1.171          resources.load_theories(session, id, dep_theories, progress)
   1.172 -        result.join_result
   1.173 +        use_theories_state.value.await_result
   1.174          check_progress.cancel
   1.175        }
   1.176        finally {
   1.177 @@ -251,7 +291,7 @@
   1.178          resources.unload_theories(session, id, dep_theories)
   1.179        }
   1.180  
   1.181 -      result.join
   1.182 +      use_theories_state.value.join_result
   1.183      }
   1.184  
   1.185      def purge_theories(