src/Pure/General/xz_file.scala
author wenzelm
Sat, 22 Feb 2014 20:52:43 +0100
changeset 55672 5e25cc741ab9
parent 52671 9a360530eac8
permissions -rw-r--r--
support for completion within the formal context; tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
52671
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/xz_file.scala
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
     3
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
     4
XZ file system operations.
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
     5
*/
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
     6
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
     7
package isabelle
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
     8
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
     9
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    10
import java.io.{BufferedOutputStream, OutputStream, FileInputStream, BufferedInputStream,
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    11
  File => JFile}
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    12
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    13
import org.tukaani.xz.{LZMA2Options, XZInputStream, XZOutputStream}
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    14
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    15
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    16
object XZ_File
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    17
{
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    18
  def read(file: JFile): String =
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    19
    File.read_stream(new XZInputStream(new BufferedInputStream(new FileInputStream(file))))
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    20
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    21
  def read(path: Path): String = read(path.file)
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    22
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    23
  def write(file: JFile, text: Iterable[CharSequence], preset: Int = 3)
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    24
  {
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    25
    val options = new LZMA2Options
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    26
    options.setPreset(preset)
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    27
    File.write_file(file, text, (s: OutputStream) =>
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    28
      new XZOutputStream(new BufferedOutputStream(s), options))
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    29
  }
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    30
}
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    31