# HG changeset patch
# User wenzelm
# Date 1532722167 -7200
# Node ID 03e104be99af3a34d8f042cbcc8d0484c81a4b0d
# Parent  a9bef20b1e476d41276cdfe289508eb5cbe61321
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);

diff -r a9bef20b1e47 -r 03e104be99af src/Doc/System/Server.thy
--- a/src/Doc/System/Server.thy	Fri Jul 27 17:32:16 2018 +0200
+++ b/src/Doc/System/Server.thy	Fri Jul 27 22:09:27 2018 +0200
@@ -894,7 +894,9 @@
   \quad~~\<open>master_dir?: string,\<close> & \<^bold>\<open>default:\<close> session \<open>tmp_dir\<close> \\
   \quad~~\<open>pretty_margin?: double,\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>76\<close> \\
   \quad~~\<open>unicode_symbols?: bool,\<close> \\
-  \quad~~\<open>export_pattern?: string}\<close> \\[2ex]
+  \quad~~\<open>export_pattern?: string,\<close> \\
+  \quad~~\<open>check_delay?: double,\<close>  & \<^bold>\<open>default:\<close> \<^verbatim>\<open>0.5\<close> \\
+  \quad~~\<open>check_limit?: int}\<close> \\
   \end{tabular}
 
   \begin{tabular}{ll}
@@ -929,6 +931,13 @@
   format of the \<open>body\<close> string: it is true for a byte vector that cannot be
   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.
 \<close>
 
 
diff -r a9bef20b1e47 -r 03e104be99af src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Fri Jul 27 17:32:16 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala	Fri Jul 27 22:09:27 2018 +0200
@@ -71,6 +71,9 @@
     }
   }
 
+  val default_use_theories_check_delay: Double = 0.5
+
+
   class Session private[Thy_Resources](
     session_name: String,
     session_options: Options,
@@ -96,6 +99,8 @@
       theories: List[String],
       qualifier: String = Sessions.DRAFT,
       master_dir: String = "",
+      check_delay: Time = Time.seconds(default_use_theories_check_delay),
+      check_limit: Int = 0,
       id: UUID = UUID(),
       progress: Progress = No_Progress): Theories_Result =
     {
@@ -105,23 +110,34 @@
 
       val result = Future.promise[Theories_Result]
 
-      def check_state
+      def check_state(beyond_limit: Boolean = false)
       {
         val state = session.current_state()
         state.stable_tip_version match {
-          case Some(version) if dep_theories.forall(state.node_consolidated(version, _)) =>
-            val nodes =
-              for (name <- dep_theories)
-              yield (name -> Protocol.node_status(state, version, name))
-            try { result.fulfill(new Theories_Result(state, version, nodes)) }
-            catch { case _: IllegalStateException => }
-          case _ =>
+          case Some(version) =>
+            if (beyond_limit || dep_theories.forall(state.node_consolidated(version, _))) {
+              val nodes =
+                for (name <- dep_theories)
+                yield (name -> Protocol.node_status(state, version, name))
+              try { result.fulfill(new Theories_Result(state, version, nodes)) }
+              catch { case _: IllegalStateException => }
+            }
+          case None =>
         }
       }
 
       val check_progress =
-        Event_Timer.request(Time.now(), repeat = Some(Time.seconds(0.5)))
-          { if (progress.stopped) result.cancel else check_state }
+      {
+        var check_count = 0
+        Event_Timer.request(Time.now(), repeat = Some(check_delay))
+          {
+            if (progress.stopped) result.cancel
+            else {
+              check_count += 1
+              check_state(check_limit > 0 && check_count > check_limit)
+            }
+          }
+      }
 
       val theories_progress = Synchronized(Set.empty[Document.Node.Name])
 
@@ -147,7 +163,7 @@
                 initialized.map(_.theory).sorted.foreach(progress.theory("", _))
               }
 
-              check_state
+              check_state()
             }
         }
 
diff -r a9bef20b1e47 -r 03e104be99af src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Fri Jul 27 17:32:16 2018 +0200
+++ b/src/Pure/Tools/server_commands.scala	Fri Jul 27 22:09:27 2018 +0200
@@ -157,7 +157,9 @@
       master_dir: String = "",
       pretty_margin: Double = Pretty.default_margin,
       unicode_symbols: Boolean = false,
-      export_pattern: String = "")
+      export_pattern: String = "",
+      check_delay: Double = Thy_Resources.default_use_theories_check_delay,
+      check_limit: Int = 0)
 
     def unapply(json: JSON.T): Option[Args] =
       for {
@@ -167,10 +169,14 @@
         pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin)
         unicode_symbols <- JSON.bool_default(json, "unicode_symbols")
         export_pattern <- JSON.string_default(json, "export_pattern")
+        check_delay <-
+          JSON.double_default(json, "check_delay", Thy_Resources.default_use_theories_check_delay)
+        check_limit <- JSON.int_default(json, "check_limit")
       }
       yield {
         Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin,
-          unicode_symbols = unicode_symbols, export_pattern = export_pattern)
+          unicode_symbols = unicode_symbols, export_pattern = export_pattern,
+          check_delay = check_delay, check_limit = check_limit)
       }
 
     def command(args: Args,
@@ -180,6 +186,7 @@
     {
       val result =
         session.use_theories(args.theories, master_dir = args.master_dir,
+          check_delay = Time.seconds(args.check_delay), check_limit = args.check_limit,
           id = id, progress = progress)
 
       def output_text(s: String): String =