clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
authorwenzelm
Sun Sep 02 21:22:52 2018 +0200 (14 months ago ago)
changeset 688833653b3ad729e
parent 68882 344a4a8847be
child 68884 9b97d0b20d95
clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
NEWS
src/Doc/System/Server.thy
src/Pure/PIDE/document_status.scala
src/Pure/Thy/thy_resources.scala
     1.1 --- a/NEWS	Sun Sep 02 20:51:07 2018 +0200
     1.2 +++ b/NEWS	Sun Sep 02 21:22:52 2018 +0200
     1.3 @@ -58,6 +58,14 @@
     1.4  observes the official standard).
     1.5  
     1.6  
     1.7 +*** System ***
     1.8 +
     1.9 +* Isabelle Server message "use_theories" terminates more robustly in the
    1.10 +presence of structurally broken sources: full consolidation of theories
    1.11 +is no longer required.
    1.12 +
    1.13 +
    1.14 +
    1.15  New in Isabelle2018 (August 2018)
    1.16  ---------------------------------
    1.17  
     2.1 --- a/src/Doc/System/Server.thy	Sun Sep 02 20:51:07 2018 +0200
     2.2 +++ b/src/Doc/System/Server.thy	Sun Sep 02 21:22:52 2018 +0200
     2.3 @@ -929,10 +929,9 @@
     2.4    \<^medskip>
     2.5    The \<^verbatim>\<open>use_theories\<close> command updates the identified session by adding the
     2.6    current version of theory files to it, while dependencies are resolved
     2.7 -  implicitly. The command succeeds eventually, when all theories have been
     2.8 -  \<^emph>\<open>consolidated\<close> in the sense the formal \<open>node_status\<close>
     2.9 -  (\secref{sec:json-types}): the outermost command structure has finished (or
    2.10 -  failed) and the final \<^theory_text>\<open>end\<close> command of each theory has been checked.
    2.11 +  implicitly. The command succeeds eventually, when all theories have status
    2.12 +  \<^emph>\<open>terminated\<close> or \<^emph>\<open>consolidated\<close> in the sense of \<open>node_status\<close>
    2.13 +  (\secref{sec:json-types}).
    2.14  
    2.15    Already used theories persist in the session until purged explicitly
    2.16    (\secref{sec:command-purge-theories}). This also means that repeated
    2.17 @@ -948,14 +947,10 @@
    2.18    represented as plain text in UTF-8 encoding, which means the string needs to
    2.19    be decoded as in \<^verbatim>\<open>java.util.Base64.getDecoder.decode(String)\<close>.
    2.20  
    2.21 -  \<^medskip> Due to asynchronous nature of PIDE document processing, structurally
    2.22 -  broken theories never reach the \<open>consolidated\<close> state: consequently
    2.23 -  \<^verbatim>\<open>use_theories\<close> will wait forever. The status is checked every \<open>check_delay\<close>
    2.24 -  seconds, and bounded by \<open>check_limit\<close> attempts (default: 0, i.e.\
    2.25 -  unbounded). A \<open>check_limit > 0\<close> effectively specifies a timeout of
    2.26 -  \<open>check_delay \<times> check_limit\<close> seconds; it needs to be greater than the system
    2.27 -  option @{system_option editor_consolidate_delay} to give PIDE processing a
    2.28 -  chance to consolidate document nodes in the first place.
    2.29 +  \<^medskip> The status of PIDE processing is checked every \<open>check_delay\<close> seconds, and
    2.30 +  bounded by \<open>check_limit\<close> attempts (default: 0, i.e.\ unbounded). A
    2.31 +  \<open>check_limit > 0\<close> effectively specifies a timeout of \<open>check_delay \<times>
    2.32 +  check_limit\<close> seconds.
    2.33  
    2.34    \<^medskip> A non-negative \<open>nodes_status_delay\<close> enables continuous notifications of
    2.35    kind \<open>nodes_status\<close>, with a field of name and type \<open>nodes_status\<close>. The time
     3.1 --- a/src/Pure/PIDE/document_status.scala	Sun Sep 02 20:51:07 2018 +0200
     3.2 +++ b/src/Pure/PIDE/document_status.scala	Sun Sep 02 21:22:52 2018 +0200
     3.3 @@ -192,6 +192,12 @@
     3.4      def apply(name: Document.Node.Name): Node_Status = rep(name)
     3.5      def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
     3.6  
     3.7 +    def is_terminated(name: Document.Node.Name): Boolean =
     3.8 +      rep.get(name) match {
     3.9 +        case Some(st) => st.terminated
    3.10 +        case None => false
    3.11 +      }
    3.12 +
    3.13      def overall_node_status(name: Document.Node.Name): Overall_Node_Status.Value =
    3.14        rep.get(name) match {
    3.15          case Some(st) if st.consolidated =>
     4.1 --- a/src/Pure/Thy/thy_resources.scala	Sun Sep 02 20:51:07 2018 +0200
     4.2 +++ b/src/Pure/Thy/thy_resources.scala	Sun Sep 02 21:22:52 2018 +0200
     4.3 @@ -111,6 +111,8 @@
     4.4            master_dir = proper_string(master_dir) getOrElse tmp_dir_name, progress = progress)
     4.5        val dep_theories_set = dep_theories.toSet
     4.6  
     4.7 +      val nodes_status_update = Synchronized(Document_Status.Nodes_Status.empty_update)
     4.8 +
     4.9        val result = Future.promise[Theories_Result]
    4.10  
    4.11        def check_state(beyond_limit: Boolean = false)
    4.12 @@ -118,7 +120,11 @@
    4.13          val state = session.current_state()
    4.14          state.stable_tip_version match {
    4.15            case Some(version) =>
    4.16 -            if (beyond_limit || dep_theories.forall(state.node_consolidated(version, _))) {
    4.17 +            if (beyond_limit ||
    4.18 +                dep_theories.forall(name =>
    4.19 +                  state.node_consolidated(version, name) ||
    4.20 +                  nodes_status_update.value._1.is_terminated(name)))
    4.21 +            {
    4.22                val nodes =
    4.23                  for (name <- dep_theories)
    4.24                  yield (name -> Document_Status.Node_Status.make(state, version, name))
    4.25 @@ -144,8 +150,6 @@
    4.26  
    4.27        val theories_progress = Synchronized(Set.empty[Document.Node.Name])
    4.28  
    4.29 -      val nodes_status_update = Synchronized(Document_Status.Nodes_Status.empty_update)
    4.30 -
    4.31        val delay_nodes_status =
    4.32          Standard_Thread.delay_first(nodes_status_delay max Time.zero) {
    4.33            val (nodes_status, names) = nodes_status_update.value
    4.34 @@ -160,19 +164,19 @@
    4.35                val state = snapshot.state
    4.36                val version = snapshot.version
    4.37  
    4.38 -              if (nodes_status_delay >= Time.zero) {
    4.39 -                nodes_status_update.change(
    4.40 -                  { case upd @ (nodes_status, _) =>
    4.41 -                      val domain =
    4.42 -                        if (nodes_status.is_empty) dep_theories_set
    4.43 -                        else changed.nodes.iterator.filter(dep_theories_set).toSet
    4.44 -                      val upd1 =
    4.45 -                        nodes_status.update(resources.session_base, state, version,
    4.46 -                          domain = Some(domain), trim = changed.assignment).getOrElse(upd)
    4.47 -                      if (upd == upd1) upd
    4.48 -                      else { delay_nodes_status.invoke; upd1 }
    4.49 -                  })
    4.50 -              }
    4.51 +              nodes_status_update.change(
    4.52 +                { case upd @ (nodes_status, _) =>
    4.53 +                    val domain =
    4.54 +                      if (nodes_status.is_empty) dep_theories_set
    4.55 +                      else changed.nodes.iterator.filter(dep_theories_set).toSet
    4.56 +                    val upd1 =
    4.57 +                      nodes_status.update(resources.session_base, state, version,
    4.58 +                        domain = Some(domain), trim = changed.assignment).getOrElse(upd)
    4.59 +                    if (nodes_status_delay >= Time.zero && upd != upd1)
    4.60 +                      delay_nodes_status.invoke
    4.61 +
    4.62 +                    upd1
    4.63 +                })
    4.64  
    4.65                val check_theories =
    4.66                  (for {