src/Pure/General/xz.scala
changeset 64002 08f89f0e8a62
parent 64000 445b3deced8f
child 64004 b4ece7a3f2ca
equal deleted inserted replaced
64001:7ecb22be8f03 64002:08f89f0e8a62
     1 /*  Title:      Pure/General/xz.scala
     1 /*  Title:      Pure/General/xz.scala
     2     Author:     Makarius
     2     Author:     Makarius
     3 
     3 
     4 XZ data compression.
     4 Support for XZ data compression.
     5 */
     5 */
     6 
     6 
     7 package isabelle
     7 package isabelle
     8 
     8 
     9 
     9 
    10 import java.io.{File => JFile, BufferedOutputStream, OutputStream, InputStream, BufferedInputStream}
    10 import org.tukaani.xz.LZMA2Options
    11 
       
    12 import org.tukaani.xz.{LZMA2Options, XZInputStream, XZOutputStream}
       
    13 
    11 
    14 
    12 
    15 object XZ
    13 object XZ
    16 {
    14 {
    17   def options(preset: Int): LZMA2Options =
    15   type Options = LZMA2Options
       
    16 
       
    17   def options(): Options = options_preset(3)
       
    18 
       
    19   def options_preset(preset: Int): Options =
    18   {
    20   {
    19     val opts = new LZMA2Options
    21     val opts = new LZMA2Options
    20     opts.setPreset(preset)
    22     opts.setPreset(preset)
    21     opts
    23     opts
    22   }
    24   }
    23 
       
    24   def write_file(file: JFile, text: Iterable[CharSequence], preset: Int = 3)
       
    25   {
       
    26     val opts = options(preset)
       
    27     File.write_file(file, text,
       
    28       (s: OutputStream) => new XZOutputStream(new BufferedOutputStream(s), opts))
       
    29   }
       
    30 
       
    31   def uncompress(s: InputStream): XZInputStream = new XZInputStream(new BufferedInputStream(s))
       
    32 }
    25 }