merged
authorwenzelm
Mon, 12 Apr 2021 22:26:30 +0200
changeset 73828 6ab97ac63809
parent 73811 92783562ab78 (current diff)
parent 73827 f86661e32bed (diff)
child 73829 a30a60aef59f
merged
--- a/src/HOL/Tools/ATP/system_on_tptp.ML	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/HOL/Tools/ATP/system_on_tptp.ML	Mon Apr 12 22:26:30 2021 +0200
@@ -8,7 +8,7 @@
 sig
   val get_url: unit -> string
   val list_systems: unit -> {url: string, systems: string list}
-  val run_system_encoded: string -> {output: string, timing: Time.time}
+  val run_system_encoded: string list -> {output: string, timing: Time.time}
   val run_system: {system: string, problem: Path.T, extra: string, timeout: Time.time} ->
     {output: string, timing: Time.time}
 end
@@ -25,15 +25,12 @@
   in {url = url, systems = systems} end
 
 fun run_system_encoded args =
-  cat_strings0 [get_url (), args]
+  (get_url () :: args)
   |> \<^scala>\<open>SystemOnTPTP.run_system\<close>
-  |> split_strings0 |> (fn [output, timing] =>
-    {output = output, timing = Time.fromMilliseconds (Value.parse_int timing)})
+  |> (fn [a, b] => {output = a, timing = Time.fromMilliseconds (Value.parse_int b)})
 
 fun run_system {system, problem, extra, timeout} =
-  cat_strings0
-    [system, Isabelle_System.absolute_path problem,
-      extra, string_of_int (Time.toMilliseconds timeout)]
+  [system, Isabelle_System.absolute_path problem, extra, string_of_int (Time.toMilliseconds timeout)]
   |> run_system_encoded
 
 end
--- a/src/HOL/Tools/ATP/system_on_tptp.scala	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/HOL/Tools/ATP/system_on_tptp.scala	Mon Apr 12 22:26:30 2021 +0200
@@ -40,7 +40,7 @@
         "ListStatus" -> "READY",
         "QuietFlag" -> "-q0"))
 
-  object List_Systems extends Scala.Fun("SystemOnTPTP.list_systems", thread = true)
+  object List_Systems extends Scala.Fun_String("SystemOnTPTP.list_systems", thread = true)
   {
     val here = Scala_Project.here
     def apply(url: String): String = list_systems(Url(url)).text
@@ -69,12 +69,12 @@
     post_request(url, paramaters, timeout = timeout + Time.seconds(15))
   }
 
-  object Run_System extends Scala.Fun("SystemOnTPTP.run_system", thread = true)
+  object Run_System extends Scala.Fun_Strings("SystemOnTPTP.run_system", thread = true)
   {
     val here = Scala_Project.here
-    def apply(arg: String): String =
+    def apply(args: List[String]): List[String] =
     {
-      val List(url, system, problem_path, extra, Value.Int(timeout)) = Library.split_strings0(arg)
+      val List(url, system, problem_path, extra, Value.Int(timeout)) = args
       val problem = File.read(Path.explode(problem_path))
 
       val res = run_system(Url(url), system, problem, extra = extra, timeout = Time.ms(timeout))
@@ -85,7 +85,7 @@
       if (split_lines(text).exists(_.startsWith(bad_prover))) {
         error("The ATP " + quote(system) + " is not available at SystemOnTPTP")
       }
-      else Library.cat_strings0(List(text, timing.toString))
+      else List(text, timing.toString)
     }
   }
 }
--- a/src/HOL/Tools/Nitpick/kodkod.scala	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/HOL/Tools/Nitpick/kodkod.scala	Mon Apr 12 22:26:30 2021 +0200
@@ -154,7 +154,7 @@
 
   /** scala function **/
 
