[isabelle-dev] NEWS: Isabelle/ML type Bytes.T and XZ compression

[Makarius]

*** ML ***

* Type Bytes.T supports scalable byte strings, beyond the limit of
String.maxSize (approx. 64 MB on 64_32 architecture).

* Operations for XZ compression (via Isabelle/Scala):

   XZ.compress: Bytes.T -> Bytes.T
   XZ.uncompress: Bytes.T -> Bytes.T


This refers to Isabelle/44815dc2b8f9.

It might be occasionally useful to have XZ (un)compression available in 
Isabelle/ML. XZ is the standard compression scheme of Isabelle/Scala.

The main point of the exercise, though, is to show how to implement this my 
mostly trivial means, see: 
https://isabelle.sketis.net/repos/isabelle/file/44815dc2b8f9/src/Pure/General/xz.ML 
and 
https://isabelle.sketis.net/repos/isabelle/file/44815dc2b8f9/src/Pure/General/xz.scala


A similar application is Base64 recoding in 
https://isabelle.sketis.net/repos/isabelle/file/44815dc2b8f9/src/Pure/General/base64.ML 
and 
https://isabelle.sketis.net/repos/isabelle/file/44815dc2b8f9/src/Pure/General/base64.scala


	Makarius