--- 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 */