# HG changeset patch # User wenzelm # Date 1476392966 -7200 # Node ID c3edc64e219d8a5ac64ee8fd6cc1ed4a8e5b2b84 # Parent 2e6597279d3898d401e2d3f949c86e43065b5de6 tuned; diff -r 2e6597279d38 -r c3edc64e219d src/Pure/Admin/other_isabelle.scala --- a/src/Pure/Admin/other_isabelle.scala Thu Oct 13 22:59:20 2016 +0200 +++ b/src/Pure/Admin/other_isabelle.scala Thu Oct 13 23:09:26 2016 +0200 @@ -15,11 +15,9 @@ /* static system */ def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result = - Isabelle_System.bash( + progress.bash( "export ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) + "\n" + script, - env = null, cwd = isabelle_home.file, redirect = redirect, - progress_stdout = progress.echo_if(echo, _), - progress_stderr = progress.echo_if(echo, _)) + env = null, cwd = isabelle_home.file, redirect = redirect) def apply(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result = bash("bin/isabelle " + cmdline, redirect, echo) diff -r 2e6597279d38 -r c3edc64e219d src/Pure/System/progress.scala --- a/src/Pure/System/progress.scala Thu Oct 13 22:59:20 2016 +0200 +++ b/src/Pure/System/progress.scala Thu Oct 13 23:09:26 2016 +0200 @@ -7,6 +7,9 @@ package isabelle +import java.io.{File => JFile} + + class Progress { def echo(msg: String) {} @@ -14,6 +17,17 @@ def theory(session: String, theory: String) {} def stopped: Boolean = false override def toString: String = if (stopped) "Progress(stopped)" else "Progress" + + def bash(script: String, + cwd: JFile = null, + env: Map[String, String] = Isabelle_System.settings(), + redirect: Boolean = false, + echo: Boolean = false): Process_Result = + { + Isabelle_System.bash(script, cwd = cwd, env = env, redirect = redirect, + progress_stdout = echo_if(echo, _), + progress_stderr = echo_if(echo, _)) + } } object Ignore_Progress extends Progress