equal
deleted
inserted
replaced
20 val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a |
20 val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a |
21 val rm_tree: Path.T -> unit |
21 val rm_tree: Path.T -> unit |
22 val with_tmp_dir: string -> (Path.T -> 'a) -> 'a |
22 val with_tmp_dir: string -> (Path.T -> 'a) -> 'a |
23 val download: string -> Bytes.T |
23 val download: string -> Bytes.T |
24 val download_file: string -> Path.T -> unit |
24 val download_file: string -> Path.T -> unit |
25 val decode_base64: Bytes.T -> Bytes.T |
|
26 val encode_base64: Bytes.T -> Bytes.T |
|
27 val compress: Bytes.T -> Bytes.T |
|
28 val uncompress: Bytes.T -> Bytes.T |
|
29 val isabelle_id: unit -> string |
25 val isabelle_id: unit -> string |
30 val isabelle_identifier: unit -> string option |
26 val isabelle_identifier: unit -> string option |
31 val isabelle_heading: unit -> string |
27 val isabelle_heading: unit -> string |
32 val isabelle_name: unit -> string |
28 val isabelle_name: unit -> string |
33 val identification: unit -> string |
29 val identification: unit -> string |
161 val download = Bytes.string #> Scala.function1_bytes "download"; |
157 val download = Bytes.string #> Scala.function1_bytes "download"; |
162 |
158 |
163 fun download_file url path = Bytes.write path (download url); |
159 fun download_file url path = Bytes.write path (download url); |
164 |
160 |
165 |
161 |
166 (* base64 *) |
|
167 |
|
168 val decode_base64 = Scala.function1_bytes "decode_base64"; |
|
169 val encode_base64 = Scala.function1_bytes "encode_base64"; |
|
170 |
|
171 |
|
172 (* XZ compression *) |
|
173 |
|
174 val compress = Scala.function1_bytes "compress"; |
|
175 val uncompress = Scala.function1_bytes "uncompress"; |
|
176 |
|
177 |
|
178 (* Isabelle distribution identification *) |
162 (* Isabelle distribution identification *) |
179 |
163 |
180 fun isabelle_id () = Scala.function1 "isabelle_id" ""; |
164 fun isabelle_id () = Scala.function1 "isabelle_id" ""; |
181 |
165 |
182 fun isabelle_identifier () = try getenv_strict "ISABELLE_IDENTIFIER"; |
166 fun isabelle_identifier () = try getenv_strict "ISABELLE_IDENTIFIER"; |