| changeset 75621 | aeb412065742 |
| parent 75620 | 44815dc2b8f9 |
| child 76183 | 8089593a364a |
| 75620:44815dc2b8f9 | 75621:aeb412065742 |
|---|---|
11 end; |
11 end; |
12 |
12 |
13 structure XZ: XZ = |
13 structure XZ: XZ = |
14 struct |
14 struct |
15 |
15 |
16 val compress = Scala.function1_bytes "XZ.compress"; |
16 val compress = \<^scala>\<open>XZ.compress\<close>; |
17 val uncompress = Scala.function1_bytes "XZ.uncompress"; |
17 val uncompress = \<^scala>\<open>XZ.uncompress\<close>; |
18 |
18 |
19 end; |
19 end; |