src/Pure/System/bash.ML
changeset 74210 c14774713d62
parent 74158 1cb0ad6f9a2d
child 77851 ec50b9213969
equal deleted inserted replaced
74209:24a2a6ced0ab 74210:c14774713d62
    17   val cwd: Path.T -> params -> params
    17   val cwd: Path.T -> params -> params
    18   val putenv: (string * string) list -> params -> params
    18   val putenv: (string * string) list -> params -> params
    19   val redirect: params -> params
    19   val redirect: params -> params
    20   val timeout: Time.time -> params -> params
    20   val timeout: Time.time -> params -> params
    21   val description: string -> params -> params
    21   val description: string -> params -> params
       
    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
    22 end;
    28 end;
    23 
    29 
    24 structure Bash: BASH =
    30 structure Bash: BASH =
    25 struct
    31 struct
    26 
    32 
    89   map_params (fn (script, input, cwd, putenv, redirect, timeout, _) =>
    95   map_params (fn (script, input, cwd, putenv, redirect, timeout, _) =>
    90     (script, input, cwd, putenv, redirect, timeout, description));
    96     (script, input, cwd, putenv, redirect, timeout, description));
    91 
    97 
    92 end;
    98 end;
    93 
    99 
       
   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 
    94 end;
   111 end;