equal
deleted
inserted
replaced
55 def progress_stdout(line: String): Unit = { |
55 def progress_stdout(line: String): Unit = { |
56 val props = space_explode(',', line).flatMap(Properties.Eq.unapply) |
56 val props = space_explode(',', line).flatMap(Properties.Eq.unapply) |
57 if (props.nonEmpty) consume(props) |
57 if (props.nonEmpty) consume(props) |
58 } |
58 } |
59 |
59 |
60 val env_prefix = |
60 val env_prefix = if_proper(stats_dir, Bash.exports("POLYSTATSDIR=" + stats_dir)) |
61 if_proper(stats_dir, "export POLYSTATSDIR=" + Bash.string(stats_dir) + "\n") |
|
62 |
61 |
63 Bash.process(env_prefix + "\"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " + |
62 Bash.process(env_prefix + "\"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " + |
64 Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " + |
63 Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " + |
65 ML_Syntax.print_double(delay.seconds)), |
64 ML_Syntax.print_double(delay.seconds)), |
66 cwd = Path.ISABELLE_HOME) |
65 cwd = Path.ISABELLE_HOME) |