# HG changeset patch
# User wenzelm
# Date 1536418538 -7200
# Node ID 53f7b6b9f73422750166af6a96c0d5e3fc0b5367
# Parent  25b431feb2e9df0eaae67c34d14caa1f43ae9cc3# Parent  e848328cb2c11c19211669944e29611efdc89074
merged

diff -r 25b431feb2e9 -r 53f7b6b9f734 src/Doc/System/Server.thy
--- a/src/Doc/System/Server.thy	Sat Sep 08 08:09:07 2018 +0000
+++ b/src/Doc/System/Server.thy	Sat Sep 08 16:55:38 2018 +0200
@@ -909,7 +909,7 @@
   \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> \\
-  \quad~~\<open>watchdog_timeout?: double,\<close> \\
+  \quad~~\<open>watchdog_timeout?: double,\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>600.0\<close> \\
   \quad~~\<open>nodes_status_delay?: double}\<close>  & \<^bold>\<open>default:\<close> \<^verbatim>\<open>-1.0\<close> \\
   \end{tabular}
 
diff -r 25b431feb2e9 -r 53f7b6b9f734 src/Pure/General/json.scala
--- a/src/Pure/General/json.scala	Sat Sep 08 08:09:07 2018 +0000
+++ b/src/Pure/General/json.scala	Sat Sep 08 16:55:38 2018 +0200
@@ -309,6 +309,11 @@
           case _ => None
         }
     }
+
+    object Seconds {
+      def unapply(json: T): Option[Time] =
+        Double.unapply(json).map(Time.seconds(_))
+    }
   }
 
 
@@ -381,4 +386,9 @@
     list(obj, name, JSON.Value.String.unapply _)
   def strings_default(obj: T, name: String, default: => List[String] = Nil): Option[List[String]] =
     list_default(obj, name, JSON.Value.String.unapply _, default)
+
+  def seconds(obj: T, name: String): Option[Time] =
+    value(obj, name, Value.Seconds.unapply)
+  def seconds_default(obj: T, name: String, default: => Time = Time.zero): Option[Time] =
+    value_default(obj, name, Value.Seconds.unapply, default)
 }
diff -r 25b431feb2e9 -r 53f7b6b9f734 src/Pure/General/value.scala
--- a/src/Pure/General/value.scala	Sat Sep 08 08:09:07 2018 +0000
+++ b/src/Pure/General/value.scala	Sat Sep 08 16:55:38 2018 +0200
@@ -51,4 +51,16 @@
     def parse(s: java.lang.String): scala.Double =
       unapply(s) getOrElse error("Bad real: " + quote(s))
   }
+
+  object Seconds
+  {
+    def apply(t: Time): java.lang.String =
+    {
+      val s = t.seconds
+      if (s.toInt.toDouble == s) s.toInt.toString else t.toString
+    }
+    def unapply(s: java.lang.String): Option[Time] = Double.unapply(s).map(Time.seconds(_))
+    def parse(s: java.lang.String): Time =
+      unapply(s) getOrElse error("Bad real (for seconds): " + quote(s))
+  }
 }
diff -r 25b431feb2e9 -r 53f7b6b9f734 src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Sat Sep 08 08:09:07 2018 +0000
+++ b/src/Pure/Thy/thy_resources.scala	Sat Sep 08 16:55:38 2018 +0200
@@ -78,9 +78,10 @@
       (nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok })
   }
 
