# HG changeset patch # User wenzelm # Date 1535916172 -7200 # Node ID 3653b3ad729efc380c70b69e5d21b618e0ac7dd9 # Parent 344a4a8847befc0fa353ca735a08850222fb4dad clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient; diff -r 344a4a8847be -r 3653b3ad729e NEWS --- 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) --------------------------------- diff -r 344a4a8847be -r 3653b3ad729e src/Doc/System/Server.thy --- 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>\use_theories\ 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>\consolidated\ in the sense the formal \node_status\ - (\secref{sec:json-types}): the outermost command structure has finished (or - failed) and the final \<^theory_text>\end\ command of each theory has been checked. + implicitly. The command succeeds eventually, when all theories have status + \<^emph>\terminated\ or \<^emph>\consolidated\ in the sense of \node_status\ + (\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>\java.util.Base64.getDecoder.decode(String)\. - \<^medskip> Due to asynchronous nature of PIDE document processing, structurally - broken theories never reach the \consolidated\ state: consequently - \<^verbatim>\use_theories\ will wait forever. The status is checked every \check_delay\ - seconds, and bounded by \check_limit\ attempts (default: 0, i.e.\ - unbounded). A \check_limit > 0\ effectively specifies a timeout of - \check_delay \ check_limit\ 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 \check_delay\ seconds, and + bounded by \check_limit\ attempts (default: 0, i.e.\ unbounded). A + \check_limit > 0\ effectively specifies a timeout of \check_delay \ + check_limit\ seconds. \<^medskip> A non-negative \nodes_status_delay\ enables continuous notifications of kind \nodes_status\, with a field of name and type \nodes_status\. The time diff -r 344a4a8847be -r 3653b3ad729e src/Pure/PIDE/document_status.scala --- 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 => diff -r 344a4a8847be -r 3653b3ad729e src/Pure/Thy/thy_resources.scala --- 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 {