-  object Fun extends Scala.Fun("kodkod", thread = true)
+  object Fun extends Scala.Fun_String("kodkod", thread = true)
   {
     val here = Scala_Project.here
     def apply(args: String): String =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Mon Apr 12 22:26:30 2021 +0200
@@ -16,7 +16,7 @@
   type atp_config =
     {exec : string list * string list,
      arguments : Proof.context -> bool -> string -> Time.time -> Path.T ->
-       term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string,
+       term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string list,
      proof_delims : (string * string) list,
      known_failures : (atp_failure * string) list,
      prem_role : atp_formula_role,
@@ -76,7 +76,7 @@
 type atp_config =
   {exec : string list * string list,
    arguments : Proof.context -> bool -> string -> Time.time -> Path.T ->
-     term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string,
+     term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string list,
    proof_delims : (string * string) list,
    known_failures : (atp_failure * string) list,
    prem_role : atp_formula_role,
@@ -163,7 +163,7 @@
 val agsyhol_config : atp_config =
   {exec = (["AGSYHOL_HOME"], ["agsyHOL"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
-     "--proof --time-out " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem,
+     ["--proof --time-out " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem],
    proof_delims = tstp_proof_delims,
    known_failures = known_szs_status_failures,
    prem_role = Hypothesis,
@@ -181,8 +181,8 @@
 val alt_ergo_config : atp_config =
   {exec = (["WHY3_HOME"], ["why3"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
-     "--format tptp --prover 'Alt-Ergo,0.95.2,' --timelimit " ^ string_of_int (to_secs 1 timeout) ^
-     " " ^ File.bash_path problem,
+     ["--format tptp --prover 'Alt-Ergo,0.95.2,' --timelimit " ^ string_of_int (to_secs 1 timeout) ^
+      " " ^ File.bash_path problem],
    proof_delims = [],
    known_failures =
      [(ProofMissing, ": Valid"),
@@ -271,13 +271,13 @@
   {exec = (["E_HOME"], ["eprover"]),
    arguments = fn ctxt => fn _ => fn heuristic => fn timeout => fn problem =>
      fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
-       "--auto-schedule --tstp-in --tstp-out --silent " ^
-       e_selection_weight_arguments ctxt heuristic sel_weights ^
-       e_term_order_info_arguments gen_weights gen_prec ord_info ^
-       "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^
-       "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
-       " --proof-object=1 " ^
-       File.bash_path problem,
+       ["--auto-schedule --tstp-in --tstp-out --silent " ^
+        e_selection_weight_arguments ctxt heuristic sel_weights ^
+        e_term_order_info_arguments gen_weights gen_prec ord_info ^
+        "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^
+        "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
+        " --proof-object=1 " ^
+        File.bash_path problem],
    proof_delims =
      [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @
      tstp_proof_delims,
@@ -318,9 +318,9 @@
 val iprover_config : atp_config =
   {exec = (["IPROVER_HOME"], ["iproveropt", "iprover"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
-     "--clausifier \"$E_HOME\"/eprover " ^
-     "--clausifier_options \"--tstp-format --silent --cnf\" " ^
-     "--time_out_real " ^ string_of_real (Time.toReal timeout) ^ " " ^ File.bash_path problem,
+     ["--clausifier \"$E_HOME\"/eprover " ^
+      "--clausifier_options \"--tstp-format --silent --cnf\" " ^
+      "--time_out_real " ^ string_of_real (Time.toReal timeout) ^ " " ^ File.bash_path problem],
    proof_delims = tstp_proof_delims,
    known_failures =
      [(ProofIncomplete, "% SZS output start CNFRefutation")] @
@@ -340,11 +340,11 @@
 val leo2_config : atp_config =
   {exec = (["LEO2_HOME"], ["leo.opt", "leo"]),
    arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn problem => fn _ =>
-     "--foatp e --atp e=\"$E_HOME\"/eprover \
-     \--atp epclextract=\"$E_HOME\"/epclextract \
-     \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^
-     (if full_proofs then "--notReplLeibnizEQ --notReplAndrewsEQ --notUseExtCnfCmbd " else "") ^
-     File.bash_path problem,
+     ["--foatp e --atp e=\"$E_HOME\"/eprover \
+      \--atp epclextract=\"$E_HOME\"/epclextract \
+      \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^
+      (if full_proofs then "--notReplLeibnizEQ --notReplAndrewsEQ --notUseExtCnfCmbd " else "") ^
+      File.bash_path problem],
    proof_delims = tstp_proof_delims,
    known_failures =
      [(TimedOut, "CPU time limit exceeded, terminating"),
@@ -366,9 +366,9 @@
 val leo3_config : atp_config =
   {exec = (["LEO3_HOME"], ["leo3"]),
    arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn problem => fn _ =>
-     File.bash_path problem ^ " " ^ "--atp cvc=\"$CVC4_SOLVER\" --atp e=\"$E_HOME\"/eprover \
-     \-p -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^
-     (if full_proofs then "--nleq --naeq " else ""),
+     [File.bash_path problem ^ " " ^ "--atp cvc=\"$CVC4_SOLVER\" --atp e=\"$E_HOME\"/eprover \
+      \-p -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^
+      (if full_proofs then "--nleq --naeq " else "")],
    proof_delims = tstp_proof_delims,
    known_failures = known_szs_status_failures,
    prem_role = Hypothesis,
@@ -387,10 +387,10 @@
 val satallax_config : atp_config =
   {exec = (["SATALLAX_HOME"], ["satallax.opt", "satallax"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
-     (case getenv "E_HOME" of
-       "" => ""
-     | home => "-E " ^ home ^ "/eprover ") ^
-     "-p tstp -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem,
+     [(case getenv "E_HOME" of
+        "" => ""
+      | home => "-E " ^ home ^ "/eprover ") ^
+      "-p tstp -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem],
    proof_delims =
      [("% SZS output start Proof", "% SZS output end Proof")],
    known_failures = known_szs_status_failures,
@@ -419,9 +419,9 @@
   in
     {exec = (["SPASS_HOME"], ["SPASS"]),
      arguments = fn _ => fn full_proofs => fn extra_options => fn timeout => fn problem => fn _ =>
-       "-Isabelle=1 " ^ (if full_proofs then "-CNFRenaming=0 -Splits=0 " else "") ^
-       "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem
-       |> extra_options <> "" ? prefix (extra_options ^ " "),
+       ["-Isabelle=1 " ^ (if full_proofs then "-CNFRenaming=0 -Splits=0 " else "") ^
+        "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem
+        |> extra_options <> "" ? prefix (extra_options ^ " ")],
      proof_delims = [("Here is a proof", "Formulae used in the proof")],
      known_failures =
        [(GaveUp, "SPASS beiseite: Completion found"),
@@ -491,9 +491,9 @@
     {exec = (["VAMPIRE_HOME"], ["vampire"]),
      arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn problem => fn _ =>
        (check_vampire_noncommercial ();
-        vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^
-        " -t " ^ string_of_int (to_secs 1 timeout) ^ " --input_file " ^ File.bash_path problem
-        |> sos = sosN ? prefix "--sos on "),
+        [vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^
+         " -t " ^ string_of_int (to_secs 1 timeout) ^ " --input_file " ^ File.bash_path problem
+         |> sos = sosN ? prefix "--sos on "]),
      proof_delims =
        [("=========== Refutation ==========",
          "======= End of refutation =======")] @
@@ -527,7 +527,7 @@
   in
     {exec = (["Z3_TPTP_HOME"], ["z3_tptp"]),
      arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
-       "-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ File.bash_path problem,
+       ["-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ File.bash_path problem],
      proof_delims = [("SZS status Theorem", "")],
      known_failures = known_szs_status_failures,
      prem_role = Hypothesis,
@@ -556,8 +556,8 @@
   in
     {exec = (["ZIPPERPOSITION_HOME"], ["zipperposition"]),
      arguments = fn _ => fn _ => fn extra_options => fn timeout => fn problem => fn _ =>
-       "--input tptp --output tptp --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem
-       |> extra_options <> "" ? prefix (extra_options ^ " "),
+       ["--input tptp --output tptp --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem
+        |> extra_options <> "" ? prefix (extra_options ^ " ")],
      proof_delims = tstp_proof_delims,
      known_failures = known_szs_status_failures,
      prem_role = Hypothesis,
@@ -615,10 +615,9 @@
 fun remote_config system_name system_versions proof_delims known_failures prem_role best_slice =
   {exec = isabelle_scala_function,
    arguments = fn _ => fn _ => fn command => fn timeout => fn problem => fn _ =>
-    (cat_strings0
      [the_remote_system system_name system_versions,
       Isabelle_System.absolute_path problem,
-      command, string_of_int (Int.min (max_remote_secs, to_secs 1 timeout) * 1000)]),
+      command, string_of_int (Int.min (max_remote_secs, to_secs 1 timeout) * 1000)],
    proof_delims = union (op =) tstp_proof_delims proof_delims,
    known_failures = known_failures @ known_says_failures,
    prem_role = prem_role,
@@ -676,7 +675,7 @@
 
 fun dummy_config prem_role format type_enc uncurried_aliases : atp_config =
   {exec = (["ISABELLE_ATP"], ["scripts/dummy_atp"]),
-   arguments = K (K (K (K (K (K ""))))),
+   arguments = K (K (K (K (K (K []))))),
    proof_delims = [],
    known_failures = known_szs_status_failures,
    prem_role = prem_role,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Apr 12 22:26:30 2021 +0200
@@ -264,7 +264,7 @@
             val ord = effective_term_order ctxt name
             val args =
               arguments ctxt full_proofs extra slice_timeout prob_path (ord, ord_info, sel_weights)
-            val command = File.bash_path executable ^ " " ^ args
+            val command = space_implode " " (File.bash_path executable :: args)
 
             fun run_command () =
               if exec = isabelle_scala_function then
--- a/src/Pure/Admin/build_csdp.scala	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/Admin/build_csdp.scala	Mon Apr 12 22:26:30 2021 +0200
@@ -97,7 +97,7 @@
       /* download source */
 
       val archive_path = tmp_dir + Path.basic(archive_name)
-      Isabelle_System.download(download_url, archive_path, progress = progress)
+      Isabelle_System.download_file(download_url, archive_path, progress = progress)
 
       Isabelle_System.bash("tar xzf " + File.bash_path(archive_path), cwd = tmp_dir.file).check
       val source_name = File.get_dir(tmp_dir)
--- a/src/Pure/Admin/build_e.scala	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/Admin/build_e.scala	Mon Apr 12 22:26:30 2021 +0200
@@ -40,7 +40,7 @@
 
       val archive_url = download_url + "/V_" + version + "/E.tgz"
       val archive_path = tmp_dir + Path.explode("E.tgz")
-      Isabelle_System.download(archive_url, archive_path, progress = progress)
+      Isabelle_System.download_file(archive_url, archive_path, progress = progress)
 
       Isabelle_System.bash("tar xzf " + archive_path, cwd = tmp_dir.file).check
       Isabelle_System.bash("tar xzf " + archive_path + " && mv E src", cwd = component_dir.file).check
--- a/src/Pure/Admin/build_jcef.scala	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/Admin/build_jcef.scala	Mon Apr 12 22:26:30 2021 +0200
@@ -57,7 +57,7 @@
       Isabelle_System.with_tmp_file("archive", ext = "zip")(archive_file =>
       {
         val url = base_url + "/" + Url.encode(version) + "/" + platform.archive
-        Isabelle_System.download(url, archive_file, progress = progress)
+        Isabelle_System.download_file(url, archive_file, progress = progress)
         Isabelle_System.bash("unzip -x " + File.bash_path(archive_file),
             cwd = component_dir.file).check
 
--- a/src/Pure/Admin/build_spass.scala	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/Admin/build_spass.scala	Mon Apr 12 22:26:30 2021 +0200
@@ -66,7 +66,7 @@
       /* download source */
 
       val archive_path = tmp_dir + Path.basic(archive_name)
-      Isabelle_System.download(download_url, archive_path, progress = progress)
+      Isabelle_System.download_file(download_url, archive_path, progress = progress)
 
       Isabelle_System.bash("tar xzf " + archive_path, cwd = tmp_dir.file).check
       Isabelle_System.bash(
--- a/src/Pure/Admin/build_sqlite.scala	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/Admin/build_sqlite.scala	Mon Apr 12 22:26:30 2021 +0200
@@ -53,7 +53,7 @@
     /* jar */
 
     val jar = component_dir + Path.basic(download_name).ext("jar")
-    Isabelle_System.download(download_url, jar, progress = progress)
+    Isabelle_System.download_file(download_url, jar, progress = progress)
 
     Isabelle_System.with_tmp_dir("sqlite")(jar_dir =>
     {
--- a/src/Pure/Admin/build_verit.scala	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/Admin/build_verit.scala	Mon Apr 12 22:26:30 2021 +0200
@@ -60,7 +60,7 @@
       /* download source */
 
       val archive_path = tmp_dir + Path.basic(archive_name)
-      Isabelle_System.download(download_url, archive_path, progress = progress)
+      Isabelle_System.download_file(download_url, archive_path, progress = progress)
 
       Isabelle_System.bash("tar xzf " + File.bash_path(archive_path), cwd = tmp_dir.file).check
       val source_name = File.get_dir(tmp_dir)
--- a/src/Pure/Admin/components.scala	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/Admin/components.scala	Mon Apr 12 22:26:30 2021 +0200
@@ -67,7 +67,7 @@
       val archive = base_dir + Path.explode(archive_name)
       if (!archive.is_file) {
         val remote = Components.default_component_repository + "/" + archive_name
-        Isabelle_System.download(remote, archive, progress = progress)
+        Isabelle_System.download_file(remote, archive, progress = progress)
       }
       for (dir <- copy_dir) {
         Isabelle_System.make_directory(dir)
--- a/src/Pure/General/bytes.scala	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/General/bytes.scala	Mon Apr 12 22:26:30 2021 +0200
@@ -134,8 +134,7 @@
     a
   }
 
-  def text: String =
-    UTF8.decode_chars(s => s, bytes, offset, offset + length).toString
+  def text: String = UTF8.decode_permissive(this)
 
   def base64: String =
   {
--- a/src/Pure/General/output_primitives.ML	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/General/output_primitives.ML	Mon Apr 12 22:26:30 2021 +0200
@@ -29,7 +29,7 @@
   val status_fn: output list -> unit
   val report_fn: output list -> unit
   val result_fn: properties -> output list -> unit
-  type protocol_message_fn = properties -> XML.body -> unit
+  type protocol_message_fn = properties -> XML.body list -> unit
   val protocol_message_fn: protocol_message_fn
   val markup_fn: string * properties -> output * output
 end;
@@ -73,7 +73,7 @@
 val report_fn = ignore_outputs;
 fun result_fn (_: properties) = ignore_outputs;
 
-type protocol_message_fn = properties -> XML.body -> unit;
+type protocol_message_fn = properties -> XML.body list -> unit;
 val protocol_message_fn: protocol_message_fn = fn _ => fn _ => ();
 
 fun markup_fn (_: string * properties) = ("", "");
--- a/src/Pure/General/utf8.scala	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/General/utf8.scala	Mon Apr 12 22:26:30 2021 +0200
@@ -29,7 +29,8 @@
 
   def decode_permissive(text: CharSequence): String =
   {
-    val buf = new java.lang.StringBuilder(text.length)
+    val len = text.length
+    val buf = new java.lang.StringBuilder(len)
     var code = -1
     var rest = 0
     def flush(): Unit =
@@ -57,7 +58,7 @@
         rest -= 1
       }
     }
-    for (i <- 0 until text.length) {
+    for (i <- 0 until len) {
       val c = text.charAt(i)
       if (c < 128) { flush(); buf.append(c) }
       else if ((c & 0xC0) == 0x80) push(c & 0x3F)
@@ -68,23 +69,4 @@
     flush()
     buf.toString
   }
-
-  private class Decode_Chars(decode: String => String,
-    buffer: Array[Byte], start: Int, end: Int) extends CharSequence
-  {
-    def length: Int = end - start
-    def charAt(i: Int): Char = (buffer(start + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
-    def subSequence(i: Int, j: Int): CharSequence =
-      new Decode_Chars(decode, buffer, start + i, start + j)
-
-    // toString with adhoc decoding: abuse of CharSequence interface
-    override def toString: String = decode(decode_permissive(this))
-  }
-
-  def decode_chars(decode: String => String,
-    buffer: Array[Byte], start: Int, end: Int): CharSequence =
-  {
-    require(0 <= start && start <= end && end <= buffer.length, "bad decode range")
-    new Decode_Chars(decode, buffer, start, end)
-  }
 }
--- a/src/Pure/PIDE/byte_message.ML	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/PIDE/byte_message.ML	Mon Apr 12 22:26:30 2021 +0200
@@ -7,12 +7,14 @@
 signature BYTE_MESSAGE =
 sig
   val write: BinIO.outstream -> string list -> unit
+  val write_yxml: BinIO.outstream -> XML.tree -> unit
   val flush: BinIO.outstream -> unit
   val write_line: BinIO.outstream -> string -> unit
   val read: BinIO.instream -> int -> string
   val read_block: BinIO.instream -> int -> string option * int
   val read_line: BinIO.instream -> string option
   val write_message: BinIO.outstream -> string list -> unit
+  val write_message_yxml: BinIO.outstream -> XML.body list -> unit
   val read_message: BinIO.instream -> string list option
   val write_line_message: BinIO.outstream -> string -> unit
   val read_line_message: BinIO.instream -> string option
@@ -25,6 +27,8 @@
 
 fun write stream = List.app (File.output stream);
 
+fun write_yxml stream tree = YXML.traverse (fn s => fn () => File.output stream s) tree ();
+
 fun flush stream = ignore (try BinIO.flushOut stream);
 
 fun write_line stream s = (write stream [s, "\n"]; flush stream);
@@ -61,6 +65,11 @@
 fun write_message stream chunks =
   (write stream (make_header (map size chunks) @ chunks); flush stream);
 
+fun write_message_yxml stream chunks =
+  (write stream (make_header (map YXML.body_size chunks));
+   (List.app o List.app) (write_yxml stream) chunks;
+   flush stream);
+
 fun parse_header line =
   map Value.parse_nat (space_explode "," line)
     handle Fail _ => error ("Malformed message header: " ^ quote line);
--- a/src/Pure/PIDE/command.ML	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/PIDE/command.ML	Mon Apr 12 22:26:30 2021 +0200
@@ -72,9 +72,7 @@
 
     fun read_url () =
       let
-        val text =
-          Isabelle_System.with_tmp_file "file" "" (fn file =>
-            (Isabelle_System.download file_node file; File.read file));
+        val text = Isabelle_System.download file_node;
         val file_pos = Position.file file_node;
       in (text, file_pos) end;
 
--- a/src/Pure/PIDE/markup.scala	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/PIDE/markup.scala	Mon Apr 12 22:26:30 2021 +0200
@@ -727,6 +727,8 @@
 
 sealed case class Markup(name: String, properties: Properties.T)
 {
+  def is_empty: Boolean = name.isEmpty
+
   def markup(s: String): String =
     YXML.string_of_tree(XML.Elem(this, List(XML.Text(s))))
 
--- a/src/Pure/PIDE/protocol.ML	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/PIDE/protocol.ML	Mon Apr 12 22:26:30 2021 +0200
@@ -60,7 +60,7 @@
   end;
 
 fun commands_accepted ids =
-  Output.protocol_message Markup.commands_accepted [XML.Text (space_implode "," ids)];
+  Output.protocol_message Markup.commands_accepted [[XML.Text (space_implode "," ids)]];
 
 val _ =
   Protocol_Command.define "Document.define_command"
@@ -141,12 +141,12 @@
 
             val _ =
               Output.protocol_message Markup.assign_update
-                ((new_id, edited, assign_update) |>
+                [(new_id, edited, assign_update) |>
                   let
                     open XML.Encode;
                     fun encode_upd (a, bs) =
                       string (space_implode "," (map Value.print_int (a :: bs)));
-                  in triple int (list string) (list encode_upd) end);
+                  in triple int (list string) (list encode_upd) end];
           in Document.start_execution state' end)));
 
 val _ =
@@ -157,7 +157,7 @@
           YXML.parse_body versions_yxml |>
             let open XML.Decode in list int end;
         val state1 = Document.remove_versions versions state;
-        val _ = Output.protocol_message Markup.removed_versions [XML.Text (versions_yxml)];
+        val _ = Output.protocol_message Markup.removed_versions [[XML.Text (versions_yxml)]];
       in state1 end));
 
 val _ =
--- a/src/Pure/PIDE/prover.scala	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/PIDE/prover.scala	Mon Apr 12 22:26:30 2021 +0200
@@ -47,17 +47,28 @@
         if (is_status || is_report) message.body.map(_.toString).mkString
         else Pretty.string_of(message.body, metric = Symbol.Metric)
       if (properties.isEmpty)
-        kind.toString + " [[" + res + "]]"
+        kind + " [[" + res + "]]"
       else
-        kind.toString + " " +
+        kind + " " +
           (for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
     }
   }
 
-  class Protocol_Output(props: Properties.T, val bytes: Bytes)
+  class Malformed(msg: String) extends Exn.User_Error("Malformed prover message: " + msg)
+  def bad_header(print: String): Nothing = throw new Malformed("bad message header\n" + print)
+  def bad_chunks(): Nothing = throw new Malformed("bad message chunks")
+
+  def the_chunk(chunks: List[Bytes], print: => String): Bytes =
+    chunks match {
+      case List(chunk) => chunk
+      case _ => throw new Malformed("single chunk expected: " + print)
+    }
+
+  class Protocol_Output(props: Properties.T, val chunks: List[Bytes])
     extends Output(XML.Elem(Markup(Markup.PROTOCOL, props), Nil))
   {
-    lazy val text: String = bytes.text
+    def chunk: Bytes = the_chunk(chunks, toString)
+    lazy val text: String = chunk.text
   }
 }
 
@@ -75,9 +86,9 @@
     receiver(new Prover.Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
   }
 
-  private def protocol_output(props: Properties.T, bytes: Bytes): Unit =
+  private def protocol_output(props: Properties.T, chunks: List[Bytes]): Unit =
   {
-    receiver(new Prover.Protocol_Output(cache.props(props), bytes))
+    receiver(new Prover.Protocol_Output(props, chunks))
   }
 
   private def output(kind: String, props: Properties.T, body: XML.Body): Unit =
@@ -252,90 +263,34 @@
 
   private def message_output(stream: InputStream): Thread =
   {
-    class EOF extends Exception
-    class Protocol_Error(msg: String) extends Exception(msg)
-
-    val name = "message_output"
-    Isabelle_Thread.fork(name = name) {
-      val default_buffer = new Array[Byte](65536)
-      var c = -1
+    def decode_chunk(chunk: Bytes): XML.Body =
+      Symbol.decode_yxml_failsafe(chunk.text, cache = cache)
 
-      def read_int(): Int =
-      //{{{
-      {
-        var n = 0
-        c = stream.read
-        if (c == -1) throw new EOF
-        while (48 <= c && c <= 57) {
-          n = 10 * n + (c - 48)
-          c = stream.read
-        }
-        if (c != 10)
-          throw new Protocol_Error("malformed header: expected integer followed by newline")
-        else n
-      }
-      //}}}
-
-      def read_chunk_bytes(): (Array[Byte], Int) =
-      //{{{
-      {
-        val n = read_int()
-        val buf =
-          if (n <= default_buffer.length) default_buffer
-          else new Array[Byte](n)
-
-        var i = 0
-        var m = 0
-        do {
-          m = stream.read(buf, i, n - i)
-          if (m != -1) i += m
+    val thread_name = "message_output"
+    Isabelle_Thread.fork(name = thread_name) {
+      try {
+        var finished = false
+        while (!finished) {
+          Byte_Message.read_message(stream) match {
+            case None => finished = true
+            case Some(header :: chunks) =>
+              decode_chunk(header) match {
+                case List(XML.Elem(Markup(kind, props), Nil)) =>
+                  if (kind == Markup.PROTOCOL) protocol_output(props, chunks)
+                  else output(kind, props, decode_chunk(Prover.the_chunk(chunks, kind)))
+                case _ => Prover.bad_header(header.toString)
+              }
+            case Some(_) => Prover.bad_chunks()
+          }
         }
-        while (m != -1 && n > i)
-
-        if (i != n)
-          throw new Protocol_Error("bad chunk (unexpected EOF after " + i + " of " + n + " bytes)")
-
-        (buf, n)
-      }
-      //}}}
-
-      def read_chunk(): XML.Body =
-      {
-        val (buf, n) = read_chunk_bytes()
-        YXML.parse_body_failsafe(UTF8.decode_chars(Symbol.decode, buf, 0, n))
-      }
-
-      try {
-        do {
-          try {
-            val header = read_chunk()
-            header match {
-              case List(XML.Elem(Markup(name, props), Nil)) =>
-                val kind = name.intern
-                if (kind == Markup.PROTOCOL) {
-                  val (buf, n) = read_chunk_bytes()
-                  protocol_output(props, Bytes(buf, 0, n))
-                }
-                else {
-                  val body = read_chunk()
-                  output(kind, props, body)
-                }
-              case _ =>
-                read_chunk()
-                throw new Protocol_Error("bad header: " + header.toString)
-            }
-          }
-          catch { case _: EOF => }
-        }
-        while (c != -1)
       }
       catch {
         case e: IOException => system_output("Cannot read message:\n" + e.getMessage)
-        case e: Protocol_Error => system_output("Malformed message:\n" + e.getMessage)
+        case e: Prover.Malformed => system_output(e.getMessage)
       }
       stream.close()
 
-      system_output(name + " terminated")
+      system_output(thread_name + " terminated")
     }
   }
 
--- a/src/Pure/PIDE/resources.ML	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/PIDE/resources.ML	Mon Apr 12 22:26:30 2021 +0200
@@ -13,7 +13,7 @@
      session_chapters: (string * string) list,
      bibtex_entries: (string * string list) list,
      command_timings: Properties.T list,
-     scala_functions: (string * Position.T) list,
+     scala_functions: (string * (bool * Position.T)) list,
      global_theories: (string * string) list,
      loaded_theories: string list} -> unit
   val init_session_yxml: string -> unit
@@ -25,7 +25,7 @@
   val session_chapter: string -> string
   val last_timing: Toplevel.transition -> Time.time
   val scala_functions: unit -> string list
-  val check_scala_function: Proof.context -> string * Position.T -> string
+  val check_scala_function: Proof.context -> string * Position.T -> string * 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 +104,7 @@
     session_chapters = Symtab.empty: string Symtab.table,
     bibtex_entries = Symtab.empty: string list Symtab.table,
     timings = empty_timings,
-    scala_functions = Symtab.empty: Position.T Symtab.table},
+    scala_functions = Symtab.empty: (bool * Position.T) Symtab.table},
    {global_theories = Symtab.empty: string Symtab.table,
     loaded_theories = Symtab.empty: unit Symtab.table});
 
@@ -136,7 +136,7 @@
           (pair (list (pair string properties))
             (pair (list (pair string string)) (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 string)) (list string))))))))
         end;
   in
@@ -146,7 +146,7 @@
        session_chapters = session_chapters,
        bibtex_entries = bibtex_entries,
        command_timings = command_timings,
-       scala_functions = map (apsnd Position.of_properties) scala_functions,
+       scala_functions = (map o apsnd o apsnd) Position.of_properties scala_functions,
        global_theories = global_theories,
        loaded_theories = loaded_theories}
   end;
@@ -184,23 +184,31 @@
 fun scala_functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS");
 
 (*regular resources*)
-fun scala_function_pos name =
-  (name, the_default Position.none (Symtab.lookup (get_session_base1 #scala_functions) name));
+fun scala_function a =
+  (a, the_default (false, Position.none) (Symtab.lookup (get_session_base1 #scala_functions) a));
 
 fun check_scala_function ctxt arg =
-  Completion.check_entity Markup.scala_functionN
-    (scala_functions () |> sort_strings |> map scala_function_pos) 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 _ = Theory.setup
  (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_function\<close>
-    (Scan.lift Parse.embedded_position) check_scala_function #>
+    (Scan.lift Parse.embedded_position) (#1 oo check_scala_function) #>
   ML_Antiquotation.inline_embedded \<^binding>\<open>scala_function\<close>
     (Args.context -- Scan.lift Parse.embedded_position
-      >> (uncurry check_scala_function #> ML_Syntax.print_string)) #>
+      >> (uncurry check_scala_function #> #1 #> ML_Syntax.print_string)) #>
   ML_Antiquotation.value_embedded \<^binding>\<open>scala\<close>
     (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) =>
-      let val name = check_scala_function ctxt arg
-      in ML_Syntax.atomic ("Scala.function " ^ ML_Syntax.print_string name) end)));
+      let
+        val (name, multi) = check_scala_function ctxt arg;
+        val func = if multi then "Scala.function" else "Scala.function1";
+      in ML_Syntax.atomic (func ^ " " ^ ML_Syntax.print_string name) end)));
 
 
 (* manage source files *)
--- a/src/Pure/PIDE/resources.scala	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/PIDE/resources.scala	Mon Apr 12 22:26:30 2021 +0200
@@ -39,14 +39,14 @@
       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, string)), list(string))))))))(
        (sessions_structure.session_positions,
        (sessions_structure.dest_session_directories,
        (sessions_structure.session_chapters,
        (sessions_structure.bibtex_entries,
        (command_timings,
-       (Scala.functions.map(fun => (fun.name, fun.position)),
+       (Scala.functions.map(fun => (fun.name, (fun.multi, fun.position))),
        (session_base.global_theories.toList,
         session_base.loaded_theories.keys)))))))))
   }
--- a/src/Pure/PIDE/session.scala	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/PIDE/session.scala	Mon Apr 12 22:26:30 2021 +0200
@@ -209,7 +209,8 @@
   private case object Stop
   private case class Get_State(promise: Promise[Document.State])
   private case class Cancel_Exec(exec_id: Document_ID.Exec)
-  private case class Protocol_Command(name: String, args: List[String])
+  private case class Protocol_Command_Raw(name: String, args: List[Bytes])
+  private case class Protocol_Command_Args(name: String, args: List[String])
   private case class Update_Options(options: Options)
   private case object Consolidate_Execution
   private case object Prune_History
@@ -506,7 +507,7 @@
               case Protocol.Export(args)
               if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined =>
                 val id = Value.Long.unapply(args.id.get).get
-                val export = Export.make_entry("", args, msg.bytes, cache)
+                val export = Export.make_entry("", args, msg.chunk, cache)
                 change_command(_.add_export(id, (args.serial, export)))
 
               case Protocol.Loading_Theory(node_name, id) =>
@@ -668,7 +669,10 @@
             prover.get.dialog_result(serial, result)
             handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result)))
 
-          case Protocol_Command(name, args) if prover.defined =>
+          case Protocol_Command_Raw(name, args) if prover.defined =>
+            prover.get.protocol_command_raw(name, args)
+
+          case Protocol_Command_Args(name, args) if prover.defined =>
             prover.get.protocol_command_args(name, args)
 
           case change: Session.Change if prover.defined =>
@@ -757,8 +761,14 @@
     }
   }
 
+  def protocol_command_raw(name: String, args: List[Bytes]): Unit =
+    manager.send(Protocol_Command_Raw(name, args))
+
+  def protocol_command_args(name: String, args: List[String]): Unit =
+    manager.send(Protocol_Command_Args(name, args))
+
   def protocol_command(name: String, args: String*): Unit =
-    manager.send(Protocol_Command(name, args.toList))
+    protocol_command_args(name, args.toList)
 
   def cancel_exec(exec_id: Document_ID.Exec): Unit =
     manager.send(Cancel_Exec(exec_id))
--- a/src/Pure/PIDE/yxml.ML	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/PIDE/yxml.ML	Mon Apr 12 22:26:30 2021 +0200
@@ -21,6 +21,8 @@
   val embed_controls: string -> string
   val detect: string -> bool
   val traverse: (string -> 'a -> 'a) -> XML.tree -> 'a -> 'a
+  val tree_size: XML.tree -> int
+  val body_size: XML.body -> int
   val string_of_body: XML.body -> string
   val string_of: XML.tree -> string
   val write_body: Path.T -> XML.body -> unit
@@ -63,18 +65,26 @@
 fun detect s = Char.contains s X_char orelse Char.contains s Y_char;
 
 
-(* output *)
+(* traverse *)
 
 fun traverse string =
   let
     fun attrib (a, x) = string Y #> string a #> string "=" #> string x;
-    fun tree (XML.Elem ((name, atts), ts)) =
-          string XY #> string name #> fold attrib atts #> string X #>
-          fold tree ts #>
-          string XYX
+    fun tree (XML.Elem (markup as (name, atts), ts)) =
+          if Markup.is_empty markup then fold tree ts
+          else
+            string XY #> string name #> fold attrib atts #> string X #>
+            fold tree ts #>
+            string XYX
       | tree (XML.Text s) = string s;
   in tree end;
 
+fun tree_size tree = traverse (Integer.add o size) tree 0;
+fun body_size body = fold (Integer.add o tree_size) body 0;
+
+
+(* output *)
+
 fun string_of_body body = Buffer.empty |> fold (traverse Buffer.add) body |> Buffer.content;
 val string_of = string_of_body o single;
 
--- a/src/Pure/PIDE/yxml.scala	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/PIDE/yxml.scala	Mon Apr 12 22:26:30 2021 +0200
@@ -36,13 +36,16 @@
   {
     def tree(t: XML.Tree): Unit =
       t match {
-        case XML.Elem(Markup(name, atts), ts) =>
-          string(XY_string)
-          string(name)
-          for ((a, x) <- atts) { string(Y_string); string(a); string("="); string(x) }
-          string(X_string)
-          ts.foreach(tree)
-          string(XYX_string)
+        case XML.Elem(markup @ Markup(name, atts), ts) =>
+          if (markup.is_empty) ts.foreach(tree)
+          else {
+            string(XY_string)
+            string(name)
+            for ((a, x) <- atts) { string(Y_string); string(a); string("="); string(x) }
+            string(X_string)
+            ts.foreach(tree)
+            string(XYX_string)
+          }
         case XML.Text(text) => string(text)
       }
     body.foreach(tree)
--- a/src/Pure/ROOT.ML	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/ROOT.ML	Mon Apr 12 22:26:30 2021 +0200
@@ -88,8 +88,8 @@
 ML_file "General/timing.ML";
 ML_file "General/sha1.ML";
 
+ML_file "PIDE/yxml.ML";
 ML_file "PIDE/byte_message.ML";
-ML_file "PIDE/yxml.ML";
 ML_file "PIDE/protocol_message.ML";
 ML_file "PIDE/document_id.ML";
 
--- a/src/Pure/System/bash.scala	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/System/bash.scala	Mon Apr 12 22:26:30 2021 +0200
@@ -206,12 +206,12 @@
 
   /* Scala function */
 
-  object Process extends Scala.Fun("bash_process", thread = true)
+  object Process extends Scala.Fun_Strings("bash_process", thread = true)
   {
     val here = Scala_Project.here
-    def apply(script: String): String =
+    def apply(args: List[String]): List[String] =
     {
-      val result = Exn.capture { Isabelle_System.bash(script) }
+      val result = Exn.capture { Isabelle_System.bash(cat_lines(args)) }
 
       val is_interrupt =
         result match {
@@ -220,15 +220,14 @@
         }
 
       result match {
-        case _ if is_interrupt => ""
-        case Exn.Exn(exn) => Exn.message(exn)
+        case _ if is_interrupt => Nil
+        case Exn.Exn(exn) => List(Exn.message(exn))
         case Exn.Res(res) =>
-          Library.cat_strings0(
-            res.rc.toString ::
-            res.timing.elapsed.ms.toString ::
-            res.timing.cpu.ms.toString ::
-            res.out_lines.length.toString ::
-            res.out_lines ::: res.err_lines)
+          res.rc.toString ::
+          res.timing.elapsed.ms.toString ::
+          res.timing.cpu.ms.toString ::
+          res.out_lines.length.toString ::
+          res.out_lines ::: res.err_lines
       }
     }
   }
--- a/src/Pure/System/isabelle_process.ML	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/System/isabelle_process.ML	Mon Apr 12 22:26:30 2021 +0200
@@ -107,8 +107,8 @@
 
     val msg_channel = Message_Channel.make out_stream;
 
-    fun message name props body =
-      Message_Channel.send msg_channel (Message_Channel.message name props body);
+    fun message name props chunks =
+      Message_Channel.send msg_channel (Message_Channel.message name props chunks);
 
     fun standard_message props name ss =
       if forall (fn s => s = "") ss then ()
@@ -117,7 +117,7 @@
           val pos_props =
             if exists Markup.position_property props then props
             else props @ Position.properties_of (Position.thread_data ());
-        in message name pos_props (XML.blob ss) end;
+        in message name pos_props [XML.blob ss] end;
 
     fun report_message ss =
       if Context_Position.pide_reports ()
@@ -145,9 +145,9 @@
       Unsynchronized.setmp Private_Output.error_message_fn
         (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s) #>
       Unsynchronized.setmp Private_Output.system_message_fn
-        (fn ss => message Markup.systemN [] (XML.blob ss)) #>
+        (fn ss => message Markup.systemN [] [XML.blob ss]) #>
       Unsynchronized.setmp Private_Output.protocol_message_fn
-        (fn props => fn body => message Markup.protocolN props body) #>
+        (fn props => fn chunks => message Markup.protocolN props chunks) #>
       Unsynchronized.setmp print_mode
         ((! print_mode @ #1 modes) |> fold (update op =) (#2 modes));
 
@@ -167,7 +167,7 @@
       in protocol_loop () end;
 
     fun protocol () =
-     (message Markup.initN [] [XML.Text (Session.welcome ())];
+     (message Markup.initN [] [[XML.Text (Session.welcome ())]];
       ml_statistics ();
       protocol_loop ());
 
--- a/src/Pure/System/isabelle_system.ML	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/System/isabelle_system.ML	Mon Apr 12 22:26:30 2021 +0200
@@ -20,7 +20,8 @@
   val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a
   val rm_tree: Path.T -> unit
   val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
-  val download: string -> Path.T -> unit
+  val download: string -> string
+  val download_file: string -> Path.T -> unit
   val isabelle_id: unit -> string
   val isabelle_identifier: unit -> string option
   val isabelle_heading: unit -> string
@@ -35,8 +36,7 @@
 
 fun bash_process script =
   Scala.function "bash_process"
-    ("export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP") ^ "\n" ^ script)
-  |> split_strings0
+    ["export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP"), script]
   |> (fn [] => raise Exn.Interrupt
       | [err] => error err
       | a :: b :: c :: d :: lines =>
@@ -78,8 +78,7 @@
 (* directory and file operations *)
 
 val absolute_path = Path.implode o File.absolute_path;
-fun scala_function0 name = ignore o Scala.function name o cat_strings0;
-fun scala_function name = scala_function0 name o map absolute_path;
+fun scala_function name = ignore o Scala.function name o map absolute_path;
 
 fun make_directory path = (scala_function "make_directory" [path]; path);
 
@@ -88,8 +87,8 @@
 fun copy_file src dst = scala_function "copy_file" [src, dst];
 
 fun copy_file_base (base_dir, src) target_dir =
-  scala_function0 "copy_file_base"
-    [absolute_path base_dir, Path.implode src, absolute_path target_dir];
+  ignore (Scala.function "copy_file_base"
+    [absolute_path base_dir, Path.implode src, absolute_path target_dir]);
 
 
 (* tmp files *)
@@ -117,13 +116,14 @@
 
 (* download file *)
 
-fun download url file =
-  ignore (Scala.function "download" (cat_strings0 [url, absolute_path file]));
+val download = Scala.function1 "download";
+
+fun download_file url path = File.write path (download url);
 
 
 (* Isabelle distribution identification *)
 
-fun isabelle_id () = Scala.function "isabelle_id" "";
+fun isabelle_id () = Scala.function1 "isabelle_id" "";
 
 fun isabelle_identifier () = try getenv_strict "ISABELLE_IDENTIFIER";
 
--- a/src/Pure/System/isabelle_system.scala	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/System/isabelle_system.scala	Mon Apr 12 22:26:30 2021 +0200
@@ -195,7 +195,7 @@
       else error("Failed to identify Isabelle distribution " + root)
     }
 
-  object Isabelle_Id extends Scala.Fun("isabelle_id")
+  object Isabelle_Id extends Scala.Fun_String("isabelle_id")
   {
     val here = Scala_Project.here
     def apply(arg: String): String = isabelle_id()
@@ -227,17 +227,17 @@
 
   /* scala functions */
 
-  private def apply_paths(arg: String, fun: List[Path] => Unit): String =
-    { fun(Library.split_strings0(arg).map(Path.explode)); "" }
+  private def apply_paths(args: List[String], fun: List[Path] => Unit): List[String] =
+    { fun(args.map(Path.explode)); Nil }
 
-  private def apply_paths1(arg: String, fun: Path => Unit): String =
-    apply_paths(arg, { case List(path) => fun(path) })
+  private def apply_paths1(args: List[String], fun: Path => Unit): List[String] =
+    apply_paths(args, { case List(path) => fun(path) })
 
-  private def apply_paths2(arg: String, fun: (Path, Path) => Unit): String =
-    apply_paths(arg, { case List(path1, path2) => fun(path1, path2) })
+  private def apply_paths2(args: List[String], fun: (Path, Path) => Unit): List[String] =
+    apply_paths(args, { case List(path1, path2) => fun(path1, path2) })
 
-  private def apply_paths3(arg: String, fun: (Path, Path, Path) => Unit): String =
-    apply_paths(arg, { case List(path1, path2, path3) => fun(path1, path2, path3) })
+  private def apply_paths3(args: List[String], fun: (Path, Path, Path) => Unit): List[String] =
+    apply_paths(args, { case List(path1, path2, path3) => fun(path1, path2, path3) })
 
 
   /* permissions */
@@ -273,16 +273,16 @@
   }
 
 
-  object Make_Directory extends Scala.Fun("make_directory")
+  object Make_Directory extends Scala.Fun_Strings("make_directory")
   {
     val here = Scala_Project.here
-    def apply(arg: String): String = apply_paths1(arg, make_directory)
+    def apply(args: List[String]): List[String] = apply_paths1(args, make_directory)
   }
 
-  object Copy_Dir extends Scala.Fun("copy_dir")
+  object Copy_Dir extends Scala.Fun_Strings("copy_dir")
   {
     val here = Scala_Project.here
-    def apply(arg: String): String = apply_paths2(arg, copy_dir)
+    def apply(args: List[String]): List[String] = apply_paths2(args, copy_dir)
   }
 
 
@@ -316,16 +316,16 @@
   }
 
 
-  object Copy_File extends Scala.Fun("copy_file")
+  object Copy_File extends Scala.Fun_Strings("copy_file")
   {
     val here = Scala_Project.here
-    def apply(arg: String): String = apply_paths2(arg, copy_file)
+    def apply(args: List[String]): List[String] = apply_paths2(args, copy_file)
   }
 
-  object Copy_File_Base extends Scala.Fun("copy_file_base")
+  object Copy_File_Base extends Scala.Fun_Strings("copy_file_base")
   {
     val here = Scala_Project.here
-    def apply(arg: String): String = apply_paths3(arg, copy_file_base)
+    def apply(args: List[String]): List[String] = apply_paths3(args, copy_file_base)
   }
 
 
@@ -416,10 +416,10 @@
 
   def rm_tree(root: Path): Unit = rm_tree(root.file)
 
-  object Rm_Tree extends Scala.Fun("rm_tree")
+  object Rm_Tree extends Scala.Fun_Strings("rm_tree")
   {
     val here = Scala_Project.here
-    def apply(arg: String): String = apply_paths1(arg, rm_tree)
+    def apply(args: List[String]): List[String] = apply_paths1(args, rm_tree)
   }
 
   def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile =
@@ -594,22 +594,21 @@
 
   /* download file */
 
-  def download(url_name: String, file: Path, progress: Progress = new Progress): Unit =
+  def download(url_name: String, progress: Progress = new Progress): HTTP.Content =
   {
     val url = Url(url_name)
     progress.echo("Getting " + quote(url_name))
-    val content =
-      try { HTTP.Client.get(url) }
-      catch { case ERROR(msg) => cat_error("Failed to download " + quote(url_name), msg) }
-    Bytes.write(file, content.bytes)
+    try { HTTP.Client.get(url) }
+    catch { case ERROR(msg) => cat_error("Failed to download " + quote(url_name), msg) }
   }
 
+  def download_file(url_name: String, file: Path, progress: Progress = new Progress): Unit =
+    Bytes.write(file, download(url_name, progress = progress).bytes)
+
   object Download extends Scala.Fun("download", thread = true)
   {
     val here = Scala_Project.here
-    def apply(arg: String): String =
-      Library.split_strings0(arg) match {
-        case List(url, file) => download(url, Path.explode(file)); ""
-      }
+    override def invoke(args: List[Bytes]): List[Bytes] =
+      args match { case List(url) => List(download(url.text).bytes) }
   }
 }
--- a/src/Pure/System/isabelle_tool.scala	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/System/isabelle_tool.scala	Mon Apr 12 22:26:30 2021 +0200
@@ -134,7 +134,7 @@
   def isabelle_tools(): List[Entry] =
     (external_tools() ::: internal_tools).sortBy(_.name)
 
-  object Isabelle_Tools extends Scala.Fun("isabelle_tools")
+  object Isabelle_Tools extends Scala.Fun_String("isabelle_tools")
   {
     val here = Scala_Project.here
     def apply(arg: String): String =
--- a/src/Pure/System/message_channel.ML	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/System/message_channel.ML	Mon Apr 12 22:26:30 2021 +0200
@@ -7,7 +7,7 @@
 signature MESSAGE_CHANNEL =
 sig
   type message
-  val message: string -> Properties.T -> XML.body -> message
+  val message: string -> Properties.T -> XML.body list -> message
   type T
   val send: T -> message -> unit
   val shutdown: T -> unit
@@ -19,17 +19,13 @@
 
 (* message *)
 
-datatype message = Message of {body: XML.body, flush: bool};
-
-fun body_size body = fold (YXML.traverse (Integer.add o size)) body 0;
+datatype message = Message of XML.body list;
 
-fun chunk body = XML.Text (string_of_int (body_size body) ^ "\n") :: body;
-
-fun message name raw_props body =
+fun message name raw_props chunks =
   let
     val robust_props = map (apply2 YXML.embed_controls) raw_props;
-    val header = XML.Elem ((name, robust_props), []);
-  in Message {body = chunk [header] @ chunk body, flush = name = Markup.protocolN} end;
+    val header = [XML.Elem ((name, robust_props), [])];
+  in Message (header :: chunks) end;
 
 
 (* channel *)
@@ -39,22 +35,14 @@
 fun send (Message_Channel {send, ...}) = send;
 fun shutdown (Message_Channel {shutdown, ...}) = shutdown ();
 
-val flush_timeout = SOME (seconds 0.02);
-
 fun message_output mbox stream =
   let
-    fun continue timeout =
-      (case Mailbox.receive timeout mbox of
-        [] => (Byte_Message.flush stream; continue NONE)
-      | msgs => received timeout msgs)
-    and received _ (NONE :: _) = Byte_Message.flush stream
-      | received _ (SOME (Message {body, flush}) :: rest) =
-          let
-            val _ = fold (YXML.traverse (fn s => fn () => File.output stream s)) body ();
-            val timeout = if flush then (Byte_Message.flush stream; NONE) else flush_timeout;
-          in received timeout rest end
-      | received timeout [] = continue timeout;
-  in fn () => continue NONE end;
+    fun continue () = Mailbox.receive NONE mbox |> received
+    and received [] = continue ()
+      | received (NONE :: _) = ()
+      | received (SOME (Message chunks) :: rest) =
+          (Byte_Message.write_message_yxml stream chunks; received rest);
+  in continue end;
 
 fun make stream =
   let
--- a/src/Pure/System/scala.ML	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/System/scala.ML	Mon Apr 12 22:26:30 2021 +0200
@@ -7,7 +7,8 @@
 signature SCALA =
 sig
   exception Null
-  val function: string -> string -> string
+  val function: string -> string list -> string list
+  val function1: string -> string -> string
 end;
 
 structure Scala: SCALA =
@@ -20,31 +21,31 @@
 val new_id = string_of_int o Counter.make ();
 
 val results =
-  Synchronized.var "Scala.results" (Symtab.empty: string Exn.result Symtab.table);
+  Synchronized.var "Scala.results" (Symtab.empty: string list Exn.result Symtab.table);
 
 val _ =
   Protocol_Command.define "Scala.result"
-    (fn [id, tag, res] =>
+    (fn id :: args =>
       let
         val result =
-          (case tag of
-            "0" => Exn.Exn Null
-          | "1" => Exn.Res res
-          | "2" => Exn.Exn (ERROR res)
-          | "3" => Exn.Exn (Fail res)
-          | "4" => Exn.Exn Exn.Interrupt
-          | _ => raise Fail ("Bad tag: " ^ tag));
+          (case args of
+            ["0"] => Exn.Exn Null
+          | "1" :: rest => Exn.Res rest
+          | ["2", msg] => Exn.Exn (ERROR msg)
+          | ["3", msg] => Exn.Exn (Fail msg)
+          | ["4"] => Exn.Exn Exn.Interrupt
+          | _ => raise Fail "Malformed Scala.result");
       in Synchronized.change results (Symtab.map_entry id (K result)) end);
 
 in
 
-fun function name arg =
+fun function name args =
   Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
     let
       val id = new_id ();
       fun invoke () =
        (Synchronized.change results (Symtab.update (id, Exn.Exn Match));
-        Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg]);
+        Output.protocol_message (Markup.invoke_scala name id) (map (single o XML.Text) args));
       fun cancel () =
        (Synchronized.change results (Symtab.delete_safe id);
         Output.protocol_message (Markup.cancel_scala id) []);
@@ -61,6 +62,8 @@
         handle exn => (if Exn.is_interrupt exn then cancel () else (); Exn.reraise exn)
     end) ();
 
+val function1 = singleton o function;
+
 end;
 
 end;
--- a/src/Pure/System/scala.scala	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/System/scala.scala	Mon Apr 12 22:26:30 2021 +0200
@@ -18,11 +18,28 @@
   /** registered functions **/
 
   abstract class Fun(val name: String, val thread: Boolean = false)
-    extends Function[String, String]
   {
     override def toString: String = name
+    def multi: Boolean = true
     def position: Properties.T = here.position
     def here: Scala_Project.Here
+    def invoke(args: List[Bytes]): List[Bytes]
+  }
+
+  abstract class Fun_Strings(name: String, thread: Boolean = false)
+    extends Fun(name, thread = thread)
+  {
+    override def invoke(args: List[Bytes]): List[Bytes] =
+      apply(args.map(_.text)).map(Bytes.apply)
+    def apply(args: List[String]): List[String]
+  }
+
+  abstract class Fun_String(name: String, thread: Boolean = false)
+    extends Fun_Strings(name, thread = thread)
+  {
+    override def multi: Boolean = false
+    override def apply(args: List[String]): List[String] =
+      List(apply(Library.the_single(args)))
     def apply(arg: String): String
   }
 
@@ -35,13 +52,13 @@
 
   /** demo functions **/
 
-  object Echo extends Fun("echo")
+  object Echo extends Fun_String("echo")
   {
     val here = Scala_Project.here
     def apply(arg: String): String = arg
   }
 
-  object Sleep extends Fun("sleep")
+  object Sleep extends Fun_String("sleep")
   {
     val here = Scala_Project.here
     def apply(seconds: String): String =
@@ -127,7 +144,7 @@
     }
   }
 
-  object Toplevel extends Fun("scala_toplevel")
+  object Toplevel extends Fun_String("scala_toplevel")
   {
     val here = Scala_Project.here
     def apply(arg: String): String =
@@ -162,16 +179,16 @@
       case None => false
     }
 
-  def function_body(name: String, arg: String): (Tag.Value, String) =
+  def function_body(name: String, args: List[Bytes]): (Tag.Value, List[Bytes]) =
     functions.find(fun => fun.name == name) match {
       case Some(fun) =>
-        Exn.capture { fun(arg) } match {
-          case Exn.Res(null) => (Tag.NULL, "")
+        Exn.capture { fun.invoke(args) } match {
+          case Exn.Res(null) => (Tag.NULL, Nil)
           case Exn.Res(res) => (Tag.OK, res)
-          case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, "")
-          case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
+          case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, Nil)
+          case Exn.Exn(e) => (Tag.ERROR, List(Bytes(Exn.message(e))))
         }
-      case None => (Tag.FAIL, "Unknown Isabelle/Scala function: " + quote(name))
+      case None => (Tag.FAIL, List(Bytes("Unknown Isabelle/Scala function: " + quote(name))))
     }
 
 
@@ -191,11 +208,11 @@
       futures = Map.empty
     }
 
-    private def result(id: String, tag: Scala.Tag.Value, res: String): Unit =
+    private def result(id: String, tag: Scala.Tag.Value, res: List[Bytes]): Unit =
       synchronized
       {
         if (futures.isDefinedAt(id)) {
-          session.protocol_command("Scala.result", id, tag.id.toString, res)
+          session.protocol_command_raw("Scala.result", Bytes(id) :: Bytes(tag.id.toString) :: res)
           futures -= id
         }
       }
@@ -203,7 +220,7 @@
     private def cancel(id: String, future: Future[Unit]): Unit =
     {
       future.cancel()
-      result(id, Scala.Tag.INTERRUPT, "")
+      result(id, Scala.Tag.INTERRUPT, Nil)
     }
 
     private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized
@@ -212,7 +229,7 @@
         case Markup.Invoke_Scala(name, id) =>
           def body: Unit =
           {
-            val (tag, res) = Scala.function_body(name, msg.text)
+            val (tag, res) = Scala.function_body(name, msg.chunks)
             result(id, tag, res)
           }
           val future =
--- a/src/Pure/Thy/bibtex.scala	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/Thy/bibtex.scala	Mon Apr 12 22:26:30 2021 +0200
@@ -146,7 +146,7 @@
     })
   }
 
-  object Check_Database extends Scala.Fun("bibtex_check_database")
+  object Check_Database extends Scala.Fun_String("bibtex_check_database")
   {
     val here = Scala_Project.here
     def apply(database: String): String =
--- a/src/Pure/Thy/export.ML	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/Thy/export.ML	Mon Apr 12 22:26:30 2021 +0200
@@ -42,7 +42,7 @@
     name = Path.implode_binding (tap Path.proper_binding binding),
     executable = executable,
     compress = compress,
-    strict = strict} body);
+    strict = strict} [body]);
 
 fun export thy binding body =
   export_params
--- a/src/Pure/Thy/thy_info.ML	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/Thy/thy_info.ML	Mon Apr 12 22:26:30 2021 +0200
@@ -344,7 +344,7 @@
 
     val _ = remove_thy name;
     val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators);
-    val _ = Output.try_protocol_message (Markup.loading_theory name @ text_props) (XML.blob [text]);
+    val _ = Output.try_protocol_message (Markup.loading_theory name @ text_props) [XML.blob [text]];
 
     val _ =
       Position.setmp_thread_data (Position.id_only id) (fn () =>
@@ -360,7 +360,7 @@
 
     val timing_result = Timing.result timing_start;
     val timing_props = [Markup.theory_timing, (Markup.nameN, name)];
-    val _  = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) []
+    val _ = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) []
 
     fun commit () = update_thy deps theory;
   in
--- a/src/Pure/Tools/build.ML	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/Tools/build.ML	Mon Apr 12 22:26:30 2021 +0200
@@ -91,6 +91,7 @@
             (Future.interruptible_task (fn () => (build (); (0, []))) () handle exn =>
               ((1, Runtime.exn_message_list exn) handle _ (*sic!*) => (2, ["CRASHED"])))
           |> let open XML.Encode in pair int (list string) end
+          |> single
           |> Output.protocol_message Markup.build_session_finished)
         end
       | _ => raise Match);
