merged
authorwenzelm
Sat Sep 08 16:55:38 2018 +0200 (10 months ago)
changeset 6895053f7b6b9f734
parent 68940 25b431feb2e9
parent 68949 e848328cb2c1
child 68951 a7b1fe2d30ad
merged
     1.1 --- a/src/Doc/System/Server.thy	Sat Sep 08 08:09:07 2018 +0000
     1.2 +++ b/src/Doc/System/Server.thy	Sat Sep 08 16:55:38 2018 +0200
     1.3 @@ -909,7 +909,7 @@
     1.4    \quad~~\<open>export_pattern?: string,\<close> \\
     1.5    \quad~~\<open>check_delay?: double,\<close>  & \<^bold>\<open>default:\<close> \<^verbatim>\<open>0.5\<close> \\
     1.6    \quad~~\<open>check_limit?: int,\<close> \\
     1.7 -  \quad~~\<open>watchdog_timeout?: double,\<close> \\
     1.8 +  \quad~~\<open>watchdog_timeout?: double,\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>600.0\<close> \\
     1.9    \quad~~\<open>nodes_status_delay?: double}\<close>  & \<^bold>\<open>default:\<close> \<^verbatim>\<open>-1.0\<close> \\
    1.10    \end{tabular}
    1.11  
     2.1 --- a/src/Pure/General/json.scala	Sat Sep 08 08:09:07 2018 +0000
     2.2 +++ b/src/Pure/General/json.scala	Sat Sep 08 16:55:38 2018 +0200
     2.3 @@ -309,6 +309,11 @@
     2.4            case _ => None
     2.5          }
     2.6      }
     2.7 +
     2.8 +    object Seconds {
     2.9 +      def unapply(json: T): Option[Time] =
    2.10 +        Double.unapply(json).map(Time.seconds(_))
    2.11 +    }
    2.12    }
    2.13  
    2.14  
    2.15 @@ -381,4 +386,9 @@
    2.16      list(obj, name, JSON.Value.String.unapply _)
    2.17    def strings_default(obj: T, name: String, default: => List[String] = Nil): Option[List[String]] =
    2.18      list_default(obj, name, JSON.Value.String.unapply _, default)
    2.19 +
    2.20 +  def seconds(obj: T, name: String): Option[Time] =
    2.21 +    value(obj, name, Value.Seconds.unapply)
    2.22 +  def seconds_default(obj: T, name: String, default: => Time = Time.zero): Option[Time] =
    2.23 +    value_default(obj, name, Value.Seconds.unapply, default)
    2.24  }
     3.1 --- a/src/Pure/General/value.scala	Sat Sep 08 08:09:07 2018 +0000
     3.2 +++ b/src/Pure/General/value.scala	Sat Sep 08 16:55:38 2018 +0200
     3.3 @@ -51,4 +51,16 @@
     3.4      def parse(s: java.lang.String): scala.Double =
     3.5        unapply(s) getOrElse error("Bad real: " + quote(s))
     3.6    }
     3.7 +
     3.8 +  object Seconds
     3.9 +  {
    3.10 +    def apply(t: Time): java.lang.String =
    3.11 +    {
    3.12 +      val s = t.seconds
    3.13 +      if (s.toInt.toDouble == s) s.toInt.toString else t.toString
    3.14 +    }
    3.15 +    def unapply(s: java.lang.String): Option[Time] = Double.unapply(s).map(Time.seconds(_))
    3.16 +    def parse(s: java.lang.String): Time =
    3.17 +      unapply(s) getOrElse error("Bad real (for seconds): " + quote(s))
    3.18 +  }
    3.19  }
     4.1 --- a/src/Pure/Thy/thy_resources.scala	Sat Sep 08 08:09:07 2018 +0000
     4.2 +++ b/src/Pure/Thy/thy_resources.scala	Sat Sep 08 16:55:38 2018 +0200
     4.3 @@ -78,9 +78,10 @@
     4.4        (nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok })
     4.5    }
     4.6  
     4.7 -  val default_check_delay: Double = 0.5
     4.8 -  val default_nodes_status_delay: Double = -1.0
     4.9 -  val default_commit_clean_delay: Double = 60.0
    4.10 +  val default_check_delay = Time.seconds(0.5)
    4.11 +  val default_nodes_status_delay = Time.seconds(-1.0)
    4.12 +  val default_commit_clean_delay = Time.seconds(60.0)
    4.13 +  val default_watchdog_timeout = Time.seconds(600.0)
    4.14  
    4.15  
    4.16    class Session private[Thy_Resources](
    4.17 @@ -152,18 +153,23 @@
    4.18        {
    4.19          val st1 =
    4.20            if (commit.isDefined) {
    4.21 -            val committed =
    4.22 -              for {
    4.23 -                name <- dep_theories
    4.24 -                if !already_committed.isDefinedAt(name) && state.node_consolidated(version, name)
    4.25 -              }
    4.26 -              yield {
    4.27 -                val snapshot = stable_snapshot(state, version, name)
    4.28 -                val status = Document_Status.Node_Status.make(state, version, name)
    4.29 -                commit.get.apply(snapshot, status)
    4.30 -                (name -> status)
    4.31 -              }
    4.32 -            copy(already_committed = already_committed ++ committed)
    4.33 +            val already_committed1 =
    4.34 +              (already_committed /: dep_theories)({ case (committed, name) =>
    4.35 +                def parents_committed: Boolean =
    4.36 +                  version.nodes(name).header.imports.forall({ case (parent, _) =>
    4.37 +                    Sessions.is_pure(parent.theory) || committed.isDefinedAt(parent)
    4.38 +                  })
    4.39 +                if (!committed.isDefinedAt(name) && parents_committed &&
    4.40 +                    state.node_consolidated(version, name))
    4.41 +                {
    4.42 +                  val snapshot = stable_snapshot(state, version, name)
    4.43 +                  val status = Document_Status.Node_Status.make(state, version, name)
    4.44 +                  commit.get.apply(snapshot, status)
    4.45 +                  committed + (name -> status)
    4.46 +                }
    4.47 +                else committed
    4.48 +              })
    4.49 +            copy(already_committed = already_committed1)
    4.50            }
    4.51            else this
    4.52  
    4.53 @@ -194,14 +200,14 @@
    4.54        theories: List[String],
    4.55        qualifier: String = Sessions.DRAFT,
    4.56        master_dir: String = "",
    4.57 -      check_delay: Time = Time.seconds(default_check_delay),
    4.58 +      check_delay: Time = default_check_delay,
    4.59        check_limit: Int = 0,
    4.60 -      watchdog_timeout: Time = Time.zero,
    4.61 -      nodes_status_delay: Time = Time.seconds(default_nodes_status_delay),
    4.62 +      watchdog_timeout: Time = default_watchdog_timeout,
    4.63 +      nodes_status_delay: Time = default_nodes_status_delay,
    4.64        id: UUID = UUID(),
    4.65        // commit: must not block, must not fail
    4.66        commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None,
    4.67 -      commit_clean_delay: Time = Time.seconds(default_commit_clean_delay),
    4.68 +      commit_clean_delay: Time = default_commit_clean_delay,
    4.69        progress: Progress = No_Progress): Theories_Result =
    4.70      {
    4.71        val dep_theories =
    4.72 @@ -303,7 +309,7 @@
    4.73  
    4.74                check_result()
    4.75  
    4.76 -              if (commit.isDefined && commit_clean_delay >= Time.zero) {
    4.77 +              if (commit.isDefined && commit_clean_delay > Time.zero) {
    4.78                  if (use_theories_state.value.finished_result)
    4.79                    delay_commit_clean.revoke
    4.80                  else delay_commit_clean.invoke
     5.1 --- a/src/Pure/Tools/dump.scala	Sat Sep 08 08:09:07 2018 +0000
     5.2 +++ b/src/Pure/Tools/dump.scala	Sat Sep 08 16:55:38 2018 +0200
     5.3 @@ -75,8 +75,7 @@
     5.4  
     5.5    /* dump */
     5.6  
     5.7 -  val default_output_dir = Path.explode("dump")
     5.8 -  val default_commit_clean_delay = Time.seconds(-1.0)
     5.9 +  val default_output_dir: Path = Path.explode("dump")
    5.10  
    5.11    def make_options(options: Options, aspects: List[Aspect]): Options =
    5.12    {
    5.13 @@ -92,7 +91,8 @@
    5.14      select_dirs: List[Path] = Nil,
    5.15      output_dir: Path = default_output_dir,
    5.16      verbose: Boolean = false,
    5.17 -    commit_clean_delay: Time = default_commit_clean_delay,
    5.18 +    commit_clean_delay: Time = Thy_Resources.default_commit_clean_delay,
    5.19 +    watchdog_timeout: Time = Thy_Resources.default_watchdog_timeout,
    5.20      system_mode: Boolean = false,
    5.21      selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
    5.22    {
    5.23 @@ -163,7 +163,8 @@
    5.24        session.use_theories(use_theories,
    5.25          progress = progress,
    5.26          commit = Some(Consumer.apply _),
    5.27 -        commit_clean_delay = commit_clean_delay)
    5.28 +        commit_clean_delay = commit_clean_delay,
    5.29 +        watchdog_timeout = watchdog_timeout)
    5.30  
    5.31      val session_result = session.stop()
    5.32  
    5.33 @@ -181,10 +182,11 @@
    5.34      {
    5.35        var aspects: List[Aspect] = known_aspects
    5.36        var base_sessions: List[String] = Nil
    5.37 -      var commit_clean_delay = default_commit_clean_delay
    5.38 +      var commit_clean_delay = Thy_Resources.default_commit_clean_delay
    5.39        var select_dirs: List[Path] = Nil
    5.40        var output_dir = default_output_dir
    5.41        var requirements = false
    5.42 +      var watchdog_timeout = Thy_Resources.default_watchdog_timeout
    5.43        var exclude_session_groups: List[String] = Nil
    5.44        var all_sessions = false
    5.45        var dirs: List[Path] = Nil
    5.46 @@ -201,11 +203,13 @@
    5.47    Options are:
    5.48      -A NAMES     dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
    5.49      -B NAME      include session NAME and all descendants
    5.50 -    -C SECONDS   delay for cleaning of already dumped theories (disabled for < 0, default: """ +
    5.51 -      default_commit_clean_delay.seconds.toInt + """)
    5.52 +    -C SECONDS   delay for cleaning of already dumped theories (0 = disabled, default: """ +
    5.53 +      Value.Seconds(Thy_Resources.default_commit_clean_delay) + """)
    5.54      -D DIR       include session directory and select its sessions
    5.55      -O DIR       output directory for dumped files (default: """ + default_output_dir + """)
    5.56      -R           operate on requirements of selected sessions
    5.57 +    -W SECONDS   watchdog timeout for PIDE processing (0 = disabled, default: """ +
    5.58 +      Value.Seconds(Thy_Resources.default_watchdog_timeout) + """)
    5.59      -X NAME      exclude sessions from group NAME and all descendants
    5.60      -a           select all sessions
    5.61      -d DIR       include session directory
    5.62 @@ -221,10 +225,11 @@
    5.63  """ + Library.prefix_lines("    ", show_aspects) + "\n",
    5.64        "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),
    5.65        "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
    5.66 -      "C:" -> (arg => commit_clean_delay = Time.seconds(Value.Double.parse(arg))),
    5.67 +      "C:" -> (arg => commit_clean_delay = Value.Seconds.parse(arg)),
    5.68        "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
    5.69        "O:" -> (arg => output_dir = Path.explode(arg)),
    5.70        "R" -> (_ => requirements = true),
    5.71 +      "W:" -> (arg => watchdog_timeout = Value.Seconds.parse(arg)),
    5.72        "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
    5.73        "a" -> (_ => all_sessions = true),
    5.74        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
    5.75 @@ -237,7 +242,7 @@
    5.76  
    5.77        val sessions = getopts(args)
    5.78  
    5.79 -      val progress = new Console_Progress(verbose = verbose)
    5.80 +      val progress = new Console_Progress()
    5.81        {
    5.82          override def theory_percentage(session: String, theory: String, percentage: Int)
    5.83          {
    5.84 @@ -250,11 +255,11 @@
    5.85            dump(options, logic,
    5.86              aspects = aspects,
    5.87              progress = progress,
    5.88 -            log = new File_Logger(Path.explode("$ISABELLE_HOME_USER/dump.log")),
    5.89              dirs = dirs,
    5.90              select_dirs = select_dirs,
    5.91              output_dir = output_dir,
    5.92              commit_clean_delay = commit_clean_delay,
    5.93 +            watchdog_timeout = watchdog_timeout,
    5.94              verbose = verbose,
    5.95              selection = Sessions.Selection(
    5.96                requirements = requirements,
     6.1 --- a/src/Pure/Tools/server_commands.scala	Sat Sep 08 08:09:07 2018 +0000
     6.2 +++ b/src/Pure/Tools/server_commands.scala	Sat Sep 08 16:55:38 2018 +0200
     6.3 @@ -158,10 +158,10 @@
     6.4        pretty_margin: Double = Pretty.default_margin,
     6.5        unicode_symbols: Boolean = false,
     6.6        export_pattern: String = "",
     6.7 -      check_delay: Double = Thy_Resources.default_check_delay,
     6.8 +      check_delay: Time = Thy_Resources.default_check_delay,
     6.9        check_limit: Int = 0,
    6.10 -      watchdog_timeout: Double = 0.0,
    6.11 -      nodes_status_delay: Double = Thy_Resources.default_nodes_status_delay)
    6.12 +      watchdog_timeout: Time = Thy_Resources.default_watchdog_timeout,
    6.13 +      nodes_status_delay: Time = Thy_Resources.default_nodes_status_delay)
    6.14  
    6.15      def unapply(json: JSON.T): Option[Args] =
    6.16        for {
    6.17 @@ -171,11 +171,12 @@
    6.18          pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin)
    6.19          unicode_symbols <- JSON.bool_default(json, "unicode_symbols")
    6.20          export_pattern <- JSON.string_default(json, "export_pattern")
    6.21 -        check_delay <- JSON.double_default(json, "check_delay", Thy_Resources.default_check_delay)
    6.22 +        check_delay <- JSON.seconds_default(json, "check_delay", Thy_Resources.default_check_delay)
    6.23          check_limit <- JSON.int_default(json, "check_limit")
    6.24 -        watchdog_timeout <- JSON.double_default(json, "watchdog_timeout")
    6.25 +        watchdog_timeout <-
    6.26 +          JSON.seconds_default(json, "watchdog_timeout", Thy_Resources.default_watchdog_timeout)
    6.27          nodes_status_delay <-
    6.28 -          JSON.double_default(json, "nodes_status_delay", Thy_Resources.default_nodes_status_delay)
    6.29 +          JSON.seconds_default(json, "nodes_status_delay", Thy_Resources.default_nodes_status_delay)
    6.30        }
    6.31        yield {
    6.32          Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin,
    6.33 @@ -191,9 +192,9 @@
    6.34      {
    6.35        val result =
    6.36          session.use_theories(args.theories, master_dir = args.master_dir,
    6.37 -          check_delay = Time.seconds(args.check_delay), check_limit = args.check_limit,
    6.38 -          watchdog_timeout = Time.seconds(args.watchdog_timeout),
    6.39 -          nodes_status_delay = Time.seconds(args.nodes_status_delay),
    6.40 +          check_delay = args.check_delay, check_limit = args.check_limit,
    6.41 +          watchdog_timeout = args.watchdog_timeout,
    6.42 +          nodes_status_delay = args.nodes_status_delay,
    6.43            id = id, progress = progress)
    6.44  
    6.45        def output_text(s: String): String =