tuned signature;
authorwenzelm
Sun Feb 14 11:52:27 2016 +0100 (2016-02-14)
changeset 62302236e1ea5a197
parent 62301 028e5b1ef9f9
child 62303 f868f12f9419
tuned signature;
src/Pure/Concurrent/bash.scala
src/Pure/System/isabelle_system.scala
src/Pure/Tools/build.scala
src/Tools/jEdit/src/active.scala
     1.1 --- a/src/Pure/Concurrent/bash.scala	Sat Feb 13 23:59:35 2016 +0100
     1.2 +++ b/src/Pure/Concurrent/bash.scala	Sun Feb 14 11:52:27 2016 +0100
     1.3 @@ -26,6 +26,13 @@
     1.4        if (rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
     1.5        else if (rc != 0) error(err)
     1.6        else this
     1.7 +
     1.8 +    def print: Result =
     1.9 +    {
    1.10 +      Output.warning(Library.trim_line(err))
    1.11 +      Output.writeln(Library.trim_line(out))
    1.12 +      Result(Nil, Nil, rc)
    1.13 +    }
    1.14    }
    1.15  
    1.16  
     2.1 --- a/src/Pure/System/isabelle_system.scala	Sat Feb 13 23:59:35 2016 +0100
     2.2 +++ b/src/Pure/System/isabelle_system.scala	Sun Feb 14 11:52:27 2016 +0100
     2.3 @@ -167,7 +167,7 @@
     2.4  
     2.5    def mkdirs(path: Path): Unit =
     2.6      if (!path.is_dir) {
     2.7 -      bash_result("perl -e \"use File::Path make_path; make_path(" + File.shell_path(path) + ");\"")
     2.8 +      bash("perl -e \"use File::Path make_path; make_path(" + File.shell_path(path) + ");\"")
     2.9        if (!path.is_dir) error("Failed to create directory: " + quote(File.platform_path(path)))
    2.10      }
    2.11  
    2.12 @@ -316,7 +316,7 @@
    2.13      }
    2.14    }
    2.15  
    2.16 -  def bash_result(script: String, cwd: JFile = null, env: Map[String, String] = null,
    2.17 +  def bash(script: String, cwd: JFile = null, env: Map[String, String] = null,
    2.18      progress_stdout: String => Unit = (_: String) => (),
    2.19      progress_stderr: String => Unit = (_: String) => (),
    2.20      progress_limit: Option[Long] = None,
    2.21 @@ -342,14 +342,6 @@
    2.22      }
    2.23    }
    2.24  
    2.25 -  def bash(script: String): Int =
    2.26 -  {
    2.27 -    val result = bash_result(script)
    2.28 -    Output.warning(Library.trim_line(result.err))
    2.29 -    Output.writeln(Library.trim_line(result.out))
    2.30 -    result.rc
    2.31 -  }
    2.32 -
    2.33  
    2.34    /* system tools */
    2.35  
    2.36 @@ -371,13 +363,13 @@
    2.37    }
    2.38  
    2.39    def open(arg: String): Unit =
    2.40 -    bash_result("exec \"$ISABELLE_OPEN\" '" + arg + "' >/dev/null 2>/dev/null &")
    2.41 +    bash("exec \"$ISABELLE_OPEN\" '" + arg + "' >/dev/null 2>/dev/null &")
    2.42  
    2.43    def pdf_viewer(arg: Path): Unit =
    2.44 -    bash_result("exec \"$PDF_VIEWER\" '" + File.standard_path(arg) + "' >/dev/null 2>/dev/null &")
    2.45 +    bash("exec \"$PDF_VIEWER\" '" + File.standard_path(arg) + "' >/dev/null 2>/dev/null &")
    2.46  
    2.47    def hg(cmd_line: String, cwd: Path = Path.current): Bash.Result =
    2.48 -    bash_result("cd " + File.shell_path(cwd) + " && \"${HG:-hg}\" " + cmd_line)
    2.49 +    bash("cd " + File.shell_path(cwd) + " && \"${HG:-hg}\" " + cmd_line)
    2.50  
    2.51  
    2.52    /** Isabelle resources **/
     3.1 --- a/src/Pure/Tools/build.scala	Sat Feb 13 23:59:35 2016 +0100
     3.2 +++ b/src/Pure/Tools/build.scala	Sun Feb 14 11:52:27 2016 +0100
     3.3 @@ -602,7 +602,7 @@
     3.4  
     3.5      private val result =
     3.6        Future.thread("build") {
     3.7 -        Isabelle_System.bash_result(script, info.dir.file, env,
     3.8 +        Isabelle_System.bash(script, info.dir.file, env,
     3.9            progress_stdout = (line: String) =>
    3.10              Library.try_unprefix("\floading_theory = ", line) match {
    3.11                case Some(theory) => progress.theory(name, theory)
     4.1 --- a/src/Tools/jEdit/src/active.scala	Sat Feb 13 23:59:35 2016 +0100
     4.2 +++ b/src/Tools/jEdit/src/active.scala	Sun Feb 14 11:52:27 2016 +0100
     4.3 @@ -33,7 +33,7 @@
     4.4                  Standard_Thread.fork("browser") {
     4.5                    val graph_file = Isabelle_System.tmp_file("graph")
     4.6                    File.write(graph_file, XML.content(body))
     4.7 -                  Isabelle_System.bash_result("\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &",
     4.8 +                  Isabelle_System.bash("\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &",
     4.9                      env = Map("GRAPH_FILE" -> File.standard_path(graph_file)))
    4.10                  }
    4.11