| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Pure/System/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 3 kB |
|
Quelle process_result.scala Sprache: Scala |
|||||||||
|
/* Title: Pure/System/process_result.scala
Author: Makarius Result of system process. */ package isabelle object Process_Result { /* return code */ object RC { val undefined = -1 val ok = 0 val error = 1 val failure = 2 val startup_failure = 127 val interrupt = 130 val timeout = 142 val regular: Set[Int] = Set(ok, error) private def text(rc: Int): String = { val txt = rc match { case `undefined` => "UNDEFINED" case `ok` => "OK" case `error` => "ERROR" case `failure` => "FAILURE" case `startup_failure` => "COMMAND NOT FOUND" case `interrupt` => "INTERRUPT" case 131 => "QUIT SIGNAL" case 137 => "KILL SIGNAL" case 138 => "BUS ERROR" case 139 => "SEGMENTATION VIOLATION" case `timeout` => "TIMEOUT" case 143 => "TERMINATION SIGNAL" case _ => "" } if (txt.isEmpty) txt else " (" + txt + ")" } def print_long(rc: Int): String = "Return code: " + rc + text(rc) def print(rc: Int): String = "return code " + rc + text(rc) def merge(rc1: Int, rc2: Int): Int = if (rc1 == interrupt || rc2 == interrupt) interrupt else rc1 max rc2 def merge(rcs: IterableOnce[Int]): Int = rcs.iterator.foldLeft(ok)(merge) def apply(ok: Boolean): Int = if (ok) RC.ok else RC.error def apply(exn: Throwable): Int = if (Exn.is_interrupt(exn)) interrupt else error def apply(result: Exn.Result[Process_Result]): Int = result match { case Exn.Res(res) => res.rc case Exn.Exn(exn) => apply(exn) } } val undefined: Process_Result = Process_Result(RC.undefined) val ok: Process_Result = Process_Result(RC.ok) val error: Process_Result = Process_Result(RC.error) val startup_failure: Process_Result = Process_Result(RC.startup_failure) } final case class Process_Result( rc: Int, out_lines: List[String] = Nil, err_lines: List[String] = Nil, timing: Timing = Timing.zero ) { def out: String = Library.trim_line(cat_lines(out_lines)) def err: String = Library.trim_line(cat_lines(err_lines)) def output(outs: List[String]): Process_Result = copy(out_lines = out_lines ::: outs.flatMap(split_lines)) def errors(errs: List[String]): Process_Result = copy(err_lines = err_lines ::: errs.flatMap(split_lines)) def error(err: String): Process_Result = if (err.isEmpty) this else errors(List(err)) def ok: Boolean = rc == Process_Result.RC.ok def interrupted: Boolean = rc == Process_Result.RC.interrupt def defined: Boolean = rc > Process_Result.RC.undefined def strict: Process_Result = if (defined) this else copy(rc = Process_Result.RC.error) def timeout_rc: Process_Result = copy(rc = Process_Result.RC.timeout) def timeout: Boolean = rc == Process_Result.RC.timeout def error_rc: Process_Result = if (interrupted) this else copy(rc = rc max Process_Result.RC.error) def errors_rc(errs: List[String]): Process_Result = if (errs.isEmpty) this else errors(errs).error_rc def check_rc(pred: Int => Boolean): Process_Result = if (pred(rc)) this else if (interrupted) throw Exn.Interrupt() else Exn.error(err) def check: Process_Result = check_rc(_ == Process_Result.RC.ok) def print_return_code: String = Process_Result.RC.print_long(rc) def print_rc: String = Process_Result.RC.print(rc) def print: Process_Result = { Output.warning(err) Output.writeln(out) copy(out_lines = Nil, err_lines = Nil) } def print_stdout: Process_Result = { Output.warning(err, stdout = true) Output.writeln(out, stdout = true) copy(out_lines = Nil, err_lines = Nil) } } ¤ Dauer der Verarbeitung: 0.25 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28