# HG changeset patch # User wenzelm # Date 1356958141 -3600 # Node ID 1fe68f1c3069beb6370d424b94597e82e3d651ec # Parent 8922afc54b3d6570ca50408d587fc4f8bd2df4f1 tuned signature; diff -r 8922afc54b3d -r 1fe68f1c3069 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Mon Dec 31 13:34:47 2012 +0100 +++ b/src/Pure/System/isabelle_system.scala Mon Dec 31 13:49:01 2012 +0100 @@ -73,7 +73,7 @@ else Nil val cmdline = shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString) - val (output, rc) = Standard_System.raw_exec(null, env, true, cmdline: _*) + val (output, rc) = process_output(raw_execute(null, env, true, cmdline: _*)) if (rc != 0) error(output) val entries = @@ -140,6 +140,40 @@ /** external processes **/ + /* raw execute for bootstrapping */ + + private def raw_execute(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*) + : Process = + { + val cmdline = new java.util.LinkedList[String] + for (s <- args) cmdline.add(s) + + val proc = new ProcessBuilder(cmdline) + if (cwd != null) proc.directory(cwd) + if (env != null) { + proc.environment.clear + for ((x, y) <- env) proc.environment.put(x, y) + } + proc.redirectErrorStream(redirect) + proc.start + } + + private def process_output(proc: Process): (String, Int) = + { + proc.getOutputStream.close + val output = File.read(proc.getInputStream) + val rc = + try { proc.waitFor } + finally { + proc.getInputStream.close + proc.getErrorStream.close + proc.destroy + Thread.interrupted + } + (output, rc) + } + + /* plain execute */ def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process = @@ -148,7 +182,7 @@ if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\env.exe") ++ args else args val env1 = if (env == null) settings else settings ++ env - Standard_System.raw_execute(cwd, env1, redirect, cmdline: _*) + raw_execute(cwd, env1, redirect, cmdline: _*) } def execute(redirect: Boolean, args: String*): Process = @@ -258,7 +292,7 @@ } match { case Some(dir) => val file = standard_path(dir + Path.basic(name)) - Standard_System.process_output(execute(true, (List(file) ++ args): _*)) + process_output(execute(true, (List(file) ++ args): _*)) case None => ("Unknown Isabelle tool: " + name, 2) } } diff -r 8922afc54b3d -r 1fe68f1c3069 src/Pure/System/standard_system.scala --- a/src/Pure/System/standard_system.scala Mon Dec 31 13:34:47 2012 +0100 +++ b/src/Pure/System/standard_system.scala Mon Dec 31 13:49:01 2012 +0100 @@ -16,42 +16,6 @@ object Standard_System { - /* shell processes */ - - def raw_execute(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process = - { - val cmdline = new java.util.LinkedList[String] - for (s <- args) cmdline.add(s) - - val proc = new ProcessBuilder(cmdline) - if (cwd != null) proc.directory(cwd) - if (env != null) { - proc.environment.clear - for ((x, y) <- env) proc.environment.put(x, y) - } - proc.redirectErrorStream(redirect) - proc.start - } - - def process_output(proc: Process): (String, Int) = - { - proc.getOutputStream.close - val output = File.read(proc.getInputStream) - val rc = - try { proc.waitFor } - finally { - proc.getInputStream.close - proc.getErrorStream.close - proc.destroy - Thread.interrupted - } - (output, rc) - } - - def raw_exec(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*) - : (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*)) - - /* cygwin_root */ def cygwin_root(): String =