clarified modules;
authorwenzelm
Sun Oct 02 22:05:40 2016 +0200 (2016-10-02)
changeset 64000445b3deced8f
parent 63999 5649a993666d
child 64001 7ecb22be8f03
clarified modules;
src/Pure/General/file.scala
src/Pure/General/xz.scala
src/Pure/General/xz_file.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/General/file.scala	Sun Oct 02 21:05:14 2016 +0200
     1.2 +++ b/src/Pure/General/file.scala	Sun Oct 02 22:05:40 2016 +0200
     1.3 @@ -190,12 +190,14 @@
     1.4    }
     1.5  
     1.6    def read_stream(stream: InputStream): String =
     1.7 -   read_stream(new BufferedReader(new InputStreamReader(stream, UTF8.charset)))
     1.8 +    read_stream(new BufferedReader(new InputStreamReader(stream, UTF8.charset)))
     1.9  
    1.10    def read_gzip(file: JFile): String =
    1.11      read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(file))))
    1.12 +  def read_gzip(path: Path): String = read_gzip(path.file)
    1.13  
    1.14 -  def read_gzip(path: Path): String = read_gzip(path.file)
    1.15 +  def read_xz(file: JFile): String = read_stream(XZ.uncompress(new FileInputStream(file)))
    1.16 +  def read_xz(path: Path): String = read_xz(path.file)
    1.17  
    1.18  
    1.19    /* read lines */
    1.20 @@ -235,6 +237,11 @@
    1.21    def write_gzip(path: Path, text: Iterable[CharSequence]): Unit = write_gzip(path.file, text)
    1.22    def write_gzip(path: Path, text: CharSequence): Unit = write_gzip(path.file, text)
    1.23  
    1.24 +  def write_xz(file: JFile, text: Iterable[CharSequence]): Unit = XZ.write_file(file, text)
    1.25 +  def write_xz(file: JFile, text: CharSequence): Unit = XZ.write_file(file, List(text))
    1.26 +  def write_xz(path: Path, text: Iterable[CharSequence]): Unit = XZ.write_file(path.file, text)
    1.27 +  def write_xz(path: Path, text: CharSequence): Unit = XZ.write_file(path.file, List(text))
    1.28 +
    1.29    def write_backup(path: Path, text: CharSequence)
    1.30    {
    1.31      path.file renameTo path.backup.file
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/General/xz.scala	Sun Oct 02 22:05:40 2016 +0200
     2.3 @@ -0,0 +1,32 @@
     2.4 +/*  Title:      Pure/General/xz.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +XZ data compression.
     2.8 +*/
     2.9 +
    2.10 +package isabelle
    2.11 +
    2.12 +
    2.13 +import java.io.{File => JFile, BufferedOutputStream, OutputStream, InputStream, BufferedInputStream}
    2.14 +
    2.15 +import org.tukaani.xz.{LZMA2Options, XZInputStream, XZOutputStream}
    2.16 +
    2.17 +
    2.18 +object XZ
    2.19 +{
    2.20 +  def options(preset: Int): LZMA2Options =
    2.21 +  {
    2.22 +    val opts = new LZMA2Options
    2.23 +    opts.setPreset(preset)
    2.24 +    opts
    2.25 +  }
    2.26 +
    2.27 +  def write_file(file: JFile, text: Iterable[CharSequence], preset: Int = 3)
    2.28 +  {
    2.29 +    val opts = options(preset)
    2.30 +    File.write_file(file, text,
    2.31 +      (s: OutputStream) => new XZOutputStream(new BufferedOutputStream(s), opts))
    2.32 +  }
    2.33 +
    2.34 +  def uncompress(s: InputStream): XZInputStream = new XZInputStream(new BufferedInputStream(s))
    2.35 +}
     3.1 --- a/src/Pure/General/xz_file.scala	Sun Oct 02 21:05:14 2016 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,31 +0,0 @@
     3.4 -/*  Title:      Pure/General/xz_file.scala
     3.5 -    Author:     Makarius
     3.6 -
     3.7 -XZ file system operations.
     3.8 -*/
     3.9 -
    3.10 -package isabelle
    3.11 -
    3.12 -
    3.13 -import java.io.{BufferedOutputStream, OutputStream, FileInputStream, BufferedInputStream,
    3.14 -  File => JFile}
    3.15 -
    3.16 -import org.tukaani.xz.{LZMA2Options, XZInputStream, XZOutputStream}
    3.17 -
    3.18 -
    3.19 -object XZ_File
    3.20 -{
    3.21 -  def read(file: JFile): String =
    3.22 -    File.read_stream(new XZInputStream(new BufferedInputStream(new FileInputStream(file))))
    3.23 -
    3.24 -  def read(path: Path): String = read(path.file)
    3.25 -
    3.26 -  def write(file: JFile, text: Iterable[CharSequence], preset: Int = 3)
    3.27 -  {
    3.28 -    val options = new LZMA2Options
    3.29 -    options.setPreset(preset)
    3.30 -    File.write_file(file, text, (s: OutputStream) =>
    3.31 -      new XZOutputStream(new BufferedOutputStream(s), options))
    3.32 -  }
    3.33 -}
    3.34 -
     4.1 --- a/src/Pure/build-jars	Sun Oct 02 21:05:14 2016 +0200
     4.2 +++ b/src/Pure/build-jars	Sun Oct 02 22:05:40 2016 +0200
     4.3 @@ -54,7 +54,7 @@
     4.4    General/url.scala
     4.5    General/value.scala
     4.6    General/word.scala
     4.7 -  General/xz_file.scala
     4.8 +  General/xz.scala
     4.9    Isar/document_structure.scala
    4.10    Isar/keyword.scala
    4.11    Isar/line_structure.scala