src/Pure/Thy/thy_resources.scala
changeset 68943 e564605d4cac
parent 68936 90c08c7bab9c
child 68947 ea804c814693
     1.1 --- a/src/Pure/Thy/thy_resources.scala	Sat Sep 08 12:01:22 2018 +0200
     1.2 +++ b/src/Pure/Thy/thy_resources.scala	Sat Sep 08 12:01:37 2018 +0200
     1.3 @@ -78,9 +78,9 @@
     1.4        (nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok })
     1.5    }
     1.6  
     1.7 -  val default_check_delay: Double = 0.5
     1.8 -  val default_nodes_status_delay: Double = -1.0
     1.9 -  val default_commit_clean_delay: Double = 60.0
    1.10 +  val default_check_delay = Time.seconds(0.5)
    1.11 +  val default_nodes_status_delay = Time.seconds(-1.0)
    1.12 +  val default_commit_clean_delay = Time.seconds(60.0)
    1.13  
    1.14  
    1.15    class Session private[Thy_Resources](
    1.16 @@ -194,14 +194,14 @@
    1.17        theories: List[String],
    1.18        qualifier: String = Sessions.DRAFT,
    1.19        master_dir: String = "",
    1.20 -      check_delay: Time = Time.seconds(default_check_delay),
    1.21 +      check_delay: Time = default_check_delay,
    1.22        check_limit: Int = 0,
    1.23        watchdog_timeout: Time = Time.zero,
    1.24 -      nodes_status_delay: Time = Time.seconds(default_nodes_status_delay),
    1.25 +      nodes_status_delay: Time = default_nodes_status_delay,
    1.26        id: UUID = UUID(),
    1.27        // commit: must not block, must not fail
    1.28        commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None,
    1.29 -      commit_clean_delay: Time = Time.seconds(default_commit_clean_delay),
    1.30 +      commit_clean_delay: Time = default_commit_clean_delay,
    1.31        progress: Progress = No_Progress): Theories_Result =
    1.32      {
    1.33        val dep_theories =