src/Pure/General/xz.ML
author wenzelm
Wed, 11 Sep 2024 22:28:42 +0200
changeset 80863 af34fcf7215d
parent 76183 8089593a364a
permissions -rw-r--r--
tuned signature: more operations;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
76183
8089593a364a proper file headers;
wenzelm
parents: 75621
diff changeset
     1
(*  Title:      Pure/General/xz.ML
75620
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
     3
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
     4
Support for XZ compression (via Isabelle/Scala).
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
     5
*)
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
     6
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
     7
signature XZ =
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
     8
sig
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
     9
  val compress: Bytes.T -> Bytes.T
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    10
  val uncompress: Bytes.T -> Bytes.T
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    11
end;
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    12
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    13
structure XZ: XZ =
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    14
struct
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    15
75621
aeb412065742 prefer antiquotations;
wenzelm
parents: 75620
diff changeset
    16
val compress = \<^scala>\<open>XZ.compress\<close>;
aeb412065742 prefer antiquotations;
wenzelm
parents: 75620
diff changeset
    17
val uncompress = \<^scala>\<open>XZ.uncompress\<close>;
75620
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    18
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    19
end;