# HG changeset patch
# User wenzelm
# Date 1455447147 -3600
# Node ID 236e1ea5a197bf79e52394d96df424562e261021
# Parent  028e5b1ef9f96e9075f253ee0d09d4b385016e67
tuned signature;

diff -r 028e5b1ef9f9 -r 236e1ea5a197 src/Pure/Concurrent/bash.scala
--- a/src/Pure/Concurrent/bash.scala	Sat Feb 13 23:59:35 2016 +0100
+++ b/src/Pure/Concurrent/bash.scala	Sun Feb 14 11:52:27 2016 +0100
@@ -26,6 +26,13 @@
       if (rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
       else if (rc != 0) error(err)
       else this
+
+    def print: Result =
+    {
+      Output.warning(Library.trim_line(err))
+      Output.writeln(Library.trim_line(out))
+      Result(Nil, Nil, rc)
+    }
   }
 
 
diff -r 028e5b1ef9f9 -r 236e1ea5a197 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Feb 13 23:59:35 2016 +0100
+++ b/src/Pure/System/isabelle_system.scala	Sun Feb 14 11:52:27 2016 +0100
@@ -167,7 +167,7 @@
 
   def mkdirs(path: Path): Unit =
     if (!path.is_dir) {
-      bash_result("perl -e \"use File::Path make_path; make_path(" + File.shell_path(path) + ");\"")
+      bash("perl -e \"use File::Path make_path; make_path(" + File.shell_path(path) + ");\"")
       if (!path.is_dir) error("Failed to create directory: " + quote(File.platform_path(path)))
     }
 
@@ -316,7 +316,7 @@
     }
   }
 
-  def bash_result(script: String, cwd: JFile = null, env: Map[String, String] = null,
+  def bash(script: String, cwd: JFile = null, env: Map[String, String] = null,
     progress_stdout: String => Unit = (_: String) => (),
     progress_stderr: String => Unit = (_: String) => (),
     progress_limit: Option[Long] = None,
@@ -342,14 +342,6 @@
     }
   }
 
-  def bash(script: String): Int =
-  {
-    val result = bash_result(script)
-    Output.warning(Library.trim_line(result.err))
-    Output.writeln(Library.trim_line(result.out))
-    result.rc
-  }
-
 
   /* system tools */
 
@@ -371,13 +363,13 @@
   }
 
   def open(arg: String): Unit =
-    bash_result("exec \"$ISABELLE_OPEN\" '" + arg + "' >/dev/null 2>/dev/null &")
+    bash("exec \"$ISABELLE_OPEN\" '" + arg + "' >/dev/null 2>/dev/null &")
 
   def pdf_viewer(arg: Path): Unit =
-    bash_result("exec \"$PDF_VIEWER\" '" + File.standard_path(arg) + "' >/dev/null 2>/dev/null &")
+    bash("exec \"$PDF_VIEWER\" '" + File.standard_path(arg) + "' >/dev/null 2>/dev/null &")
 
   def hg(cmd_line: String, cwd: Path = Path.current): Bash.Result =
-    bash_result("cd " + File.shell_path(cwd) + " && \"${HG:-hg}\" " + cmd_line)
+    bash("cd " + File.shell_path(cwd) + " && \"${HG:-hg}\" " + cmd_line)
 
 
   /** Isabelle resources **/
diff -r 028e5b1ef9f9 -r 236e1ea5a197 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Feb 13 23:59:35 2016 +0100
+++ b/src/Pure/Tools/build.scala	Sun Feb 14 11:52:27 2016 +0100
@@ -602,7 +602,7 @@
 
     private val result =
       Future.thread("build") {
-        Isabelle_System.bash_result(script, info.dir.file, env,
+        Isabelle_System.bash(script, info.dir.file, env,
           progress_stdout = (line: String) =>
             Library.try_unprefix("\floading_theory = ", line) match {
               case Some(theory) => progress.theory(name, theory)
diff -r 028e5b1ef9f9 -r 236e1ea5a197 src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Sat Feb 13 23:59:35 2016 +0100
+++ b/src/Tools/jEdit/src/active.scala	Sun Feb 14 11:52:27 2016 +0100
@@ -33,7 +33,7 @@
                 Standard_Thread.fork("browser") {
                   val graph_file = Isabelle_System.tmp_file("graph")
                   File.write(graph_file, XML.content(body))
-                  Isabelle_System.bash_result("\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &",
+                  Isabelle_System.bash("\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &",
                     env = Map("GRAPH_FILE" -> File.standard_path(graph_file)))
                 }