-  val default_check_delay: Double = 0.5
-  val default_nodes_status_delay: Double = -1.0
-  val default_commit_clean_delay: Double = 60.0
+  val default_check_delay = Time.seconds(0.5)
+  val default_nodes_status_delay = Time.seconds(-1.0)
+  val default_commit_clean_delay = Time.seconds(60.0)
+  val default_watchdog_timeout = Time.seconds(600.0)
 
 
   class Session private[Thy_Resources](
@@ -152,18 +153,23 @@
       {
         val st1 =
           if (commit.isDefined) {
-            val committed =
-              for {
-                name <- dep_theories
-                if !already_committed.isDefinedAt(name) && state.node_consolidated(version, name)
-              }
-              yield {
-                val snapshot = stable_snapshot(state, version, name)
-                val status = Document_Status.Node_Status.make(state, version, name)
-                commit.get.apply(snapshot, status)
-                (name -> status)
-              }
-            copy(already_committed = already_committed ++ committed)
+            val already_committed1 =
+              (already_committed /: dep_theories)({ case (committed, name) =>
+                def parents_committed: Boolean =
+                  version.nodes(name).header.imports.forall({ case (parent, _) =>
+                    Sessions.is_pure(parent.theory) || committed.isDefinedAt(parent)
+                  })
+                if (!committed.isDefinedAt(name) && parents_committed &&
+                    state.node_consolidated(version, name))
+                {
+                  val snapshot = stable_snapshot(state, version, name)
+                  val status = Document_Status.Node_Status.make(state, version, name)
+                  commit.get.apply(snapshot, status)
+                  committed + (name -> status)
+                }
+                else committed
+              })
+            copy(already_committed = already_committed1)
           }
           else this
 
@@ -194,14 +200,14 @@
       theories: List[String],
       qualifier: String = Sessions.DRAFT,
       master_dir: String = "",
-      check_delay: Time = Time.seconds(default_check_delay),
+      check_delay: Time = default_check_delay,
       check_limit: Int = 0,
-      watchdog_timeout: Time = Time.zero,
-      nodes_status_delay: Time = Time.seconds(default_nodes_status_delay),
+      watchdog_timeout: Time = default_watchdog_timeout,
+      nodes_status_delay: Time = default_nodes_status_delay,
       id: UUID = UUID(),
       // commit: must not block, must not fail
       commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None,
-      commit_clean_delay: Time = Time.seconds(default_commit_clean_delay),
+      commit_clean_delay: Time = default_commit_clean_delay,
       progress: Progress = No_Progress): Theories_Result =
     {
       val dep_theories =
@@ -303,7 +309,7 @@
 
               check_result()
 
-              if (commit.isDefined && commit_clean_delay >= Time.zero) {
+              if (commit.isDefined && commit_clean_delay > Time.zero) {
                 if (use_theories_state.value.finished_result)
                   delay_commit_clean.revoke
                 else delay_commit_clean.invoke
diff -r 25b431feb2e9 -r 53f7b6b9f734 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Sat Sep 08 08:09:07 2018 +0000
+++ b/src/Pure/Tools/dump.scala	Sat Sep 08 16:55:38 2018 +0200
@@ -75,8 +75,7 @@
 
   /* dump */
 
-  val default_output_dir = Path.explode("dump")
-  val default_commit_clean_delay = Time.seconds(-1.0)
+  val default_output_dir: Path = Path.explode("dump")
 
   def make_options(options: Options, aspects: List[Aspect]): Options =
   {
@@ -92,7 +91,8 @@
     select_dirs: List[Path] = Nil,
     output_dir: Path = default_output_dir,
     verbose: Boolean = false,
-    commit_clean_delay: Time = default_commit_clean_delay,
+    commit_clean_delay: Time = Thy_Resources.default_commit_clean_delay,
+    watchdog_timeout: Time = Thy_Resources.default_watchdog_timeout,
     system_mode: Boolean = false,
     selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
   {
@@ -163,7 +163,8 @@
       session.use_theories(use_theories,
         progress = progress,
         commit = Some(Consumer.apply _),
-        commit_clean_delay = commit_clean_delay)
+        commit_clean_delay = commit_clean_delay,
+        watchdog_timeout = watchdog_timeout)
 
     val session_result = session.stop()
 
@@ -181,10 +182,11 @@
     {
       var aspects: List[Aspect] = known_aspects
       var base_sessions: List[String] = Nil
-      var commit_clean_delay = default_commit_clean_delay
+      var commit_clean_delay = Thy_Resources.default_commit_clean_delay
       var select_dirs: List[Path] = Nil
       var output_dir = default_output_dir
       var requirements = false
+      var watchdog_timeout = Thy_Resources.default_watchdog_timeout
       var exclude_session_groups: List[String] = Nil
       var all_sessions = false
       var dirs: List[Path] = Nil
@@ -201,11 +203,13 @@
   Options are:
     -A NAMES     dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
     -B NAME      include session NAME and all descendants
-    -C SECONDS   delay for cleaning of already dumped theories (disabled for < 0, default: """ +
-      default_commit_clean_delay.seconds.toInt + """)
+    -C SECONDS   delay for cleaning of already dumped theories (0 = disabled, default: """ +
+      Value.Seconds(Thy_Resources.default_commit_clean_delay) + """)
     -D DIR       include session directory and select its sessions
     -O DIR       output directory for dumped files (default: """ + default_output_dir + """)
     -R           operate on requirements of selected sessions
+    -W SECONDS   watchdog timeout for PIDE processing (0 = disabled, default: """ +
+      Value.Seconds(Thy_Resources.default_watchdog_timeout) + """)
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions
     -d DIR       include session directory
@@ -221,10 +225,11 @@
 """ + Library.prefix_lines("    ", show_aspects) + "\n",
       "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),
       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
-      "C:" -> (arg => commit_clean_delay = Time.seconds(Value.Double.parse(arg))),
+      "C:" -> (arg => commit_clean_delay = Value.Seconds.parse(arg)),
       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
       "O:" -> (arg => output_dir = Path.explode(arg)),
       "R" -> (_ => requirements = true),
+      "W:" -> (arg => watchdog_timeout = Value.Seconds.parse(arg)),
       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
       "a" -> (_ => all_sessions = true),
       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
@@ -237,7 +242,7 @@
 
       val sessions = getopts(args)
 
-      val progress = new Console_Progress(verbose = verbose)
+      val progress = new Console_Progress()
       {
         override def theory_percentage(session: String, theory: String, percentage: Int)
         {
@@ -250,11 +255,11 @@
           dump(options, logic,
             aspects = aspects,
             progress = progress,
-            log = new File_Logger(Path.explode("$ISABELLE_HOME_USER/dump.log")),
             dirs = dirs,
             select_dirs = select_dirs,
             output_dir = output_dir,
             commit_clean_delay = commit_clean_delay,
+            watchdog_timeout = watchdog_timeout,
             verbose = verbose,
             selection = Sessions.Selection(
               requirements = requirements,
diff -r 25b431feb2e9 -r 53f7b6b9f734 src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Sat Sep 08 08:09:07 2018 +0000
+++ b/src/Pure/Tools/server_commands.scala	Sat Sep 08 16:55:38 2018 +0200
@@ -158,10 +158,10 @@
       pretty_margin: Double = Pretty.default_margin,
       unicode_symbols: Boolean = false,
       export_pattern: String = "",
-      check_delay: Double = Thy_Resources.default_check_delay,
+      check_delay: Time = Thy_Resources.default_check_delay,
       check_limit: Int = 0,
-      watchdog_timeout: Double = 0.0,
-      nodes_status_delay: Double = Thy_Resources.default_nodes_status_delay)
+      watchdog_timeout: Time = Thy_Resources.default_watchdog_timeout,
+      nodes_status_delay: Time = Thy_Resources.default_nodes_status_delay)
 
     def unapply(json: JSON.T): Option[Args] =
       for {
@@ -171,11 +171,12 @@
         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_check_delay)
+        check_delay <- JSON.seconds_default(json, "check_delay", Thy_Resources.default_check_delay)
         check_limit <- JSON.int_default(json, "check_limit")
-        watchdog_timeout <- JSON.double_default(json, "watchdog_timeout")
+        watchdog_timeout <-
+          JSON.seconds_default(json, "watchdog_timeout", Thy_Resources.default_watchdog_timeout)
         nodes_status_delay <-
-          JSON.double_default(json, "nodes_status_delay", Thy_Resources.default_nodes_status_delay)
+          JSON.seconds_default(json, "nodes_status_delay", Thy_Resources.default_nodes_status_delay)
       }
       yield {
         Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin,
@@ -191,9 +192,9 @@
     {
       val result =
         session.use_theories(args.theories, master_dir = args.master_dir,
-          check_delay = Time.seconds(args.check_delay), check_limit = args.check_limit,
-          watchdog_timeout = Time.seconds(args.watchdog_timeout),
-          nodes_status_delay = Time.seconds(args.nodes_status_delay),
+          check_delay = args.check_delay, check_limit = args.check_limit,
+          watchdog_timeout = args.watchdog_timeout,
+          nodes_status_delay = args.nodes_status_delay,
           id = id, progress = progress)
 
       def output_text(s: String): String =