--- a/src/Pure/Tools/build_job.scala	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/Tools/build_job.scala	Mon Apr 12 22:26:30 2021 +0200
@@ -322,7 +322,7 @@
           private def export(msg: Prover.Protocol_Output): Boolean =
             msg.properties match {
               case Protocol.Export(args) =>
-                export_consumer(session_name, args, msg.bytes)
+                export_consumer(session_name, args, msg.chunk)
                 true
               case _ => false
             }
--- a/src/Pure/Tools/debugger.ML	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/Tools/debugger.ML	Mon Apr 12 22:26:30 2021 +0200
@@ -23,7 +23,7 @@
   else
     Output.protocol_message
       (Markup.debugger_output (Isabelle_Thread.get_name ()))
-      [XML.Text (Markup.markup (kind, Markup.serial_properties (serial ())) msg)];
+      [[XML.Text (Markup.markup (kind, Markup.serial_properties (serial ())) msg)]];
 
 val writeln_message = output_message Markup.writelnN;
 val warning_message = output_message Markup.warningN;
@@ -201,12 +201,12 @@
 
 fun debugger_state thread_name =
   Output.protocol_message (Markup.debugger_state thread_name)
-   (get_debugging ()
+   [get_debugging ()
     |> map (fn st =>
       (Position.properties_of
         (Exn_Properties.position_of_polyml_location (PolyML.DebuggerInterface.debugLocation st)),
        PolyML.DebuggerInterface.debugFunction st))
-    |> let open XML.Encode in list (pair properties string) end);
+    |> let open XML.Encode in list (pair properties string) end];
 
 fun debugger_command thread_name =
   (case get_input thread_name of
--- a/src/Pure/Tools/debugger.scala	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/Tools/debugger.scala	Mon Apr 12 22:26:30 2021 +0200
@@ -112,7 +112,7 @@
     {
       msg.properties match {
         case Markup.Debugger_State(thread_name) =>
-          val msg_body = Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.bytes))
+          val msg_body = Symbol.decode_yxml_failsafe(msg.text)
           val debug_states =
           {
             import XML.Decode._
@@ -130,7 +130,7 @@
     {
       msg.properties match {
         case Markup.Debugger_Output(thread_name) =>
-          Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.bytes)) match {
+          Symbol.decode_yxml_failsafe(msg.text) match {
             case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
               val message = XML.Elem(Markup(Markup.message(name), props), body)
               debugger.add_output(thread_name, i -> session.cache.elem(message))
@@ -259,7 +259,7 @@
   }
 
   def input(thread_name: String, msg: String*): Unit =
-    session.protocol_command("Debugger.input", (thread_name :: msg.toList):_*)
+    session.protocol_command_args("Debugger.input", thread_name :: msg.toList)
 
   def continue(thread_name: String): Unit = input(thread_name, "continue")
   def step(thread_name: String): Unit = input(thread_name, "step")
--- a/src/Pure/Tools/doc.scala	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/Tools/doc.scala	Mon Apr 12 22:26:30 2021 +0200
@@ -73,7 +73,7 @@
     examples() ::: release_notes() ::: main_contents
   }
 
-  object Doc_Names extends Scala.Fun("doc_names")
+  object Doc_Names extends Scala.Fun_String("doc_names")
   {
     val here = Scala_Project.here
     def apply(arg: String): String =
--- a/src/Pure/Tools/phabricator.scala	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/Tools/phabricator.scala	Mon Apr 12 22:26:30 2021 +0200
@@ -209,7 +209,7 @@
       val archive =
         if (Url.is_wellformed(mercurial_source)) {
           val archive = tmp_dir + Path.basic("mercurial.tar.gz")
-          Isabelle_System.download(mercurial_source, archive)
+          Isabelle_System.download_file(mercurial_source, archive)
           archive
         }
         else Path.explode(mercurial_source)
--- a/src/Pure/Tools/print_operation.ML	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/Tools/print_operation.ML	Mon Apr 12 22:26:30 2021 +0200
@@ -23,9 +23,9 @@
 
 fun report () =
   Output.try_protocol_message Markup.print_operations
-    (Synchronized.value print_operations
+    [Synchronized.value print_operations
       |> map (fn (x, (y, _)) => (x, y)) |> rev
-      |> let open XML.Encode in list (pair string string) end);
+      |> let open XML.Encode in list (pair string string) end];
 
 val _ = Protocol_Command.define "print_operations" (fn [] => report ());
 
--- a/src/Pure/library.ML	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/library.ML	Mon Apr 12 22:26:30 2021 +0200
@@ -143,8 +143,6 @@
   val cat_lines: string list -> string
   val space_explode: string -> string -> string list
   val split_lines: string -> string list
-  val cat_strings0: string list -> string
-  val split_strings0: string -> string list
   val plain_words: string -> string
   val prefix_lines: string -> string -> string
   val prefix: string -> string -> string
@@ -741,9 +739,6 @@
 
 val split_lines = space_explode "\n";
 
-val cat_strings0 = space_implode "\000";
-val split_strings0 = space_explode "\000";
-
 fun plain_words s = space_explode "_" s |> space_implode " ";
 
 fun prefix_lines "" txt = txt
--- a/src/Pure/library.scala	Sun Apr 11 07:35:24 2021 +0000
+++ b/src/Pure/library.scala	Mon Apr 12 22:26:30 2021 +0200
@@ -275,6 +275,12 @@
       res.toList
     }
 
+  def the_single[A](xs: List[A]): A =
+    xs match {
+      case List(x) => x
+      case _ => error("Single argument expected")
+    }
+
 
   /* proper values */