src/Pure/System/isabelle_system.scala
changeset 50651 1fe68f1c3069
parent 50403 87868964733c
child 50652 ead5714cc480
equal deleted inserted replaced
50650:8922afc54b3d 50651:1fe68f1c3069
    71               val shell_prefix =
    71               val shell_prefix =
    72                 if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\bash", "-l")
    72                 if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\bash", "-l")
    73                 else Nil
    73                 else Nil
    74               val cmdline =
    74               val cmdline =
    75                 shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
    75                 shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
    76               val (output, rc) = Standard_System.raw_exec(null, env, true, cmdline: _*)
    76               val (output, rc) = process_output(raw_execute(null, env, true, cmdline: _*))
    77               if (rc != 0) error(output)
    77               if (rc != 0) error(output)
    78 
    78 
    79               val entries =
    79               val entries =
    80                 (for (entry <- File.read(dump) split "\0" if entry != "") yield {
    80                 (for (entry <- File.read(dump) split "\0" if entry != "") yield {
    81                   val i = entry.indexOf('=')
    81                   val i = entry.indexOf('=')
   138 
   138 
   139 
   139 
   140 
   140 
   141   /** external processes **/
   141   /** external processes **/
   142 
   142 
       
   143   /* raw execute for bootstrapping */
       
   144 
       
   145   private def raw_execute(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
       
   146     : Process =
       
   147   {
       
   148     val cmdline = new java.util.LinkedList[String]
       
   149     for (s <- args) cmdline.add(s)
       
   150 
       
   151     val proc = new ProcessBuilder(cmdline)
       
   152     if (cwd != null) proc.directory(cwd)
       
   153     if (env != null) {
       
   154       proc.environment.clear
       
   155       for ((x, y) <- env) proc.environment.put(x, y)
       
   156     }
       
   157     proc.redirectErrorStream(redirect)
       
   158     proc.start
       
   159   }
       
   160 
       
   161   private def process_output(proc: Process): (String, Int) =
       
   162   {
       
   163     proc.getOutputStream.close
       
   164     val output = File.read(proc.getInputStream)
       
   165     val rc =
       
   166       try { proc.waitFor }
       
   167       finally {
       
   168         proc.getInputStream.close
       
   169         proc.getErrorStream.close
       
   170         proc.destroy
       
   171         Thread.interrupted
       
   172       }
       
   173     (output, rc)
       
   174   }
       
   175 
       
   176 
   143   /* plain execute */
   177   /* plain execute */
   144 
   178 
   145   def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
   179   def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
   146   {
   180   {
   147     val cmdline =
   181     val cmdline =
   148       if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\env.exe") ++ args
   182       if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\env.exe") ++ args
   149       else args
   183       else args
   150     val env1 = if (env == null) settings else settings ++ env
   184     val env1 = if (env == null) settings else settings ++ env
   151     Standard_System.raw_execute(cwd, env1, redirect, cmdline: _*)
   185     raw_execute(cwd, env1, redirect, cmdline: _*)
   152   }
   186   }
   153 
   187 
   154   def execute(redirect: Boolean, args: String*): Process =
   188   def execute(redirect: Boolean, args: String*): Process =
   155     execute_env(null, null, redirect, args: _*)
   189     execute_env(null, null, redirect, args: _*)
   156 
   190 
   256       }
   290       }
   257       catch { case _: SecurityException => false }
   291       catch { case _: SecurityException => false }
   258     } match {
   292     } match {
   259       case Some(dir) =>
   293       case Some(dir) =>
   260         val file = standard_path(dir + Path.basic(name))
   294         val file = standard_path(dir + Path.basic(name))
   261         Standard_System.process_output(execute(true, (List(file) ++ args): _*))
   295         process_output(execute(true, (List(file) ++ args): _*))
   262       case None => ("Unknown Isabelle tool: " + name, 2)
   296       case None => ("Unknown Isabelle tool: " + name, 2)
   263     }
   297     }
   264   }
   298   }
   265 
   299 
   266 
   300