equal
deleted
inserted
replaced
21 { |
21 { |
22 /* properties */ |
22 /* properties */ |
23 |
23 |
24 val Now = new Properties.Double("now") |
24 val Now = new Properties.Double("now") |
25 def now(props: Properties.T): Double = Now.unapply(props).get |
25 def now(props: Properties.T): Double = Now.unapply(props).get |
|
26 |
|
27 |
|
28 /* monitor process */ |
|
29 |
|
30 def monitor(pid: Long, |
|
31 delay: Time = Time.seconds(0.5), |
|
32 consume: Properties.T => Unit = Console.println) |
|
33 { |
|
34 def progress_stdout(line: String) |
|
35 { |
|
36 val props = |
|
37 Library.space_explode(',', line).flatMap((entry: String) => |
|
38 Library.space_explode('=', entry) match { |
|
39 case List(a, b) => Some((a, b)) |
|
40 case _ => None |
|
41 }) |
|
42 if (props.nonEmpty) consume(props) |
|
43 } |
|
44 |
|
45 Bash.process("exec \"$POLYML_EXE\" -q --use " + |
|
46 File.bash_path(Path.explode("~~/src/Pure/ML/ml_statistics.ML")) + |
|
47 " --eval " + Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " + |
|
48 ML_Syntax.print_double(delay.seconds))) |
|
49 .result(progress_stdout = progress_stdout, strict = false).check |
|
50 } |
26 |
51 |
27 |
52 |
28 /* memory fields (mega bytes) */ |
53 /* memory fields (mega bytes) */ |
29 |
54 |
30 def mem_print(x: Long): Option[String] = |
55 def mem_print(x: Long): Option[String] = |