src/Pure/System/isabelle_system.ML
changeset 75620 44815dc2b8f9
parent 75579 3362b6a5d697
child 78672 fcdfd3251892
equal deleted inserted replaced
75619:9639c3867b86 75620:44815dc2b8f9
    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";