# HG changeset patch
# User wenzelm
# Date 1364137965 -3600
# Node ID 18095684c5a6f52997342c0ca69d69a4a1259509
# Parent  5247f5cd68fd3d2e344452e41b13ead3d41adbda
basic support for xz files;

diff -r 5247f5cd68fd -r 18095684c5a6 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Sun Mar 24 16:10:19 2013 +0100
+++ b/src/Pure/General/file.scala	Sun Mar 24 16:12:45 2013 +0100
@@ -8,12 +8,14 @@
 
 
 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
-  InputStream, FileInputStream, BufferedInputStream, BufferedReader, InputStreamReader,
-  File => JFile, IOException}
+  OutputStream, InputStream, FileInputStream, BufferedInputStream, BufferedReader,
+  InputStreamReader, File => JFile, IOException}
 import java.util.zip.{GZIPInputStream, GZIPOutputStream}
 
 import scala.collection.mutable
 
+import org.tukaani.xz.{LZMA2Options, XZInputStream, XZOutputStream}
+
 
 object File
 {
@@ -72,8 +74,14 @@
 
   def read_gzip(file: JFile): String =
     read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(file))))
+
   def read_gzip(path: Path): String = read_gzip(path.file)
 
+  def read_xz(file: JFile): String =
+    read_stream(new XZInputStream(new BufferedInputStream(new FileInputStream(file))))
+
+  def read_xz(path: Path): String = read_xz(path.file)
+
 
   /* read lines */
 
@@ -105,21 +113,39 @@
 
   /* write */
 
-  private def write_file(file: JFile, text: CharSequence, gzip: Boolean)
+  private def write_file(file: JFile, text: CharSequence, make_stream: OutputStream => OutputStream)
   {
-    val stream1 = new FileOutputStream(file)
-    val stream2 = if (gzip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1
-    val writer = new BufferedWriter(new OutputStreamWriter(stream2, UTF8.charset))
-    try { writer.append(text) }
-    finally { writer.close }
+    val stream = make_stream(new FileOutputStream(file))
+    val writer = new BufferedWriter(new OutputStreamWriter(stream, UTF8.charset))
+    try { writer.append(text) } finally { writer.close }
   }
 
-  def write(file: JFile, text: CharSequence): Unit = write_file(file, text, false)
+  def write(file: JFile, text: CharSequence): Unit = write_file(file, text, (s) => s)
+
   def write(path: Path, text: CharSequence): Unit = write(path.file, text)
 
-  def write_gzip(file: JFile, text: CharSequence): Unit = write_file(file, text, true)
+  def write_gzip(file: JFile, text: CharSequence): Unit =
+    write_file(file, text, (s: OutputStream) => new GZIPOutputStream(new BufferedOutputStream(s)))
+
   def write_gzip(path: Path, text: CharSequence): Unit = write_gzip(path.file, text)
 
+  def write_xz(file: JFile, text: CharSequence, preset: Int)
+  {
+    val options = new LZMA2Options
+    options.setPreset(preset)
+    write_file(file, text, (s: OutputStream) =>
+      new XZOutputStream(new BufferedOutputStream(s), options))
+  }
+
+  def write_xz(file: JFile, text: CharSequence): Unit =
+    write_xz(file, text, LZMA2Options.PRESET_DEFAULT)
+
+  def write_xz(path: Path, text: CharSequence, preset: Int): Unit =
+    write_xz(path.file, text, preset)
+
+  def write_xz(path: Path, text: CharSequence): Unit =
+    write_xz(path.file, text, LZMA2Options.PRESET_DEFAULT)
+
 
   /* copy */
 
diff -r 5247f5cd68fd -r 18095684c5a6 src/Pure/build-jars
--- a/src/Pure/build-jars	Sun Mar 24 16:10:19 2013 +0100
+++ b/src/Pure/build-jars	Sun Mar 24 16:12:45 2013 +0100
@@ -196,7 +196,7 @@
   JFXRT="$ISABELLE_JDK_HOME/jre/lib/jfxrt.jar"
 
   (
-    for X in "$JFXRT" "${JFREECHART_JARS[@]}" classes
+    for X in "$JFXRT" "${JFREECHART_JARS[@]}" "$XZ_JAVA_HOME/lib/xz.jar" classes
     do
       CLASSPATH="$CLASSPATH:$X"
     done
diff -r 5247f5cd68fd -r 18095684c5a6 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Sun Mar 24 16:10:19 2013 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Sun Mar 24 16:12:45 2013 +0100
@@ -233,7 +233,7 @@
   else
     if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
       declare -a DEPS=(
-        "$JEDIT_JAR" "${JEDIT_JARS[@]}" "${JFREECHART_JARS[@]}"
+        "$JEDIT_JAR" "${JEDIT_JARS[@]}" "${JFREECHART_JARS[@]}" "$XZ_JAVA_HOME/lib/xz.jar"
         "$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}"
       )
     elif [ -e "$ISABELLE_HOME/Admin/build" ]; then
@@ -287,8 +287,8 @@
 
   cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed
   (
-    for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "${JFREECHART_JARS[@]}" "$PURE_JAR" \
-      "$GRAPHVIEW_JAR" "$SCALA_HOME/lib/scala-compiler.jar"
+    for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "${JFREECHART_JARS[@]}" "$XZ_JAVA_HOME/lib/xz.jar" \
+      "$PURE_JAR" "$GRAPHVIEW_JAR" "$SCALA_HOME/lib/scala-compiler.jar"
     do
       CLASSPATH="$CLASSPATH:$JAR"
     done