src/Pure/ML/ml_statistics.scala
changeset 82466 d5ef492dd673
parent 80224 db92e0b6a11a
equal deleted inserted replaced
82465:3cc075052033 82466:d5ef492dd673
    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)