clarified defaults via system options;
authorwenzelm
Thu Dec 27 16:56:53 2018 +0100 (7 months ago ago)
changeset 6953216779868de1f
parent 69518 7d59af98af29
child 69533 0428fd0a13b7
clarified defaults via system options;
etc/options
src/Pure/PIDE/headless.scala
src/Pure/Tools/dump.scala
src/Pure/Tools/server_commands.scala
     1.1 --- a/etc/options	Wed Dec 26 20:57:23 2018 +0100
     1.2 +++ b/etc/options	Thu Dec 27 16:56:53 2018 +0100
     1.3 @@ -144,7 +144,7 @@
     1.4    -- "ML process command prefix (process policy)"
     1.5  
     1.6  
     1.7 -section "Editor Reactivity"
     1.8 +section "Editor Session"
     1.9  
    1.10  public option editor_load_delay : real = 0.5
    1.11    -- "delay for file load operations (new buffers etc.)"
    1.12 @@ -195,6 +195,24 @@
    1.13    -- "dynamic presentation while editing"
    1.14  
    1.15  
    1.16 +section "Headless Session"
    1.17 +
    1.18 +option headless_check_delay : real = 0.5
    1.19 +  -- "delay for theory status check during PIDE processing (seconds)"
    1.20 +
    1.21 +option headless_check_limit : int = 0
    1.22 +  -- "maximum number of theory status checks (0 = unlimited)"
    1.23 +
    1.24 +option headless_nodes_status_delay : real = -1
    1.25 +  -- "delay for overall nodes status check during PIDE processing (seconds, disabled for < 0)"
    1.26 +
    1.27 +option headless_watchdog_timeout : real = 600
    1.28 +  -- "watchdog timeout for PIDE processing of broken theories (seconds, 0 = disabled)"
    1.29 +
    1.30 +option headless_commit_cleanup_delay : real = 60
    1.31 +  -- "delay for cleanup of already imported theories (seconds, 0 = disabled)"
    1.32 +
    1.33 +
    1.34  section "Miscellaneous Tools"
    1.35  
    1.36  public option find_theorems_limit : int = 40
     2.1 --- a/src/Pure/PIDE/headless.scala	Wed Dec 26 20:57:23 2018 +0100
     2.2 +++ b/src/Pure/PIDE/headless.scala	Thu Dec 27 16:56:53 2018 +0100
     2.3 @@ -84,18 +84,21 @@
     2.4        (nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok })
     2.5    }
     2.6  
     2.7 -  val default_check_delay = Time.seconds(0.5)
     2.8 -  val default_nodes_status_delay = Time.seconds(-1.0)
     2.9 -  val default_commit_cleanup_delay = Time.seconds(60.0)
    2.10 -  val default_watchdog_timeout = Time.seconds(600.0)
    2.11 +  class Session private[Headless](
    2.12 +    session_name: String,
    2.13 +    _session_options: => Options,
    2.14 +    override val resources: Resources) extends isabelle.Session(_session_options, resources)
    2.15 +  {
    2.16 +    session =>
    2.17  
    2.18  
    2.19 -  class Session private[Headless](
    2.20 -    session_name: String,
    2.21 -    session_options: Options,
    2.22 -    override val resources: Resources) extends isabelle.Session(session_options, resources)
    2.23 -  {
    2.24 -    session =>
    2.25 +    /* options */
    2.26 +
    2.27 +    def default_check_delay: Time = session_options.seconds("headless_check_delay")
    2.28 +    def default_check_limit: Int = session_options.int("headless_check_limit")
    2.29 +    def default_nodes_status_delay: Time = session_options.seconds("headless_nodes_status_delay")
    2.30 +    def default_watchdog_timeout: Time = session_options.seconds("headless_watchdog_timeout")
    2.31 +    def default_commit_cleanup_delay: Time = session_options.seconds("headless_commit_cleanup_delay")
    2.32  
    2.33  
    2.34      /* temporary directory */
    2.35 @@ -190,7 +193,7 @@
    2.36        qualifier: String = Sessions.DRAFT,
    2.37        master_dir: String = "",
    2.38        check_delay: Time = default_check_delay,
    2.39 -      check_limit: Int = 0,
    2.40 +      check_limit: Int = default_check_limit,
    2.41        watchdog_timeout: Time = default_watchdog_timeout,
    2.42        nodes_status_delay: Time = default_nodes_status_delay,
    2.43        id: UUID.T = UUID.random(),
     3.1 --- a/src/Pure/Tools/dump.scala	Wed Dec 26 20:57:23 2018 +0100
     3.2 +++ b/src/Pure/Tools/dump.scala	Thu Dec 27 16:56:53 2018 +0100
     3.3 @@ -94,8 +94,6 @@
     3.4      select_dirs: List[Path] = Nil,
     3.5      output_dir: Path = default_output_dir,
     3.6      verbose: Boolean = false,
     3.7 -    commit_cleanup_delay: Time = Headless.default_commit_cleanup_delay,
     3.8 -    watchdog_timeout: Time = Headless.default_watchdog_timeout,
     3.9      system_mode: Boolean = false,
    3.10      selection: Sessions.Selection = Sessions.Selection.empty): Boolean =
    3.11    {
    3.12 @@ -163,11 +161,7 @@
    3.13          include_sessions = include_sessions, progress = progress, log = log)
    3.14  
    3.15      val use_theories_result =
    3.16 -      session.use_theories(use_theories,
    3.17 -        progress = progress,
    3.18 -        commit = Some(Consumer.apply _),
    3.19 -        commit_cleanup_delay = commit_cleanup_delay,
    3.20 -        watchdog_timeout = watchdog_timeout)
    3.21 +      session.use_theories(use_theories, progress = progress, commit = Some(Consumer.apply _))
    3.22  
    3.23      session.stop()
    3.24  
    3.25 @@ -189,11 +183,9 @@
    3.26      {
    3.27        var aspects: List[Aspect] = known_aspects
    3.28        var base_sessions: List[String] = Nil
    3.29 -      var commit_cleanup_delay = Headless.default_commit_cleanup_delay
    3.30        var select_dirs: List[Path] = Nil
    3.31        var output_dir = default_output_dir
    3.32        var requirements = false
    3.33 -      var watchdog_timeout = Headless.default_watchdog_timeout
    3.34        var exclude_session_groups: List[String] = Nil
    3.35        var all_sessions = false
    3.36        var dirs: List[Path] = Nil
    3.37 @@ -210,13 +202,9 @@
    3.38    Options are:
    3.39      -A NAMES     dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
    3.40      -B NAME      include session NAME and all descendants
    3.41 -    -C SECONDS   delay for cleaning of already dumped theories (0 = disabled, default: """ +
    3.42 -      Value.Seconds(Headless.default_commit_cleanup_delay) + """)
    3.43      -D DIR       include session directory and select its sessions
    3.44      -O DIR       output directory for dumped files (default: """ + default_output_dir + """)
    3.45      -R           operate on requirements of selected sessions
    3.46 -    -W SECONDS   watchdog timeout for PIDE processing (0 = disabled, default: """ +
    3.47 -      Value.Seconds(Headless.default_watchdog_timeout) + """)
    3.48      -X NAME      exclude sessions from group NAME and all descendants
    3.49      -a           select all sessions
    3.50      -d DIR       include session directory
    3.51 @@ -232,11 +220,9 @@
    3.52  """ + Library.prefix_lines("    ", show_aspects) + "\n",
    3.53        "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),
    3.54        "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
    3.55 -      "C:" -> (arg => commit_cleanup_delay = Value.Seconds.parse(arg)),
    3.56        "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
    3.57        "O:" -> (arg => output_dir = Path.explode(arg)),
    3.58        "R" -> (_ => requirements = true),
    3.59 -      "W:" -> (arg => watchdog_timeout = Value.Seconds.parse(arg)),
    3.60        "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
    3.61        "a" -> (_ => all_sessions = true),
    3.62        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
    3.63 @@ -259,8 +245,6 @@
    3.64              dirs = dirs,
    3.65              select_dirs = select_dirs,
    3.66              output_dir = output_dir,
    3.67 -            commit_cleanup_delay = commit_cleanup_delay,
    3.68 -            watchdog_timeout = watchdog_timeout,
    3.69              verbose = verbose,
    3.70              selection = Sessions.Selection(
    3.71                requirements = requirements,
     4.1 --- a/src/Pure/Tools/server_commands.scala	Wed Dec 26 20:57:23 2018 +0100
     4.2 +++ b/src/Pure/Tools/server_commands.scala	Thu Dec 27 16:56:53 2018 +0100
     4.3 @@ -158,10 +158,11 @@
     4.4        pretty_margin: Double = Pretty.default_margin,
     4.5        unicode_symbols: Boolean = false,
     4.6        export_pattern: String = "",
     4.7 -      check_delay: Time = Headless.default_check_delay,
     4.8 -      check_limit: Int = 0,
     4.9 -      watchdog_timeout: Time = Headless.default_watchdog_timeout,
    4.10 -      nodes_status_delay: Time = Headless.default_nodes_status_delay)
    4.11 +      check_delay: Option[Time] = None,
    4.12 +      check_limit: Option[Int] = None,
    4.13 +      watchdog_timeout: Option[Time] = None,
    4.14 +      nodes_status_delay: Option[Time] = None,
    4.15 +      commit_cleanup_delay: Option[Time] = None)
    4.16  
    4.17      def unapply(json: JSON.T): Option[Args] =
    4.18        for {
    4.19 @@ -171,18 +172,17 @@
    4.20          pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin)
    4.21          unicode_symbols <- JSON.bool_default(json, "unicode_symbols")
    4.22          export_pattern <- JSON.string_default(json, "export_pattern")
    4.23 -        check_delay <- JSON.seconds_default(json, "check_delay", Headless.default_check_delay)
    4.24 -        check_limit <- JSON.int_default(json, "check_limit")
    4.25 -        watchdog_timeout <-
    4.26 -          JSON.seconds_default(json, "watchdog_timeout", Headless.default_watchdog_timeout)
    4.27 -        nodes_status_delay <-
    4.28 -          JSON.seconds_default(json, "nodes_status_delay", Headless.default_nodes_status_delay)
    4.29 +        check_delay = JSON.seconds(json, "check_delay")
    4.30 +        check_limit = JSON.int(json, "check_limit")
    4.31 +        watchdog_timeout = JSON.seconds(json, "watchdog_timeout")
    4.32 +        nodes_status_delay = JSON.seconds(json, "nodes_status_delay")
    4.33 +        commit_cleanup_delay = JSON.seconds(json, "commit_cleanup_delay")
    4.34        }
    4.35        yield {
    4.36          Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin,
    4.37            unicode_symbols = unicode_symbols, export_pattern = export_pattern,
    4.38            check_delay = check_delay, check_limit = check_limit, watchdog_timeout = watchdog_timeout,
    4.39 -          nodes_status_delay = nodes_status_delay)
    4.40 +          nodes_status_delay = nodes_status_delay, commit_cleanup_delay = commit_cleanup_delay)
    4.41        }
    4.42  
    4.43      def command(args: Args,
    4.44 @@ -192,9 +192,12 @@
    4.45      {
    4.46        val result =
    4.47          session.use_theories(args.theories, master_dir = args.master_dir,
    4.48 -          check_delay = args.check_delay, check_limit = args.check_limit,
    4.49 -          watchdog_timeout = args.watchdog_timeout,
    4.50 -          nodes_status_delay = args.nodes_status_delay,
    4.51 +          check_delay = args.check_delay.getOrElse(session.default_check_delay),
    4.52 +          check_limit = args.check_limit.getOrElse(session.default_check_limit),
    4.53 +          watchdog_timeout = args.watchdog_timeout.getOrElse(session.default_watchdog_timeout),
    4.54 +          nodes_status_delay = args.nodes_status_delay.getOrElse(session.default_nodes_status_delay),
    4.55 +          commit_cleanup_delay =
    4.56 +            args.commit_cleanup_delay.getOrElse(session.default_commit_cleanup_delay),
    4.57            id = id, progress = progress)
    4.58  
    4.59        def output_text(s: String): String =