| author | wenzelm |
| Sat, 20 Jan 2024 16:09:35 +0100 | |
| changeset 79503 | c67b47cd41dc |
| parent 75393 | 87ebf5a50283 |
| permissions | -rw-r--r-- |
|
48346
e2382bede914
more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/System/command_line.scala |
|
e2382bede914
more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
|
e2382bede914
more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff
changeset
|
3 |
|
|
e2382bede914
more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff
changeset
|
4 |
Support for Isabelle/Scala command line tools. |
|
e2382bede914
more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
|
e2382bede914
more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff
changeset
|
6 |
|
|
e2382bede914
more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle |
|
e2382bede914
more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff
changeset
|
8 |
|
|
e2382bede914
more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff
changeset
|
9 |
|
| 75393 | 10 |
object Command_Line {
|
11 |
object Chunks {
|
|
|
48346
e2382bede914
more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff
changeset
|
12 |
private def chunks(list: List[String]): List[List[String]] = |
|
e2382bede914
more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff
changeset
|
13 |
list.indexWhere(_ == "\n") match {
|
|
e2382bede914
more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff
changeset
|
14 |
case -1 => List(list) |
|
e2382bede914
more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff
changeset
|
15 |
case i => |
|
e2382bede914
more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff
changeset
|
16 |
val (chunk, rest) = list.splitAt(i) |
|
e2382bede914
more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff
changeset
|
17 |
chunk :: chunks(rest.tail) |
|
e2382bede914
more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff
changeset
|
18 |
} |
|
e2382bede914
more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff
changeset
|
19 |
def unapplySeq(list: List[String]): Option[List[List[String]]] = Some(chunks(list)) |
|
e2382bede914
more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff
changeset
|
20 |
} |
|
e2382bede914
more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff
changeset
|
21 |
|
| 75393 | 22 |
def tool(body: => Unit): Unit = {
|
| 71687 | 23 |
val thread = |
| 71692 | 24 |
Isabelle_Thread.fork(name = "command_line", inherit_locals = true) {
|
| 71687 | 25 |
val rc = |
| 74306 | 26 |
try { body; Process_Result.RC.ok }
|
| 71687 | 27 |
catch {
|
28 |
case exn: Throwable => |
|
| 73963 | 29 |
Output.error_message(Exn.print(exn)) |
| 74068 | 30 |
Exn.failure_rc(exn) |
| 71687 | 31 |
} |
32 |
sys.exit(rc) |
|
| 51980 | 33 |
} |
| 74140 | 34 |
thread.join() |
|
48346
e2382bede914
more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff
changeset
|
35 |
} |
| 56631 | 36 |
|
| 71632 | 37 |
def ML_tool(body: List[String]): String = |
38 |
"Command_Line.tool (fn () => (" + body.mkString("; ") + "));"
|
|
|
48346
e2382bede914
more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff
changeset
|
39 |
} |