clarified Use_Theories_State;
authorwenzelm
Wed Sep 05 20:00:38 2018 +0200 (13 months ago)
changeset 6891451bd9e9501fb
parent 68913 55b12fde48d0
child 68915 634768c0bd22
clarified Use_Theories_State;
src/Pure/Thy/thy_resources.scala
     1.1 --- a/src/Pure/Thy/thy_resources.scala	Wed Sep 05 09:36:17 2018 +0200
     1.2 +++ b/src/Pure/Thy/thy_resources.scala	Wed Sep 05 20:00:38 2018 +0200
     1.3 @@ -96,6 +96,32 @@
     1.4  
     1.5      /* theories */
     1.6  
     1.7 +    private sealed case class Use_Theories_State(
     1.8 +      last_update: Time = Time.now(),
     1.9 +      nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty,
    1.10 +      already_initialized: Set[Document.Node.Name] = Set.empty)
    1.11 +    {
    1.12 +      def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State =
    1.13 +        copy(last_update = Time.now(), nodes_status = new_nodes_status)
    1.14 +
    1.15 +      def watchdog(watchdog_timeout: Time): Boolean =
    1.16 +        watchdog_timeout > Time.zero && Time.now() - last_update > watchdog_timeout
    1.17 +
    1.18 +      def initialized_theories(
    1.19 +        state: Document.State,
    1.20 +        version: Document.Version,
    1.21 +        new_theories: List[Document.Node.Name]): (List[Document.Node.Name], Use_Theories_State) =
    1.22 +      {
    1.23 +        val initialized =
    1.24 +          for {
    1.25 +            name <- new_theories
    1.26 +            if !already_initialized(name) &&
    1.27 +              Document_Status.Node_Status.make(state, version, name).initialized
    1.28 +          } yield name
    1.29 +        (initialized, copy(already_initialized = already_initialized ++ initialized))
    1.30 +      }
    1.31 +    }
    1.32 +
    1.33      def use_theories(
    1.34        theories: List[String],
    1.35        qualifier: String = Sessions.DRAFT,
    1.36 @@ -116,23 +142,19 @@
    1.37        }
    1.38        val dep_theories_set = dep_theories.toSet
    1.39  
    1.40 -      val current_nodes_status = Synchronized(Document_Status.Nodes_Status.empty)
    1.41 -
    1.42 +      val use_theories_state = Synchronized(Use_Theories_State())
    1.43        val result = Future.promise[Theories_Result]
    1.44  
    1.45 -      var watchdog_time = Synchronized(Time.now())
    1.46 -      def watchdog: Boolean =
    1.47 -        watchdog_timeout > Time.zero && Time.now() - watchdog_time.value > watchdog_timeout
    1.48 -
    1.49        def check_state(beyond_limit: Boolean = false)
    1.50        {
    1.51          val state = session.current_state()
    1.52          state.stable_tip_version match {
    1.53            case Some(version) =>
    1.54 -            if (beyond_limit || watchdog ||
    1.55 +            val st = use_theories_state.value
    1.56 +            if (beyond_limit || st.watchdog(watchdog_timeout) ||
    1.57                  dep_theories.forall(name =>
    1.58                    state.node_consolidated(version, name) ||
    1.59 -                  current_nodes_status.value.quasi_consolidated(name)))
    1.60 +                  st.nodes_status.quasi_consolidated(name)))
    1.61              {
    1.62                val nodes =
    1.63                  for (name <- dep_theories)
    1.64 @@ -159,11 +181,9 @@
    1.65  
    1.66        val consumer =
    1.67        {
    1.68 -        val theories_progress = Synchronized(Set.empty[Document.Node.Name])
    1.69 -
    1.70          val delay_nodes_status =
    1.71            Standard_Thread.delay_first(nodes_status_delay max Time.zero) {
    1.72 -            progress.nodes_status(current_nodes_status.value)
    1.73 +            progress.nodes_status(use_theories_state.value.nodes_status)
    1.74            }
    1.75  
    1.76          Session.Consumer[Session.Commands_Changed](getClass.getName) {
    1.77 @@ -173,17 +193,15 @@
    1.78                val state = snapshot.state
    1.79                val version = snapshot.version
    1.80  
    1.81 -              watchdog_time.change(_ => Time.now())
    1.82 -
    1.83                val theory_percentages =
    1.84 -                current_nodes_status.change_result(nodes_status =>
    1.85 +                use_theories_state.change_result(st =>
    1.86                    {
    1.87                      val domain =
    1.88 -                      if (nodes_status.is_empty) dep_theories_set
    1.89 +                      if (st.nodes_status.is_empty) dep_theories_set
    1.90                        else changed.nodes.iterator.filter(dep_theories_set).toSet
    1.91  
    1.92                      val (nodes_status_changed, nodes_status1) =
    1.93 -                      nodes_status.update(resources.session_base, state, version,
    1.94 +                      st.nodes_status.update(resources.session_base, state, version,
    1.95                          domain = Some(domain), trim = changed.assignment)
    1.96  
    1.97                      if (nodes_status_delay >= Time.zero && nodes_status_changed) {
    1.98 @@ -195,27 +213,22 @@
    1.99                          (name, node_status) <- nodes_status1.present.iterator
   1.100                          if changed.nodes.contains(name)
   1.101                          p1 = node_status.percentage
   1.102 -                        if p1 > 0 && Some(p1) != nodes_status.get(name).map(_.percentage)
   1.103 +                        if p1 > 0 && Some(p1) != st.nodes_status.get(name).map(_.percentage)
   1.104                        } yield (name.theory, p1)).toList
   1.105  
   1.106 -                    (progress_percentage, nodes_status1)
   1.107 +                    (progress_percentage, st.update(nodes_status1))
   1.108                    })
   1.109  
   1.110                val check_theories =
   1.111                  (for {
   1.112                    command <- changed.commands.iterator
   1.113                    if dep_theories_set(command.node_name) && command.potentially_initialized
   1.114 -                } yield command.node_name).toSet
   1.115 +                } yield command.node_name).toList
   1.116  
   1.117                if (check_theories.nonEmpty) {
   1.118                  val initialized =
   1.119 -                  theories_progress.change_result(theories =>
   1.120 -                  {
   1.121 -                    val initialized =
   1.122 -                      (check_theories -- theories).toList.filter(name =>
   1.123 -                        Document_Status.Node_Status.make(state, version, name).initialized)
   1.124 -                    (initialized, theories ++ initialized)
   1.125 -                  })
   1.126 +                  use_theories_state.change_result(
   1.127 +                    _.initialized_theories(state, version, check_theories))
   1.128                  initialized.map(_.theory).sorted.foreach(progress.theory("", _))
   1.129                }
   1.130