tuned;
authorwenzelm
Thu Oct 13 23:09:26 2016 +0200 (2016-10-13)
changeset 64201c3edc64e219d
parent 64200 2e6597279d38
child 64202 967515846691
tuned;
src/Pure/Admin/other_isabelle.scala
src/Pure/System/progress.scala
     1.1 --- a/src/Pure/Admin/other_isabelle.scala	Thu Oct 13 22:59:20 2016 +0200
     1.2 +++ b/src/Pure/Admin/other_isabelle.scala	Thu Oct 13 23:09:26 2016 +0200
     1.3 @@ -15,11 +15,9 @@
     1.4    /* static system */
     1.5  
     1.6    def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
     1.7 -    Isabelle_System.bash(
     1.8 +    progress.bash(
     1.9        "export ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) + "\n" + script,
    1.10 -      env = null, cwd = isabelle_home.file, redirect = redirect,
    1.11 -      progress_stdout = progress.echo_if(echo, _),
    1.12 -      progress_stderr = progress.echo_if(echo, _))
    1.13 +      env = null, cwd = isabelle_home.file, redirect = redirect)
    1.14  
    1.15    def apply(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
    1.16      bash("bin/isabelle " + cmdline, redirect, echo)
     2.1 --- a/src/Pure/System/progress.scala	Thu Oct 13 22:59:20 2016 +0200
     2.2 +++ b/src/Pure/System/progress.scala	Thu Oct 13 23:09:26 2016 +0200
     2.3 @@ -7,6 +7,9 @@
     2.4  package isabelle
     2.5  
     2.6  
     2.7 +import java.io.{File => JFile}
     2.8 +
     2.9 +
    2.10  class Progress
    2.11  {
    2.12    def echo(msg: String) {}
    2.13 @@ -14,6 +17,17 @@
    2.14    def theory(session: String, theory: String) {}
    2.15    def stopped: Boolean = false
    2.16    override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
    2.17 +
    2.18 +  def bash(script: String,
    2.19 +    cwd: JFile = null,
    2.20 +    env: Map[String, String] = Isabelle_System.settings(),
    2.21 +    redirect: Boolean = false,
    2.22 +    echo: Boolean = false): Process_Result =
    2.23 +  {
    2.24 +    Isabelle_System.bash(script, cwd = cwd, env = env, redirect = redirect,
    2.25 +      progress_stdout = echo_if(echo, _),
    2.26 +      progress_stderr = echo_if(echo, _))
    2.27 +  }
    2.28  }
    2.29  
    2.30  object Ignore_Progress extends Progress