# HG changeset patch # User wenzelm # Date 1656155955 -7200 # Node ID 44815dc2b8f9fc9e3fca9bc0818c50c49889dab2 # Parent 9639c3867b86e4e393f9659f438e34742c8acb1b clarified modules; diff -r 9639c3867b86 -r 44815dc2b8f9 NEWS --- a/NEWS Sat Jun 25 10:27:42 2022 +0200 +++ b/NEWS Sat Jun 25 13:19:15 2022 +0200 @@ -171,8 +171,8 @@ * Operations for XZ compression (via Isabelle/Scala): - Isabelle_System.compress: Bytes.T -> Bytes.T - Isabelle_System.uncompress: Bytes.T -> Bytes.T + XZ.compress: Bytes.T -> Bytes.T + XZ.uncompress: Bytes.T -> Bytes.T *** System *** diff -r 9639c3867b86 -r 44815dc2b8f9 etc/build.props --- a/etc/build.props Sat Jun 25 10:27:42 2022 +0200 +++ b/etc/build.props Sat Jun 25 13:19:15 2022 +0200 @@ -54,6 +54,7 @@ src/Pure/GUI/popup.scala \ src/Pure/GUI/wrap_panel.scala \ src/Pure/General/antiquote.scala \ + src/Pure/General/base64.scala \ src/Pure/General/bytes.scala \ src/Pure/General/cache.scala \ src/Pure/General/codepoint.scala \ diff -r 9639c3867b86 -r 44815dc2b8f9 src/Pure/General/base64.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/base64.ML Sat Jun 25 13:19:15 2022 +0200 @@ -0,0 +1,19 @@ +(* Title: Pure/System/base64.ML + Author: Makarius + +Support for Base64 data encoding (via Isabelle/Scala). +*) + +signature BASE64 = +sig + val decode: Bytes.T -> Bytes.T + val encode: Bytes.T -> Bytes.T +end; + +structure Base64: BASE64 = +struct + +val decode = Scala.function1_bytes "Base64.decode"; +val encode = Scala.function1_bytes "Base64.encode"; + +end; diff -r 9639c3867b86 -r 44815dc2b8f9 src/Pure/General/base64.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/base64.scala Sat Jun 25 13:19:15 2022 +0200 @@ -0,0 +1,26 @@ +/* Title: Pure/General/base64.scala + Author: Makarius + +Support for Base64 data encoding. +*/ + +package isabelle + + +object Base64 { + def encode(a: Array[Byte]): String = java.util.Base64.getEncoder.encodeToString(a) + def decode(s: String): Array[Byte] = java.util.Base64.getDecoder.decode(s) + + + /* Scala functions in ML */ + + object Decode extends Scala.Fun_Bytes("Base64.decode") { + val here = Scala_Project.here + def apply(arg: Bytes): Bytes = Bytes.decode_base64(arg.text) + } + + object Encode extends Scala.Fun_Bytes("Base64.encode") { + val here = Scala_Project.here + def apply(arg: Bytes): Bytes = Bytes(arg.encode_base64) + } +} diff -r 9639c3867b86 -r 44815dc2b8f9 src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala Sat Jun 25 10:27:42 2022 +0200 +++ b/src/Pure/General/bytes.scala Sat Jun 25 13:19:15 2022 +0200 @@ -10,7 +10,6 @@ import java.io.{File => JFile, ByteArrayOutputStream, ByteArrayInputStream, OutputStream, InputStream, FileInputStream, FileOutputStream} import java.net.URL -import java.util.Base64 import org.tukaani.xz.{XZInputStream, XZOutputStream} @@ -43,33 +42,10 @@ /* base64 */ def decode_base64(s: String): Bytes = { - val a = Base64.getDecoder.decode(s) + val a = Base64.decode(s) new Bytes(a, 0, a.length) } - object Decode_Base64 extends Scala.Fun_Bytes("decode_base64") { - val here = Scala_Project.here - def apply(arg: Bytes): Bytes = decode_base64(arg.text) - } - - object Encode_Base64 extends Scala.Fun_Bytes("encode_base64") { - val here = Scala_Project.here - def apply(arg: Bytes): Bytes = Bytes(arg.encode_base64) - } - - - /* XZ compression */ - - object Compress extends Scala.Fun_Bytes("compress") { - val here = Scala_Project.here - def apply(arg: Bytes): Bytes = arg.compress() - } - - object Uncompress extends Scala.Fun_Bytes("uncompress") { - val here = Scala_Project.here - def apply(arg: Bytes): Bytes = arg.uncompress() - } - /* read */ @@ -160,7 +136,7 @@ val b = if (offset == 0 && length == bytes.length) bytes else Bytes(bytes, offset, length).bytes - Base64.getEncoder.encodeToString(b) + Base64.encode(b) } def maybe_encode_base64: (Boolean, String) = { diff -r 9639c3867b86 -r 44815dc2b8f9 src/Pure/General/xz.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/xz.ML Sat Jun 25 13:19:15 2022 +0200 @@ -0,0 +1,19 @@ +(* Title: Pure/System/xz.ML + Author: Makarius + +Support for XZ compression (via Isabelle/Scala). +*) + +signature XZ = +sig + val compress: Bytes.T -> Bytes.T + val uncompress: Bytes.T -> Bytes.T +end; + +structure XZ: XZ = +struct + +val compress = Scala.function1_bytes "XZ.compress"; +val uncompress = Scala.function1_bytes "XZ.uncompress"; + +end; diff -r 9639c3867b86 -r 44815dc2b8f9 src/Pure/General/xz.scala --- a/src/Pure/General/xz.scala Sat Jun 25 10:27:42 2022 +0200 +++ b/src/Pure/General/xz.scala Sat Jun 25 13:19:15 2022 +0200 @@ -31,4 +31,17 @@ def apply(): ArrayCache = ArrayCache.getDefaultCache() def make(): ArrayCache = new BasicArrayCache } + + + /* Scala functions in ML */ + + object Compress extends Scala.Fun_Bytes("XZ.compress") { + val here = Scala_Project.here + def apply(arg: Bytes): Bytes = arg.compress() + } + + object Uncompress extends Scala.Fun_Bytes("XZ.uncompress") { + val here = Scala_Project.here + def apply(arg: Bytes): Bytes = arg.uncompress() + } } diff -r 9639c3867b86 -r 44815dc2b8f9 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Sat Jun 25 10:27:42 2022 +0200 +++ b/src/Pure/ROOT.ML Sat Jun 25 13:19:15 2022 +0200 @@ -300,6 +300,8 @@ ML_file "System/scala.ML"; ML_file "System/process_result.ML"; ML_file "System/isabelle_system.ML"; +ML_file "General/base64.ML"; +ML_file "General/xz.ML"; (*theory documents*) diff -r 9639c3867b86 -r 44815dc2b8f9 src/Pure/System/isabelle_system.ML --- a/src/Pure/System/isabelle_system.ML Sat Jun 25 10:27:42 2022 +0200 +++ b/src/Pure/System/isabelle_system.ML Sat Jun 25 13:19:15 2022 +0200 @@ -22,10 +22,6 @@ val with_tmp_dir: string -> (Path.T -> 'a) -> 'a val download: string -> Bytes.T val download_file: string -> Path.T -> unit - val decode_base64: Bytes.T -> Bytes.T - val encode_base64: Bytes.T -> Bytes.T - val compress: Bytes.T -> Bytes.T - val uncompress: Bytes.T -> Bytes.T val isabelle_id: unit -> string val isabelle_identifier: unit -> string option val isabelle_heading: unit -> string @@ -163,18 +159,6 @@ fun download_file url path = Bytes.write path (download url); -(* base64 *) - -val decode_base64 = Scala.function1_bytes "decode_base64"; -val encode_base64 = Scala.function1_bytes "encode_base64"; - - -(* XZ compression *) - -val compress = Scala.function1_bytes "compress"; -val uncompress = Scala.function1_bytes "uncompress"; - - (* Isabelle distribution identification *) fun isabelle_id () = Scala.function1 "isabelle_id" ""; diff -r 9639c3867b86 -r 44815dc2b8f9 src/Pure/System/scala.scala --- a/src/Pure/System/scala.scala Sat Jun 25 10:27:42 2022 +0200 +++ b/src/Pure/System/scala.scala Sat Jun 25 13:19:15 2022 +0200 @@ -323,10 +323,10 @@ Scala.Echo, Scala.Sleep, Scala.Toplevel, - Bytes.Decode_Base64, - Bytes.Encode_Base64, - Bytes.Compress, - Bytes.Uncompress, + Base64.Decode, + Base64.Encode, + XZ.Compress, + XZ.Uncompress, Doc.Doc_Names, Bibtex.Check_Database, Isabelle_System.Make_Directory,