author | wenzelm |
Sat, 11 Dec 2021 13:06:46 +0100 | |
changeset 74919 | 115a47a103aa |
parent 74210 | c14774713d62 |
child 77851 | ec50b9213969 |
permissions | -rw-r--r-- |
73264 | 1 |
(* Title: Pure/System/bash.ML |
64304 | 2 |
Author: Makarius |
3 |
||
74158 | 4 |
Support for GNU bash. |
64304 | 5 |
*) |
6 |
||
73264 | 7 |
signature BASH = |
64304 | 8 |
sig |
9 |
val string: string -> string |
|
10 |
val strings: string list -> string |
|
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
11 |
type params |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
12 |
val dest_params: params -> |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
13 |
{script: string, input: string, cwd: Path.T option, putenv: (string * string) list, |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
14 |
redirect: bool, timeout: Time.time, description: string} |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
15 |
val script: string -> params |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
16 |
val input: string -> params -> params |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
17 |
val cwd: Path.T -> params -> params |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
18 |
val putenv: (string * string) list -> params -> params |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
19 |
val redirect: params -> params |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
20 |
val timeout: Time.time -> params -> params |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
21 |
val description: string -> params -> params |
74210 | 22 |
val server_run: string |
23 |
val server_kill: string |
|
24 |
val server_uuid: string |
|
25 |
val server_interrupt: string |
|
26 |
val server_failure: string |
|
27 |
val server_result: string |
|
64304 | 28 |
end; |
29 |
||
73264 | 30 |
structure Bash: BASH = |
64304 | 31 |
struct |
32 |
||
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
33 |
(* concrete syntax *) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
34 |
|
64304 | 35 |
fun string "" = "\"\"" |
36 |
| string str = |
|
37 |
str |> translate_string (fn ch => |
|
38 |
let val c = ord ch in |
|
39 |
(case ch of |
|
40 |
"\t" => "$'\\t'" |
|
41 |
| "\n" => "$'\\n'" |
|
42 |
| "\f" => "$'\\f'" |
|
43 |
| "\r" => "$'\\r'" |
|
44 |
| _ => |
|
45 |
if Symbol.is_ascii_letter ch orelse Symbol.is_ascii_digit ch orelse |
|
67200 | 46 |
exists_string (fn c => c = ch) "+,-./:_" then ch |
64304 | 47 |
else if c < 16 then "$'\\x0" ^ Int.fmt StringCvt.HEX c ^ "'" |
48 |
else if c < 32 orelse c >= 127 then "$'\\x" ^ Int.fmt StringCvt.HEX c ^ "'" |
|
49 |
else "\\" ^ ch) |
|
50 |
end); |
|
51 |
||
52 |
val strings = space_implode " " o map string; |
|
53 |
||
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
54 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
55 |
(* server parameters *) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
56 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
57 |
abstype params = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
58 |
Params of |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
59 |
{script: string, input: string, cwd: Path.T option, putenv: (string * string) list, |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
60 |
redirect: bool, timeout: Time.time, description: string} |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
61 |
with |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
62 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
63 |
fun dest_params (Params args) = args; |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
64 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
65 |
fun make_params (script, input, cwd, putenv, redirect, timeout, description) = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
66 |
Params {script = script, input = input, cwd = cwd, putenv = putenv, redirect = redirect, |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
67 |
timeout = timeout, description = description}; |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
68 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
69 |
fun map_params f (Params {script, input, cwd, putenv, redirect, timeout, description}) = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
70 |
make_params (f (script, input, cwd, putenv, redirect, timeout, description)); |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
71 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
72 |
fun script script = make_params (script, "", NONE, [], false, Time.zeroTime, ""); |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
73 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
74 |
fun input input = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
75 |
map_params (fn (script, _, cwd, putenv, redirect, timeout, description) => |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
76 |
(script, input, cwd, putenv, redirect, timeout, description)); |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
77 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
78 |
fun cwd cwd = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
79 |
map_params (fn (script, input, _, putenv, redirect, timeout, description) => |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
80 |
(script, input, SOME cwd, putenv, redirect, timeout, description)); |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
81 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
82 |
fun putenv putenv = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
83 |
map_params (fn (script, input, cwd, _, redirect, timeout, description) => |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
84 |
(script, input, cwd, putenv, redirect, timeout, description)); |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
85 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
86 |
val redirect = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
87 |
map_params (fn (script, input, cwd, putenv, _, timeout, description) => |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
88 |
(script, input, cwd, putenv, true, timeout, description)); |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
89 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
90 |
fun timeout timeout = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
91 |
map_params (fn (script, input, cwd, putenv, redirect, _, description) => |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
92 |
(script, input, cwd, putenv, redirect, timeout, description)); |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
93 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
94 |
fun description description = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
95 |
map_params (fn (script, input, cwd, putenv, redirect, timeout, _) => |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
96 |
(script, input, cwd, putenv, redirect, timeout, description)); |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
97 |
|
64304 | 98 |
end; |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
99 |
|
74210 | 100 |
|
101 |
(* server messages *) |
|
102 |
||
103 |
val server_run = "run"; |
|
104 |
val server_kill = "kill"; |
|
105 |
||
106 |
val server_uuid = "uuid"; |
|
107 |
val server_interrupt = "interrupt"; |
|
108 |
val server_failure = "failure"; |
|
109 |
val server_result = "result"; |
|
110 |
||
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
111 |
end; |