--- a/src/Pure/General/bytes.ML Wed Jun 22 14:52:27 2022 +0200
+++ b/src/Pure/General/bytes.ML Wed Jun 22 17:07:00 2022 +0200
@@ -30,6 +30,10 @@
val string: string -> T
val newline: T
val buffer: Buffer.T -> T
+ val space_explode: string -> T -> string list
+ val split_lines: T -> string list
+ val trim_split_lines: T -> string list
+ val cat_lines: string list -> T
val read_block: int -> BinIO.instream -> string
val read_stream: int -> BinIO.instream -> T
val write_stream: BinIO.outstream -> T -> unit
@@ -138,6 +142,49 @@
val buffer = build o fold add o Buffer.contents;
+
+(* space_explode *)
+
+fun space_explode sep bytes =
+ if is_empty bytes then []
+ else if size sep <> 1 then [content bytes]
+ else
+ let
+ val sep_char = String.sub (sep, 0);
+
+ fun add_part s part =
+ Buffer.add (Substring.string s) (the_default Buffer.empty part);
+
+ fun explode head tail part res =
+ if Substring.isEmpty head then
+ (case tail of
+ [] =>
+ (case part of
+ NONE => rev res
+ | SOME buf => rev (Buffer.content buf :: res))
+ | chunk :: chunks => explode (Substring.full chunk) chunks part res)
+ else
+ (case Substring.fields (fn c => c = sep_char) head of
+ [a] => explode Substring.empty tail (SOME (add_part a part)) res
+ | a :: rest =>
+ let
+ val (bs, c) = split_last rest;
+ val res' = res
+ |> cons (Buffer.content (add_part a part))
+ |> fold (cons o Substring.string) bs;
+ val part' = SOME (add_part c NONE);
+ in explode Substring.empty tail part' res' end)
+ in explode Substring.empty (contents bytes) NONE [] end;
+
+val split_lines = space_explode "\n";
+
+val trim_split_lines = trim_line #> split_lines #> map Library.trim_line;
+
+fun cat_lines lines = build (fold add (separate "\n" lines));
+
+
+(* IO *)
+
fun read_block limit =
File.input_size (if limit < 0 then chunk_size else Int.min (chunk_size, limit));
--- a/src/Pure/General/bytes.scala Wed Jun 22 14:52:27 2022 +0200
+++ b/src/Pure/General/bytes.scala Wed Jun 22 17:07:00 2022 +0200
@@ -42,36 +42,32 @@
/* base64 */
- def base64(s: String): Bytes = {
+ def decode_base64(s: String): Bytes = {
val a = Base64.getDecoder.decode(s)
new Bytes(a, 0, a.length)
}
- object Decode_Base64 extends Scala.Fun("decode_base64") {
+ object Decode_Base64 extends Scala.Fun_Bytes("decode_base64") {
val here = Scala_Project.here
- def invoke(args: List[Bytes]): List[Bytes] =
- List(base64(Library.the_single(args).text))
+ def apply(arg: Bytes): Bytes = decode_base64(arg.text)
}
- object Encode_Base64 extends Scala.Fun("encode_base64") {
+ object Encode_Base64 extends Scala.Fun_Bytes("encode_base64") {
val here = Scala_Project.here
- def invoke(args: List[Bytes]): List[Bytes] =
- List(Bytes(Library.the_single(args).base64))
+ def apply(arg: Bytes): Bytes = Bytes(arg.encode_base64)
}
/* XZ compression */
- object Compress extends Scala.Fun("compress") {
+ object Compress extends Scala.Fun_Bytes("compress") {
val here = Scala_Project.here
- def invoke(args: List[Bytes]): List[Bytes] =
- List(Library.the_single(args).compress())
+ def apply(arg: Bytes): Bytes = arg.compress()
}
- object Uncompress extends Scala.Fun("uncompress") {
+ object Uncompress extends Scala.Fun_Bytes("uncompress") {
val here = Scala_Project.here
- def invoke(args: List[Bytes]): List[Bytes] =
- List(Library.the_single(args).uncompress())
+ def apply(arg: Bytes): Bytes = arg.uncompress()
}
@@ -160,16 +156,16 @@
def text: String = UTF8.decode_permissive(this)
- def base64: String = {
+ def encode_base64: String = {
val b =
if (offset == 0 && length == bytes.length) bytes
else Bytes(bytes, offset, length).bytes
Base64.getEncoder.encodeToString(b)
}
- def maybe_base64: (Boolean, String) = {
+ def maybe_encode_base64: (Boolean, String) = {
val s = text
- if (this == Bytes(s)) (false, s) else (true, base64)
+ if (this == Bytes(s)) (false, s) else (true, encode_base64)
}
override def toString: String = "Bytes(" + length + ")"
--- a/src/Pure/General/file.ML Wed Jun 22 14:52:27 2022 +0200
+++ b/src/Pure/General/file.ML Wed Jun 22 17:07:00 2022 +0200
@@ -30,9 +30,7 @@
val input_size: int -> BinIO.instream -> string
val input_all: BinIO.instream -> string
val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
- val fold_pages: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
val read_lines: Path.T -> string list
- val read_pages: Path.T -> string list
val read: Path.T -> string
val write: Path.T -> string -> unit
val append: Path.T -> string -> unit
@@ -143,24 +141,20 @@
. avoid size limit of TextIO.inputAll and overhead of many TextIO.inputLine
. optional terminator at end-of-input
*)
-fun fold_chunks terminator f path a = open_input (fn file =>
+fun fold_lines f path a = open_input (fn file =>
let
fun read buf x =
(case input file of
"" => (case Buffer.content buf of "" => x | line => f line x)
| input =>
- (case String.fields (fn c => c = terminator) input of
+ (case String.fields (fn c => c = #"\n") input of
[rest] => read (Buffer.add rest buf) x
- | line :: more => read_lines more (f (Buffer.content (Buffer.add line buf)) x)))
- and read_lines [rest] x = read (Buffer.add rest Buffer.empty) x
- | read_lines (line :: more) x = read_lines more (f line x);
+ | line :: more => read_more more (f (Buffer.content (Buffer.add line buf)) x)))
+ and read_more [rest] x = read (Buffer.add rest Buffer.empty) x
+ | read_more (line :: more) x = read_more more (f line x);
in read Buffer.empty a end) path;
-fun fold_lines f = fold_chunks #"\n" f;
-fun fold_pages f = fold_chunks #"\f" f;
-
fun read_lines path = rev (fold_lines cons path []);
-fun read_pages path = rev (fold_pages cons path []);
val read = open_input input_all;
--- a/src/Pure/ML/ml_init.ML Wed Jun 22 14:52:27 2022 +0200
+++ b/src/Pure/ML/ml_init.ML Wed Jun 22 17:07:00 2022 +0200
@@ -33,3 +33,9 @@
if n = 1 then String.str (String.sub (s, i))
else String.substring (s, i, n);
end;
+
+structure Substring =
+struct
+ open Substring;
+ val empty = full "";
+end;
--- a/src/Pure/ML/ml_process.scala Wed Jun 22 14:52:27 2022 +0200
+++ b/src/Pure/ML/ml_process.scala Wed Jun 22 17:07:00 2022 +0200
@@ -72,22 +72,20 @@
// options
+ val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
val isabelle_process_options = Isabelle_System.tmp_file("options")
Isabelle_System.chmod("600", File.path(isabelle_process_options))
File.write(isabelle_process_options, YXML.string_of_body(options.encode))
- val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
// session base
+ val (init_session_base, eval_init_session) =
+ session_base match {
+ case None => (sessions_structure.bootstrap, Nil)
+ case Some(base) => (base, List("Resources.init_session_env ()"))
+ }
val init_session = Isabelle_System.tmp_file("init_session")
Isabelle_System.chmod("600", File.path(init_session))
- val eval_init_session =
- session_base match {
- case None => Nil
- case Some(base) =>
- File.write(init_session, new Resources(sessions_structure, base).init_session_yxml)
- List("Resources.init_session_file (Path.explode " +
- ML_Syntax.print_string_bytes(File.path(init_session).implode) + ")")
- }
+ File.write(init_session, new Resources(sessions_structure, init_session_base).init_session_yxml)
// process
val eval_process =
@@ -119,9 +117,9 @@
val bash_env = new HashMap(env)
bash_env.put("ISABELLE_PROCESS_OPTIONS", File.standard_path(isabelle_process_options))
+ bash_env.put("ISABELLE_INIT_SESSION", File.standard_path(init_session))
bash_env.put("ISABELLE_TMP", File.standard_path(isabelle_tmp))
bash_env.put("POLYSTATSDIR", isabelle_tmp.getAbsolutePath)
- bash_env.put("ISABELLE_SCALA_FUNCTIONS", Scala.functions.mkString(","))
Bash.process(
options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
--- a/src/Pure/PIDE/resources.ML Wed Jun 22 14:52:27 2022 +0200
+++ b/src/Pure/PIDE/resources.ML Wed Jun 22 17:07:00 2022 +0200
@@ -13,19 +13,18 @@
bibtex_entries: (string * string list) list,
command_timings: Properties.T list,
load_commands: (string * Position.T) list,
- scala_functions: (string * (bool * Position.T)) list,
+ scala_functions: (string * ((bool * bool) * Position.T)) list,
global_theories: (string * string) list,
loaded_theories: string list} -> unit
val init_session_yxml: string -> unit
- val init_session_file: Path.T -> unit
+ val init_session_env: unit -> unit
val finish_session_base: unit -> unit
val global_theory: string -> string option
val loaded_theory: string -> bool
val check_session: Proof.context -> string * Position.T -> string
val last_timing: Toplevel.transition -> Time.time
val check_load_command: Proof.context -> string * Position.T -> string
- val scala_functions: unit -> string list
- val check_scala_function: Proof.context -> string * Position.T -> string * bool
+ val check_scala_function: Proof.context -> string * Position.T -> string * (bool * bool)
val master_directory: theory -> Path.T
val imports_of: theory -> (string * Position.T) list
val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
@@ -104,7 +103,7 @@
bibtex_entries = Symtab.empty: string list Symtab.table,
timings = empty_timings,
load_commands = []: (string * Position.T) list,
- scala_functions = Symtab.empty: (bool * Position.T) Symtab.table},
+ scala_functions = Symtab.empty: ((bool * bool) * Position.T) Symtab.table},
{global_theories = Symtab.empty: string Symtab.table,
loaded_theories = Symtab.empty: unit Symtab.table});
@@ -137,7 +136,7 @@
(pair (list (pair string string))
(pair (list (pair string (list string))) (pair (list properties)
(pair (list (pair string properties))
- (pair (list (pair string (pair bool properties)))
+ (pair (list (pair string (pair (pair bool bool) properties)))
(pair (list (pair string string)) (list string))))))))
end;
in
@@ -152,8 +151,14 @@
loaded_theories = loaded_theories}
end;
-fun init_session_file path =
- init_session_yxml (File.read path) before File.rm path;
+fun init_session_env () =
+ (case getenv "ISABELLE_INIT_SESSION" of
+ "" => ()
+ | name =>
+ try File.read (Path.explode name)
+ |> Option.app init_session_yxml);
+
+val _ = init_session_env ();
fun finish_session_base () =
Synchronized.change global_session_base
@@ -180,22 +185,13 @@
(* Scala functions *)
-(*raw bootstrap environment*)
-fun scala_functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS");
-
-(*regular resources*)
-fun scala_function a =
- (a, the_default (false, Position.none) (Symtab.lookup (get_session_base1 #scala_functions) a));
-
fun check_scala_function ctxt arg =
let
- val funs = scala_functions () |> sort_strings |> map scala_function;
- val name = Completion.check_entity Markup.scala_functionN (map (apsnd #2) funs) ctxt arg;
- val multi =
- (case AList.lookup (op =) funs name of
- SOME (multi, _) => multi
- | NONE => false);
- in (name, multi) end;
+ val table = get_session_base1 #scala_functions;
+ val funs = Symtab.fold (fn (a, (_, pos)) => cons (a, pos)) table [] |> sort_by #1;
+ val name = Completion.check_entity Markup.scala_functionN funs ctxt arg;
+ val flags = #1 (the (Symtab.lookup table name));
+ in (name, flags) end;
val _ = Theory.setup
(Document_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_function\<close>
@@ -206,8 +202,10 @@
ML_Antiquotation.value_embedded \<^binding>\<open>scala\<close>
(Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, arg) =>
let
- val (name, multi) = check_scala_function ctxt arg;
- val func = if multi then "Scala.function" else "Scala.function1";
+ val (name, (single, bytes)) = check_scala_function ctxt arg;
+ val func =
+ (if single then "Scala.function1" else "Scala.function") ^
+ (if bytes then "_bytes" else "");
in ML_Syntax.atomic (func ^ " " ^ ML_Syntax.print_string name) end)));
--- a/src/Pure/PIDE/resources.scala Wed Jun 22 14:52:27 2022 +0200
+++ b/src/Pure/PIDE/resources.scala Wed Jun 22 17:07:00 2022 +0200
@@ -46,14 +46,14 @@
pair(list(pair(string, list(string))),
pair(list(properties),
pair(list(pair(string, properties)),
- pair(list(pair(string, pair(bool, properties))),
+ pair(list(Scala.encode_fun),
pair(list(pair(string, string)), list(string))))))))(
(sessions_structure.session_positions,
(sessions_structure.dest_session_directories,
(sessions_structure.bibtex_entries,
(command_timings,
(Command_Span.load_commands.map(cmd => (cmd.name, cmd.position)),
- (Scala.functions.map(fun => (fun.name, (fun.multi, fun.position))),
+ (Scala.functions,
(session_base.global_theories.toList,
session_base.loaded_theories.keys)))))))))
}
--- a/src/Pure/System/options.ML Wed Jun 22 14:52:27 2022 +0200
+++ b/src/Pure/System/options.ML Wed Jun 22 17:07:00 2022 +0200
@@ -211,11 +211,8 @@
(case getenv "ISABELLE_PROCESS_OPTIONS" of
"" => ()
| name =>
- let val path = Path.explode name in
- (case try File.read path of
- SOME s => set_default (decode (YXML.parse_body s))
- | NONE => ())
- end);
+ try File.read (Path.explode name)
+ |> Option.app (set_default o decode o YXML.parse_body));
val _ = load_default ();
val _ = ML_Print_Depth.set_print_depth (default_int "ML_print_depth");
--- a/src/Pure/System/scala.scala Wed Jun 22 14:52:27 2022 +0200
+++ b/src/Pure/System/scala.scala Wed Jun 22 17:07:00 2022 +0200
@@ -18,12 +18,16 @@
abstract class Fun(val name: String, val thread: Boolean = false) {
override def toString: String = name
- def multi: Boolean = true
+ def single: Boolean = false
+ def bytes: Boolean = false
def position: Properties.T = here.position
def here: Scala_Project.Here
def invoke(args: List[Bytes]): List[Bytes]
}
+ trait Single_Fun extends Fun { override def single: Boolean = true }
+ trait Bytes_Fun extends Fun { override def bytes: Boolean = true }
+
abstract class Fun_Strings(name: String, thread: Boolean = false)
extends Fun(name, thread = thread) {
override def invoke(args: List[Bytes]): List[Bytes] =
@@ -32,13 +36,25 @@
}
abstract class Fun_String(name: String, thread: Boolean = false)
- extends Fun_Strings(name, thread = thread) {
- override def multi: Boolean = false
+ extends Fun_Strings(name, thread = thread) with Single_Fun {
override def apply(args: List[String]): List[String] =
List(apply(Library.the_single(args)))
def apply(arg: String): String
}
+ abstract class Fun_Bytes(name: String, thread: Boolean = false)
+ extends Fun(name, thread = thread) with Single_Fun with Bytes_Fun {
+ override def invoke(args: List[Bytes]): List[Bytes] =
+ List(apply(Library.the_single(args)))
+ def apply(arg: Bytes): Bytes
+ }
+
+ val encode_fun: XML.Encode.T[Fun] = { fun =>
+ import XML.Encode._
+ pair(string, pair(pair(bool, bool), properties))(
+ fun.name, ((fun.single, fun.bytes), fun.position))
+ }
+
class Functions(val functions: Fun*) extends Isabelle_System.Service
lazy val functions: List[Fun] =
--- a/src/Pure/Tools/server_commands.scala Wed Jun 22 14:52:27 2022 +0200
+++ b/src/Pure/Tools/server_commands.scala Wed Jun 22 17:07:00 2022 +0200
@@ -266,7 +266,7 @@
val matcher = Export.make_matcher(args.export_pattern)
for { entry <- snapshot.exports if matcher(entry.theory_name, entry.name) }
yield {
- val (base64, body) = entry.uncompressed.maybe_base64
+ val (base64, body) = entry.uncompressed.maybe_encode_base64
JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body)
}
}))