src/Pure/System/isabelle_system.scala
changeset 62302 236e1ea5a197
parent 62298 d4e99aa28abc
child 62304 e7a52a838a23
     1.1 --- a/src/Pure/System/isabelle_system.scala	Sat Feb 13 21:17:08 2016 +0100
     1.2 +++ b/src/Pure/System/isabelle_system.scala	Sun Feb 14 11:52:27 2016 +0100
     1.3 @@ -167,7 +167,7 @@
     1.4  
     1.5    def mkdirs(path: Path): Unit =
     1.6      if (!path.is_dir) {
     1.7 -      bash_result("perl -e \"use File::Path make_path; make_path(" + File.shell_path(path) + ");\"")
     1.8 +      bash("perl -e \"use File::Path make_path; make_path(" + File.shell_path(path) + ");\"")
     1.9        if (!path.is_dir) error("Failed to create directory: " + quote(File.platform_path(path)))
    1.10      }
    1.11  
    1.12 @@ -316,7 +316,7 @@
    1.13      }
    1.14    }
    1.15  
    1.16 -  def bash_result(script: String, cwd: JFile = null, env: Map[String, String] = null,
    1.17 +  def bash(script: String, cwd: JFile = null, env: Map[String, String] = null,
    1.18      progress_stdout: String => Unit = (_: String) => (),
    1.19      progress_stderr: String => Unit = (_: String) => (),
    1.20      progress_limit: Option[Long] = None,
    1.21 @@ -342,14 +342,6 @@
    1.22      }
    1.23    }
    1.24  
    1.25 -  def bash(script: String): Int =
    1.26 -  {
    1.27 -    val result = bash_result(script)
    1.28 -    Output.warning(Library.trim_line(result.err))
    1.29 -    Output.writeln(Library.trim_line(result.out))
    1.30 -    result.rc
    1.31 -  }
    1.32 -
    1.33  
    1.34    /* system tools */
    1.35  
    1.36 @@ -371,13 +363,13 @@
    1.37    }
    1.38  
    1.39    def open(arg: String): Unit =
    1.40 -    bash_result("exec \"$ISABELLE_OPEN\" '" + arg + "' >/dev/null 2>/dev/null &")
    1.41 +    bash("exec \"$ISABELLE_OPEN\" '" + arg + "' >/dev/null 2>/dev/null &")
    1.42  
    1.43    def pdf_viewer(arg: Path): Unit =
    1.44 -    bash_result("exec \"$PDF_VIEWER\" '" + File.standard_path(arg) + "' >/dev/null 2>/dev/null &")
    1.45 +    bash("exec \"$PDF_VIEWER\" '" + File.standard_path(arg) + "' >/dev/null 2>/dev/null &")
    1.46  
    1.47    def hg(cmd_line: String, cwd: Path = Path.current): Bash.Result =
    1.48 -    bash_result("cd " + File.shell_path(cwd) + " && \"${HG:-hg}\" " + cmd_line)
    1.49 +    bash("cd " + File.shell_path(cwd) + " && \"${HG:-hg}\" " + cmd_line)
    1.50  
    1.51  
    1.52    /** Isabelle resources **/