clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
--- a/NEWS Sun Sep 02 20:51:07 2018 +0200
+++ b/NEWS Sun Sep 02 21:22:52 2018 +0200
@@ -58,6 +58,14 @@
observes the official standard).
+*** System ***
+
+* Isabelle Server message "use_theories" terminates more robustly in the
+presence of structurally broken sources: full consolidation of theories
+is no longer required.
+
+
+
New in Isabelle2018 (August 2018)
---------------------------------
--- a/src/Doc/System/Server.thy Sun Sep 02 20:51:07 2018 +0200
+++ b/src/Doc/System/Server.thy Sun Sep 02 21:22:52 2018 +0200
@@ -929,10 +929,9 @@
\<^medskip>
The \<^verbatim>\<open>use_theories\<close> command updates the identified session by adding the
current version of theory files to it, while dependencies are resolved
- implicitly. The command succeeds eventually, when all theories have been
- \<^emph>\<open>consolidated\<close> in the sense the formal \<open>node_status\<close>
- (\secref{sec:json-types}): the outermost command structure has finished (or
- failed) and the final \<^theory_text>\<open>end\<close> command of each theory has been checked.
+ implicitly. The command succeeds eventually, when all theories have status
+ \<^emph>\<open>terminated\<close> or \<^emph>\<open>consolidated\<close> in the sense of \<open>node_status\<close>
+ (\secref{sec:json-types}).
Already used theories persist in the session until purged explicitly
(\secref{sec:command-purge-theories}). This also means that repeated
@@ -948,14 +947,10 @@
represented as plain text in UTF-8 encoding, which means the string needs to
be decoded as in \<^verbatim>\<open>java.util.Base64.getDecoder.decode(String)\<close>.
- \<^medskip> Due to asynchronous nature of PIDE document processing, structurally
- broken theories never reach the \<open>consolidated\<close> state: consequently
- \<^verbatim>\<open>use_theories\<close> will wait forever. The status is checked every \<open>check_delay\<close>
- seconds, and bounded by \<open>check_limit\<close> attempts (default: 0, i.e.\
- unbounded). A \<open>check_limit > 0\<close> effectively specifies a timeout of
- \<open>check_delay \<times> check_limit\<close> seconds; it needs to be greater than the system
- option @{system_option editor_consolidate_delay} to give PIDE processing a
- chance to consolidate document nodes in the first place.
+ \<^medskip> The status of PIDE processing is checked every \<open>check_delay\<close> seconds, and
+ bounded by \<open>check_limit\<close> attempts (default: 0, i.e.\ unbounded). A
+ \<open>check_limit > 0\<close> effectively specifies a timeout of \<open>check_delay \<times>
+ check_limit\<close> seconds.
\<^medskip> A non-negative \<open>nodes_status_delay\<close> enables continuous notifications of
kind \<open>nodes_status\<close>, with a field of name and type \<open>nodes_status\<close>. The time
--- a/src/Pure/PIDE/document_status.scala Sun Sep 02 20:51:07 2018 +0200
+++ b/src/Pure/PIDE/document_status.scala Sun Sep 02 21:22:52 2018 +0200
@@ -192,6 +192,12 @@
def apply(name: Document.Node.Name): Node_Status = rep(name)
def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
+ def is_terminated(name: Document.Node.Name): Boolean =
+ rep.get(name) match {
+ case Some(st) => st.terminated
+ case None => false
+ }
+
def overall_node_status(name: Document.Node.Name): Overall_Node_Status.Value =
rep.get(name) match {
case Some(st) if st.consolidated =>
--- a/src/Pure/Thy/thy_resources.scala Sun Sep 02 20:51:07 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala Sun Sep 02 21:22:52 2018 +0200
@@ -111,6 +111,8 @@
master_dir = proper_string(master_dir) getOrElse tmp_dir_name, progress = progress)
val dep_theories_set = dep_theories.toSet
+ val nodes_status_update = Synchronized(Document_Status.Nodes_Status.empty_update)
+
val result = Future.promise[Theories_Result]
def check_state(beyond_limit: Boolean = false)
@@ -118,7 +120,11 @@
val state = session.current_state()
state.stable_tip_version match {
case Some(version) =>
- if (beyond_limit || dep_theories.forall(state.node_consolidated(version, _))) {
+ if (beyond_limit ||
+ dep_theories.forall(name =>
+ state.node_consolidated(version, name) ||
+ nodes_status_update.value._1.is_terminated(name)))
+ {
val nodes =
for (name <- dep_theories)
yield (name -> Document_Status.Node_Status.make(state, version, name))
@@ -144,8 +150,6 @@
val theories_progress = Synchronized(Set.empty[Document.Node.Name])
- val nodes_status_update = Synchronized(Document_Status.Nodes_Status.empty_update)
-
val delay_nodes_status =
Standard_Thread.delay_first(nodes_status_delay max Time.zero) {
val (nodes_status, names) = nodes_status_update.value
@@ -160,19 +164,19 @@
val state = snapshot.state
val version = snapshot.version
- if (nodes_status_delay >= Time.zero) {
- nodes_status_update.change(
- { case upd @ (nodes_status, _) =>
- val domain =
- if (nodes_status.is_empty) dep_theories_set
- else changed.nodes.iterator.filter(dep_theories_set).toSet
- val upd1 =
- nodes_status.update(resources.session_base, state, version,
- domain = Some(domain), trim = changed.assignment).getOrElse(upd)
- if (upd == upd1) upd
- else { delay_nodes_status.invoke; upd1 }
- })
- }
+ nodes_status_update.change(
+ { case upd @ (nodes_status, _) =>
+ val domain =
+ if (nodes_status.is_empty) dep_theories_set
+ else changed.nodes.iterator.filter(dep_theories_set).toSet
+ val upd1 =
+ nodes_status.update(resources.session_base, state, version,
+ domain = Some(domain), trim = changed.assignment).getOrElse(upd)
+ if (nodes_status_delay >= Time.zero && upd != upd1)
+ delay_nodes_status.invoke
+
+ upd1
+ })
val check_theories =
(for {