equal
deleted
inserted
replaced
461 progress_stdout: String => Unit = (_: String) => (), |
461 progress_stdout: String => Unit = (_: String) => (), |
462 progress_stderr: String => Unit = (_: String) => (), |
462 progress_stderr: String => Unit = (_: String) => (), |
463 strict: Boolean = true): Process_Result = |
463 strict: Boolean = true): Process_Result = |
464 exec(command).result(progress_stdout, progress_stderr, strict) |
464 exec(command).result(progress_stdout, progress_stderr, strict) |
465 |
465 |
|
466 override def isabelle_platform: Isabelle_Platform = Isabelle_Platform.remote(this) |
|
467 |
466 |
468 |
467 /* tmp dirs */ |
469 /* tmp dirs */ |
468 |
470 |
469 def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir)) |
471 def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir)) |
470 |
472 |
478 { |
480 { |
479 val remote_dir = tmp_dir() |
481 val remote_dir = tmp_dir() |
480 try { body(Path.explode(remote_dir)) } finally { rm_tree(remote_dir) } |
482 try { body(Path.explode(remote_dir)) } finally { rm_tree(remote_dir) } |
481 } |
483 } |
482 } |
484 } |
483 |
|
484 |
485 |
485 |
486 |
486 /* system operations */ |
487 /* system operations */ |
487 |
488 |
488 trait System |
489 trait System |
499 progress_stdout: String => Unit = (_: String) => (), |
500 progress_stdout: String => Unit = (_: String) => (), |
500 progress_stderr: String => Unit = (_: String) => (), |
501 progress_stderr: String => Unit = (_: String) => (), |
501 strict: Boolean = true): Process_Result = |
502 strict: Boolean = true): Process_Result = |
502 Isabelle_System.bash(command, progress_stdout = progress_stdout, |
503 Isabelle_System.bash(command, progress_stdout = progress_stdout, |
503 progress_stderr = progress_stderr, strict = strict) |
504 progress_stderr = progress_stderr, strict = strict) |
|
505 |
|
506 def isabelle_platform: Isabelle_Platform = Isabelle_Platform.local() |
504 } |
507 } |
505 |
508 |
506 object Local extends System |
509 object Local extends System |
507 } |
510 } |