author | wenzelm |
Thu, 19 Aug 2021 12:01:57 +0200 | |
changeset 74158 | 1cb0ad6f9a2d |
parent 74147 | d030b988d470 |
child 74210 | c14774713d62 |
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 |
64304 | 22 |
end; |
23 |
||
73264 | 24 |
structure Bash: BASH = |
64304 | 25 |
struct |
26 |
||
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
27 |
(* concrete syntax *) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
28 |
|
64304 | 29 |
fun string "" = "\"\"" |
30 |
| string str = |
|
31 |
str |> translate_string (fn ch => |
|
32 |
let val c = ord ch in |
|
33 |
(case ch of |
|
34 |
"\t" => "$'\\t'" |
|
35 |
| "\n" => "$'\\n'" |
|
36 |
| "\f" => "$'\\f'" |
|
37 |
| "\r" => "$'\\r'" |
|
38 |
| _ => |
|
39 |
if Symbol.is_ascii_letter ch orelse Symbol.is_ascii_digit ch orelse |
|
67200 | 40 |
exists_string (fn c => c = ch) "+,-./:_" then ch |
64304 | 41 |
else if c < 16 then "$'\\x0" ^ Int.fmt StringCvt.HEX c ^ "'" |
42 |
else if c < 32 orelse c >= 127 then "$'\\x" ^ Int.fmt StringCvt.HEX c ^ "'" |
|
43 |
else "\\" ^ ch) |
|
44 |
end); |
|
45 |
||
46 |
val strings = space_implode " " o map string; |
|
47 |
||
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
48 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
49 |
(* server parameters *) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
50 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
51 |
abstype params = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
52 |
Params of |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
53 |
{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
|
54 |
redirect: bool, timeout: Time.time, description: string} |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
55 |
with |
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 |
fun dest_params (Params args) = args; |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
58 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
59 |
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
|
60 |
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
|
61 |
timeout = timeout, description = description}; |
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 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
|
64 |
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
|
65 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
66 |
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
|
67 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
68 |
fun input input = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
69 |
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
|
70 |
(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 cwd cwd = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
73 |
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
|
74 |
(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
|
75 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
76 |
fun putenv putenv = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
77 |
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
|
78 |
(script, input, cwd, putenv, redirect, timeout, description)); |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
79 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
80 |
val redirect = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
81 |
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
|
82 |
(script, input, cwd, putenv, true, timeout, description)); |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
83 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
84 |
fun timeout timeout = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
85 |
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
|
86 |
(script, input, cwd, putenv, redirect, timeout, description)); |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
87 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
88 |
fun description description = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
89 |
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
|
90 |
(script, input, cwd, putenv, redirect, timeout, description)); |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
73264
diff
changeset
|
91 |
|
64304 | 92 |
end; |
74147
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 |
end; |