# HG changeset patch # User wenzelm # Date 1655910420 -7200 # Node ID e6e0a95f87f3072eac5cc879ee5a2d7387d4871a # Parent a789c5732f7a96623d62806718276bf8a7ed4794# Parent 7ff9745609d7cf03d33de6cd68ee9f34982be9ec merged diff -r a789c5732f7a -r e6e0a95f87f3 src/Pure/General/bytes.ML --- 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)); diff -r a789c5732f7a -r e6e0a95f87f3 src/Pure/General/bytes.scala --- 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 + ")" diff -r a789c5732f7a -r e6e0a95f87f3 src/Pure/General/file.ML --- 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; diff -r a789c5732f7a -r e6e0a95f87f3 src/Pure/ML/ml_init.ML --- 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; diff -r a789c5732f7a -r e6e0a95f87f3 src/Pure/ML/ml_process.scala --- 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 """ + diff -r a789c5732f7a -r e6e0a95f87f3 src/Pure/PIDE/resources.ML --- 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>\scala_function\ @@ -206,8 +202,10 @@ ML_Antiquotation.value_embedded \<^binding>\scala\ (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))); diff -r a789c5732f7a -r e6e0a95f87f3 src/Pure/PIDE/resources.scala --- 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))))))))) } diff -r a789c5732f7a -r e6e0a95f87f3 src/Pure/System/options.ML --- 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"); diff -r a789c5732f7a -r e6e0a95f87f3 src/Pure/System/scala.scala --- 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] = diff -r a789c5732f7a -r e6e0a95f87f3 src/Pure/Tools/server_commands.scala --- 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) } }))