--- a/src/Pure/General/time.scala Wed Aug 18 23:04:58 2021 +0200
+++ b/src/Pure/General/time.scala Thu Aug 19 12:01:57 2021 +0200
@@ -14,8 +14,8 @@
object Time
{
def seconds(s: Double): Time = new Time((s * 1000.0).round)
- def minutes(s: Double): Time = new Time((s * 60000.0).round)
- def ms(m: Long): Time = new Time(m)
+ def minutes(m: Double): Time = new Time((m * 60000.0).round)
+ def ms(ms: Long): Time = new Time(ms)
def hms(h: Int, m: Int, s: Double): Time = seconds(s + 60 * m + 3600 * h)
def now(): Time = ms(System.currentTimeMillis())
--- a/src/Pure/General/timing.ML Wed Aug 18 23:04:58 2021 +0200
+++ b/src/Pure/General/timing.ML Thu Aug 19 12:01:57 2021 +0200
@@ -1,7 +1,7 @@
(* Title: Pure/General/timing.ML
Author: Makarius
-Basic support for time measurement.
+Support for time measurement.
*)
signature BASIC_TIMING =
--- a/src/Pure/System/bash.ML Wed Aug 18 23:04:58 2021 +0200
+++ b/src/Pure/System/bash.ML Thu Aug 19 12:01:57 2021 +0200
@@ -1,7 +1,7 @@
(* Title: Pure/System/bash.ML
Author: Makarius
-Syntax for GNU bash.
+Support for GNU bash.
*)
signature BASH =
--- a/src/Pure/System/bash.scala Wed Aug 18 23:04:58 2021 +0200
+++ b/src/Pure/System/bash.scala Thu Aug 19 12:01:57 2021 +0200
@@ -1,7 +1,8 @@
/* Title: Pure/System/bash.scala
Author: Makarius
-GNU bash processes, with propagation of interrupts.
+Support for GNU bash: portable external processes with propagation of
+interrupts.
*/
package isabelle