tuned;
authorwenzelm
Thu, 13 Oct 2016 23:09:26 +0200
changeset 64201 c3edc64e219d
parent 64200 2e6597279d38
child 64202 967515846691
tuned;
src/Pure/Admin/other_isabelle.scala
src/Pure/System/progress.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)
--- 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