--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Fri Sep 20 14:28:13 2024 +0200
@@ -283,7 +283,7 @@
val n = dim v
val strs =
map (decimalize 20 o (fn i => FuncUtil.Intfunc.tryapplyd (snd v) i @0)) (1 upto n)
- in space_implode " " strs ^ "\n" end;
+ in implode_space strs ^ "\n" end;
fun triple_int_ord ((a, b, c), (a', b', c')) =
prod_ord int_ord (prod_ord int_ord int_ord) ((a, (b, c)), (a', (b', c')));
@@ -559,7 +559,7 @@
in
string_of_int m ^ "\n" ^
string_of_int nblocks ^ "\n" ^
- (space_implode " " (map string_of_int blocksizes)) ^
+ (implode_space (map string_of_int blocksizes)) ^
"\n" ^
sdpa_of_vector obj ^
fold_rev (fn (k, m) => fn a => sdpa_of_blockdiagonal (k - 1) m ^ a)
--- a/src/HOL/SPARK/Tools/fdl_parser.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/SPARK/Tools/fdl_parser.ML Fri Sep 20 14:28:13 2024 +0200
@@ -64,7 +64,7 @@
fun beginning n cs =
let val dots = if length cs > n then " ..." else "";
in
- space_implode " " (take n cs) ^ dots
+ implode_space (take n cs) ^ dots
end;
fun !!! scan =
--- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML Fri Sep 20 14:28:13 2024 +0200
@@ -411,7 +411,7 @@
case x of
Term_FuncG (symbol, tptp_type_list, tptp_term_list) =>
"(" ^ string_of_symbol symbol ^ " " ^
- space_implode " " (map string_of_tptp_type tptp_type_list
+ implode_space (map string_of_tptp_type tptp_type_list
@ map string_of_tptp_term tptp_term_list) ^ ")"
| Term_Var str => str
| Term_Conditional (tptp_formula, tptp_term1, tptp_term2) => "" (*FIXME*)
@@ -496,11 +496,11 @@
and string_of_tptp_formula (Pred (symbol, tptp_term_list)) =
"(" ^ string_of_symbol symbol ^
- space_implode " " (map string_of_tptp_term tptp_term_list) ^ ")"
+ implode_space (map string_of_tptp_term tptp_term_list) ^ ")"
| string_of_tptp_formula (Fmla (symbol, tptp_formula_list)) =
"(" ^
string_of_symbol symbol ^
- space_implode " " (map string_of_tptp_formula tptp_formula_list) ^ ")"
+ implode_space (map string_of_tptp_formula tptp_formula_list) ^ ")"
| string_of_tptp_formula (Sequent (tptp_formula_list1, tptp_formula_list2)) = "" (*FIXME*)
| string_of_tptp_formula (Quant (quantifier, varlist, tptp_formula)) =
string_of_quantifier quantifier ^ "[" ^
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Fri Sep 20 14:28:13 2024 +0200
@@ -664,7 +664,7 @@
|> (fn l =>
if null l then ""
else
- space_implode " " l
+ implode_space l
|> pair " "
|> (op ^))
--- a/src/HOL/TPTP/atp_theory_export.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Fri Sep 20 14:28:13 2024 +0200
@@ -56,7 +56,7 @@
|> File.write_list prob_file
val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec)
val command =
- space_implode " " (File.bash_path (Path.explode path) ::
+ implode_space (File.bash_path (Path.explode path) ::
arguments false false "" atp_timeout prob_file)
val outcome =
Timeout.apply atp_timeout Isabelle_System.bash_output command
--- a/src/HOL/TPTP/mash_eval.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Fri Sep 20 14:28:13 2024 +0200
@@ -70,7 +70,7 @@
(used_facts |> map (with_index facts o fst)
|> sort (int_ord o apply2 fst)
|> map index_str
- |> space_implode " ") ^
+ |> implode_space) ^
(if length facts < the max_facts then
" (of " ^ string_of_int (length facts) ^ ")"
else
@@ -79,7 +79,7 @@
"Failure: " ^
(facts |> take (the max_facts) |> tag_list 1
|> map index_str
- |> space_implode " "))
+ |> implode_space))
end
fun solve_goal (j, lines) =
--- a/src/HOL/TPTP/mash_export.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/TPTP/mash_export.ML Fri Sep 20 14:28:13 2024 +0200
@@ -43,7 +43,7 @@
fun encode_feature (names, weight) =
encode_str names ^ (if Real.== (weight, 1.0) then "" else "=" ^ Real.toString weight)
-val encode_features = map encode_feature #> space_implode " "
+val encode_features = map encode_feature #> implode_space
(* The suggested weights do not make much sense. *)
fun extract_suggestion sugg =
--- a/src/HOL/Tools/ATP/atp_proof.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Fri Sep 20 14:28:13 2024 +0200
@@ -162,7 +162,7 @@
""
fun from_lemmas [] = ""
- | from_lemmas ss = " from " ^ space_implode " " (Try.serial_commas "and" (map quote ss))
+ | from_lemmas ss = " from " ^ implode_space (Try.serial_commas "and" (map quote ss))
fun string_of_atp_failure MaybeUnprovable = "Problem maybe unprovable"
| string_of_atp_failure Unprovable = "Problem unprovable"
--- a/src/HOL/Tools/Argo/argo_tactic.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Tools/Argo/argo_tactic.ML Fri Sep 20 14:28:13 2024 +0200
@@ -634,7 +634,7 @@
val id = Argo_Proof.string_of_proof_id proof_id
val ids = map (Argo_Proof.string_of_proof_id o Argo_Proof.id_of) proofs
val rule_string = Argo_Proof.string_of_rule rule
- in full_tracing ctxt' (" " ^ id ^ " <- " ^ space_implode " " ids ^ " . " ^ rule_string) end)
+ in full_tracing ctxt' (" " ^ id ^ " <- " ^ implode_space ids ^ " . " ^ rule_string) end)
fun replay_bottom_up (env as (ctxt, _, _)) proof thm_cache =
let
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Sep 20 14:28:13 2024 +0200
@@ -322,7 +322,7 @@
| replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
fun path_finder_fail tm ps t =
raise METIS_RECONSTRUCT ("equality_inference (path_finder)",
- "path = " ^ space_implode " " (map string_of_int ps) ^
+ "path = " ^ implode_space (map string_of_int ps) ^
" isa-term: " ^ Syntax.string_of_term ctxt tm ^
(case t of
SOME t => " fol-term: " ^ Metis_Term.toString t
--- a/src/HOL/Tools/Nitpick/nitpick.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Sep 20 14:28:13 2024 +0200
@@ -669,7 +669,7 @@
options
in
print ("Try again with " ^
- space_implode " " (serial_commas "and" ss) ^
+ implode_space (serial_commas "and" ss) ^
" to confirm that the " ^ das_wort_model ^
" is genuine")
end
--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML Fri Sep 20 14:28:13 2024 +0200
@@ -291,7 +291,7 @@
extract_params (Proof_Context.init_global thy) Normal (default_raw_params thy)
o map (apsnd single)
-val parse_key = Scan.repeat1 Parse.embedded >> space_implode " "
+val parse_key = Scan.repeat1 Parse.embedded >> implode_space
val parse_value =
Scan.repeats1 (Parse.minus >> single
|| Scan.repeat1 (Scan.unless Parse.minus
--- a/src/HOL/Tools/Nunchaku/nunchaku_commands.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_commands.ML Fri Sep 20 14:28:13 2024 +0200
@@ -235,7 +235,7 @@
extract_params (Proof_Context.init_global thy) Normal (default_raw_params thy)
o map (apsnd single);
-val parse_key = Scan.repeat1 Parse.embedded >> space_implode " ";
+val parse_key = Scan.repeat1 Parse.embedded >> implode_space;
val parse_value =
Scan.repeat1 (Parse.minus >> single
|| Scan.repeat1 (Scan.unless Parse.minus (Parse.name || Parse.float_number))
--- a/src/HOL/Tools/Nunchaku/nunchaku_display.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_display.ML Fri Sep 20 14:28:13 2024 +0200
@@ -23,7 +23,7 @@
val pretty_indent = Pretty.indent indent_size;
fun sorting_str_of_typ (TFree (s, _)) = "a" ^ s
- | sorting_str_of_typ (Type (s, Ts)) = "b" ^ s ^ space_implode " " (map sorting_str_of_typ Ts)
+ | sorting_str_of_typ (Type (s, Ts)) = "b" ^ s ^ implode_space (map sorting_str_of_typ Ts)
| sorting_str_of_typ (TVar _) = "X";
fun sorting_str_of_term (Const (s, T)) = "b" ^ s ^ sorting_str_of_typ T
--- a/src/HOL/Tools/Nunchaku/nunchaku_problem.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_problem.ML Fri Sep 20 14:28:13 2024 +0200
@@ -660,7 +660,7 @@
| (NConst (id, _, _), NAbs _) =>
if is_nun_const_quantifier id then
let val (vars, body) = strip_nun_binders id app in
- id ^ " " ^ space_implode " " (map (nun_parens o str_of_tmty) vars) ^ nun_dot ^ " " ^
+ id ^ " " ^ implode_space (map (nun_parens o str_of_tmty) vars) ^ nun_dot ^ " " ^
str_of NONE body
end
else
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Sep 20 14:28:13 2024 +0200
@@ -257,7 +257,7 @@
val executable = in_path + Path.basic "isabelle_quickcheck_narrowing"
val cmd =
"exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^ ghc_options ^ " " ^
- (space_implode " "
+ (implode_space
(map File.bash_platform_path
(map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^
" -o " ^ File.bash_platform_path executable ^ ";"
--- a/src/HOL/Tools/Quotient/quotient_term.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Fri Sep 20 14:28:13 2024 +0200
@@ -116,7 +116,7 @@
val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
val ty_str = Syntax.string_of_typ ctxt ty
in
- raise LIFT_MATCH (space_implode " "
+ raise LIFT_MATCH (implode_space
["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
end
@@ -283,7 +283,7 @@
val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
val ty_str = Syntax.string_of_typ ctxt ty
in
- raise LIFT_MATCH (space_implode " "
+ raise LIFT_MATCH (implode_space
["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
end
@@ -689,7 +689,7 @@
val rtrm_str = Syntax.string_of_term ctxt rtrm
val qtrm_str = Syntax.string_of_term ctxt qtrm
in
- raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str])
+ raise LIFT_MATCH (implode_space [msg, quote rtrm_str, "and", quote qtrm_str])
end
--- a/src/HOL/Tools/SMT/smt_config.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Tools/SMT/smt_config.ML Fri Sep 20 14:28:13 2024 +0200
@@ -279,7 +279,7 @@
in
Pretty.writeln (Pretty.big_list "SMT setup:" [
Pretty.str ("Current SMT solver: " ^ n),
- Pretty.str ("Current SMT solver options: " ^ space_implode " " opts),
+ Pretty.str ("Current SMT solver options: " ^ implode_space opts),
Pretty.str_list "Available SMT solvers: " "" ns,
Pretty.str ("Current timeout: " ^ t ^ " seconds"),
Pretty.str ("With proofs: " ^
--- a/src/HOL/Tools/SMT/smt_solver.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML Fri Sep 20 14:28:13 2024 +0200
@@ -139,7 +139,7 @@
fun invoke name command options smt_options ithms ctxt =
let
val options = options @ SMT_Config.solver_options_of ctxt
- val comments = [space_implode " " options]
+ val comments = [implode_space options]
val (str, replay_data as {context = ctxt', ...}) =
ithms
--- a/src/HOL/Tools/SMT/smt_translate.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML Fri Sep 20 14:28:13 2024 +0200
@@ -440,7 +440,7 @@
SOME (n, []) => pair n
| SOME (n, Ts) =>
fold_map transT Ts
- #>> (fn ns => enclose "(" ")" (space_implode " " (n :: ns)))
+ #>> (fn ns => enclose "(" ")" (implode_space (n :: ns)))
| NONE => add_typ T true)
fun trans t =
--- a/src/HOL/Tools/SMT/smtlib_interface.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML Fri Sep 20 14:28:13 2024 +0200
@@ -131,10 +131,10 @@
fun sctrarg (sel, typ) = "(" ^ sel ^ " " ^ typ ^ ")"
-fun sctr (name, args) = enclose "(" ")" (space_implode " " (name :: map sctrarg args))
-fun sdatatype (name, ctrs) = enclose "(" ")" (space_implode " " (name :: map sctr ctrs))
+fun sctr (name, args) = enclose "(" ")" (implode_space (name :: map sctrarg args))
+fun sdatatype (name, ctrs) = enclose "(" ")" (implode_space (name :: map sctr ctrs))
-fun string_of_fun (f, (ss, s)) = f ^ " (" ^ space_implode " " ss ^ ") " ^ s
+fun string_of_fun (f, (ss, s)) = f ^ " (" ^ implode_space ss ^ ") " ^ s
fun named_sterm s t = SMTLIB.S [SMTLIB.Sym "!", t, SMTLIB.Key "named", SMTLIB.Sym s]
--- a/src/HOL/Tools/SMT/z3_proof.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Tools/SMT/z3_proof.ML Fri Sep 20 14:28:13 2024 +0200
@@ -125,7 +125,7 @@
enclose "{" "}" (commas
[string_of_int id,
string_of_rule rule,
- enclose "[" "]" (space_implode " " bounds),
+ enclose "[" "]" (implode_space bounds),
Syntax.string_of_term ctxt concl] ^
cat_lines (map (prefix "\n" o str (depth + 1)) prems))
in str 0 end
--- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Fri Sep 20 14:28:13 2024 +0200
@@ -19,7 +19,7 @@
struct
fun implode_message (workers, work) =
- space_implode " " (Try.serial_commas "and" workers) ^ work
+ implode_space (Try.serial_commas "and" workers) ^ work
structure Thread_Heap = Heap
(
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Sep 20 14:28:13 2024 +0200
@@ -262,7 +262,7 @@
| facts => "The goal is falsified by these facts: " ^ commas facts)
else
"Derived \"False\" from these facts alone: " ^
- space_implode " " (map fst used_facts)))
+ implode_space (map fst used_facts)))
fun check_expected_outcome ctxt prover_name expect outcome =
let
@@ -351,7 +351,7 @@
fun string_of_facts filter facts =
"Selected " ^ string_of_int (length facts) ^ " " ^ (if filter = "" then "" else filter ^ " ") ^
- "fact" ^ plural_s (length facts) ^ ": " ^ (space_implode " " (map (fst o fst) facts))
+ "fact" ^ plural_s (length facts) ^ ": " ^ (implode_space (map (fst o fst) facts))
fun string_of_factss factss =
if forall (null o snd) factss then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Sep 20 14:28:13 2024 +0200
@@ -154,7 +154,7 @@
(* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are
read correctly. *)
-val implode_param = strip_spaces_except_between_idents o space_implode " "
+val implode_param = strip_spaces_except_between_idents o implode_space
(* FIXME: use "Generic_Data" *)
structure Data = Theory_Data
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri Sep 20 14:28:13 2024 +0200
@@ -412,7 +412,7 @@
ctxt |> perhaps (try (Proof_Context.augment term)))
fun using_facts [] [] = ""
- | using_facts ls ss = enclose "using " " " (space_implode " " (map string_of_label ls @ ss))
+ | using_facts ls ss = enclose "using " " " (implode_space (map string_of_label ls @ ss))
(* Local facts are always passed via "using", which affects "meson" and "metis". This is
arguably stylistically superior, because it emphasises the structure of the proof. It is also
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Sep 20 14:28:13 2024 +0200
@@ -512,7 +512,7 @@
|> map fst
in
(trace_msg ctxt (fn () => "MaSh query internal " ^ commas (map fst goal_feats) ^ " from {" ^
- elide_string 1000 (space_implode " " (Vector.foldr (op ::) [] fact_names)) ^ "}");
+ elide_string 1000 (implode_space (Vector.foldr (op ::) [] fact_names)) ^ "}");
(case algorithm of
MaSh_NB => nb ()
| MaSh_kNN => knn ()
@@ -545,7 +545,7 @@
| unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
val encode_str = String.translate meta_char
-val encode_strs = map encode_str #> space_implode " "
+val encode_strs = map encode_str #> implode_space
fun decode_str s =
if String.isSubstring "%" s then unmeta_chars [] (String.explode s) else s;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Fri Sep 20 14:28:13 2024 +0200
@@ -145,7 +145,7 @@
| Algebra_Method => "algebra"
| Order_Method => "order")
in
- maybe_paren (space_implode " " (meth_s :: merge_indexed_facts ss))
+ maybe_paren (implode_space (meth_s :: merge_indexed_facts ss))
end
fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
@@ -211,7 +211,7 @@
if is_proof_method_direct meth then ([], extras) else (extras, [])
in
(if null indirect_ss then ""
- else "using " ^ space_implode " " (merge_indexed_facts indirect_ss) ^ " ") ^
+ else "using " ^ implode_space (merge_indexed_facts indirect_ss) ^ " ") ^
apply_on_subgoal i n ^ string_of_proof_method direct_ss meth ^
(if is_proof_method_multi_goal meth andalso n <> 1 then "[1]" else "")
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Sep 20 14:28:13 2024 +0200
@@ -204,7 +204,7 @@
string_of_int (Time.toMilliseconds elapsed) ^ " ms"))
val args = arguments abduce full_proofs extra run_timeout prob_path
- val command = space_implode " " (File.bash_path executable :: args)
+ val command = implode_space (File.bash_path executable :: args)
fun run_command () =
if exec = isabelle_scala_function then
@@ -290,7 +290,7 @@
if mode = Normal andalso not (is_conjecture_used_in_proof atp_proof)
andalso not (Logic.get_goal (Thm.prop_of goal) subgoal aconv @{prop False}) then
warning ("Derived \"False\" from these facts alone: " ^
- space_implode " " (map fst used_facts))
+ implode_space (map fst used_facts))
else
()
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Sep 20 14:28:13 2024 +0200
@@ -75,7 +75,7 @@
fun n_facts names =
let val n = length names in
string_of_int n ^ " fact" ^ plural_s n ^
- (if n > 0 then ": " ^ (names |> map fst |> sort string_ord |> space_implode " ") else "")
+ (if n > 0 then ": " ^ (names |> map fst |> sort string_ord |> implode_space) else "")
end
fun print silent f = if silent then () else writeln (f ())
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Sep 20 14:28:13 2024 +0200
@@ -51,7 +51,7 @@
handle Option.Option =>
let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
error ("Parameter " ^ quote name ^ " must be assigned " ^
- space_implode " " (serial_commas "or" ss))
+ implode_space (serial_commas "or" ss))
end
val has_junk =
--- a/src/HOL/Tools/try0.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Tools/try0.ML Fri Sep 20 14:28:13 2024 +0200
@@ -55,7 +55,7 @@
fun add_attr_text (NONE, _) s = s
| add_attr_text (_, []) s = s
| add_attr_text (SOME x, fs) s =
- s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ space_implode " " fs;
+ s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ implode_space fs;
fun attrs_text (sx, ix, ex, dx) (ss, is, es, ds) =
"" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es), (dx, ds)];
@@ -131,7 +131,7 @@
else Par_List.get_some try_method #> the_list;
in
if mode = Normal then
- "Trying " ^ space_implode " " (Try.serial_commas "and" (map (quote o fst) named_methods)) ^
+ "Trying " ^ implode_space (Try.serial_commas "and" (map (quote o fst) named_methods)) ^
"..."
|> writeln
else
--- a/src/HOL/ex/Sketch_and_Explore.thy Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/ex/Sketch_and_Explore.thy Fri Sep 20 14:28:13 2024 +0200
@@ -91,12 +91,12 @@
val prefix = Symbol.spaces indent;
val fixes_s =
if not is_for orelse null fixes then NONE
- else SOME ("for " ^ space_implode " "
+ else SOME ("for " ^ implode_space
(map (fn (v, _) => Thy_Header.print_name' ctxt' v) fixes));
val premises_s = if is_prems then SOME "premises prems" else NONE;
val sh_s = if is_sh then SOME "sledgehammer" else NONE;
val subgoal_s = map_filter I [SOME "subgoal", premises_s, fixes_s]
- |> space_implode " ";
+ |> implode_space;
val using_s = if is_prems then SOME "using prems" else NONE;
val s = cat_lines (
[subgoal_s]
--- a/src/Pure/General/graph_display.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/Pure/General/graph_display.ML Fri Sep 20 14:28:13 2024 +0200
@@ -85,7 +85,7 @@
sort_graph
#> map (fn ((key, Node {name, unfold, content = _, directory, path}), parents) =>
"\"" ^ name ^ "\" \"" ^ key ^ "\" \"" ^ directory ^ (if unfold then "\" + \"" else "\" \"") ^
- path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;")
+ path ^ "\" > " ^ implode_space (map quote parents) ^ " ;")
#> cat_lines;
in
--- a/src/Pure/Isar/locale.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/Pure/Isar/locale.ML Fri Sep 20 14:28:13 2024 +0200
@@ -597,7 +597,7 @@
NONE =>
error ("No interpretation of locale " ^ quote (markup_name ctxt name) ^
" with\nparameter instantiation " ^
- space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
+ implode_space (map (quote o Syntax.string_of_term_global thy) base) ^
" available")
| SOME {serial = serial', ...} => serial');
in
--- a/src/Pure/Isar/obtain.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/Pure/Isar/obtain.ML Fri Sep 20 14:28:13 2024 +0200
@@ -47,7 +47,7 @@
if member (op =) vs v then insert (op aconv) t else I | _ => I) tm [];
val _ = null bads orelse
error ("Result contains obtained parameters: " ^
- space_implode " " (map (Syntax.string_of_term ctxt) bads));
+ implode_space (map (Syntax.string_of_term ctxt) bads));
in tm end;
fun eliminate ctxt rule xs As thm =
--- a/src/Pure/Isar/proof_context.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/Pure/Isar/proof_context.ML Fri Sep 20 14:28:13 2024 +0200
@@ -1564,7 +1564,7 @@
fun print_case name xs =
(case trim_names xs of
[] => print_name name
- | xs' => enclose "(" ")" (space_implode " " (map print_name (name :: xs'))));
+ | xs' => enclose "(" ")" (implode_space (map print_name (name :: xs'))));
fun is_case x t =
x = Rule_Cases.case_conclN andalso not (Term.exists_subterm Term.is_Var t);
--- a/src/Pure/Isar/token.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/Pure/Isar/token.ML Fri Sep 20 14:28:13 2024 +0200
@@ -833,7 +833,7 @@
val (markup, xname) = print ctxt';
in plain_words kind ^ " " ^ quote (Markup.markup markup xname) end);
val print_args =
- if null args2 then "" else ":\n " ^ space_implode " " (map print args2);
+ if null args2 then "" else ":\n " ^ implode_space (map print args2);
in
error ("Bad arguments for " ^ print_name ^ Position.here pos ^ print_args ^
Markup.markup_report (implode (reported_text ())))
--- a/src/Pure/ML/ml_syntax.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/Pure/ML/ml_syntax.ML Fri Sep 20 14:28:13 2024 +0200
@@ -98,7 +98,7 @@
fun print_position pos =
let val {line, offset, end_offset, props = {label, file, id}} = Position.dest pos in
- space_implode " "
+ implode_space
["Position.make0", print_int line, print_int offset, print_int end_offset,
print_string label, print_string file, print_string id]
end;
--- a/src/Pure/PIDE/xml.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/Pure/PIDE/xml.ML Fri Sep 20 14:28:13 2024 +0200
@@ -132,7 +132,7 @@
(* elements *)
fun elem name atts =
- space_implode " " (name :: map (fn (a, x) => a ^ "=\"" ^ text x ^ "\"") atts);
+ implode_space (name :: map (fn (a, x) => a ^ "=\"" ^ text x ^ "\"") atts);
fun element name atts body =
let val b = implode body in
--- a/src/Pure/System/bash.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/Pure/System/bash.ML Fri Sep 20 14:28:13 2024 +0200
@@ -49,7 +49,7 @@
else "\\" ^ ch)
end);
-val strings = space_implode " " o map string;
+val strings = implode_space o map string;
(* server parameters *)
--- a/src/Pure/Thy/document_antiquotation.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/Pure/Thy/document_antiquotation.ML Fri Sep 20 14:28:13 2024 +0200
@@ -61,7 +61,7 @@
fun trim_lines ctxt =
if not (Config.get ctxt thy_output_display) then
- split_lines #> map Symbol.trim_blanks #> space_implode " "
+ split_lines #> map Symbol.trim_blanks #> implode_space
else I;
fun indent_lines ctxt =
--- a/src/Pure/Thy/document_output.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/Pure/Thy/document_output.ML Fri Sep 20 14:28:13 2024 +0200
@@ -530,7 +530,7 @@
fun source ctxt embedded =
Token.args_of_src
#> map (token_source ctxt embedded #> Document_Antiquotation.prepare_lines ctxt)
- #> space_implode " "
+ #> implode_space
#> output_source ctxt
#> isabelle ctxt;
--- a/src/Pure/library.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/Pure/library.ML Fri Sep 20 14:28:13 2024 +0200
@@ -143,6 +143,7 @@
val quote: string -> string
val cartouche: string -> string
val space_implode: string -> string list -> string
+ val implode_space: string list -> string
val commas: string list -> string
val commas_quote: string list -> string
val cat_lines: string list -> string
@@ -740,6 +741,7 @@
val cartouche = enclose "\<open>" "\<close>";
val space_implode = String.concatWith;
+val implode_space = space_implode " ";
val commas = space_implode ", ";
val commas_quote = commas o map quote;
@@ -752,7 +754,7 @@
val split_lines = space_explode "\n";
-fun plain_words s = space_explode "_" s |> space_implode " ";
+val plain_words = implode_space o space_explode "_";
fun prefix_lines "" txt = txt
| prefix_lines prfx txt = txt |> split_lines |> map (fn s => prfx ^ s) |> cat_lines;
--- a/src/Pure/pattern.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/Pure/pattern.ML Fri Sep 20 14:28:13 2024 +0200
@@ -36,7 +36,7 @@
Syntax.string_of_term ctxt (Envir.norm_term env (subst_bounds (map Free binders, t)));
fun bname binders i = fst (nth binders i);
-fun bnames binders is = space_implode " " (map (bname binders) is);
+fun bnames binders is = implode_space (map (bname binders) is);
fun typ_clash context (tye,T,U) =
if Config.get_generic context unify_trace_failure then
--- a/src/Tools/Code/code_haskell.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/Tools/Code/code_haskell.ML Fri Sep 20 14:28:13 2024 +0200
@@ -23,7 +23,7 @@
"{-# LANGUAGE " ^ commas language_extensions ^ " #-}";
val language_params =
- space_implode " " (map (prefix "-X") language_extensions);
+ implode_space (map (prefix "-X") language_extensions);
open Basic_Code_Symbol;
open Basic_Code_Thingol;
--- a/src/Tools/Code/code_runtime.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/Tools/Code/code_runtime.ML Fri Sep 20 14:28:13 2024 +0200
@@ -97,7 +97,7 @@
fun run_compilation_text cookie ctxt comp vs_t args =
let
val (program_code, value_name) = comp vs_t;
- val value_code = space_implode " "
+ val value_code = implode_space
(value_name :: "()" :: map (enclose "(" ")") args);
in Exn.result (value ctxt cookie) (program_code, value_code) end;
@@ -582,7 +582,7 @@
fun print_computation kind ctxt T =
print (fn { of_term_for_typ, ... } => fn prfx =>
- enclose "(" ")" (space_implode " " [
+ enclose "(" ")" (implode_space [
kind,
"(Context.proof_of (Context.the_generic_context ()))",
Long_Name.implode [prfx, generated_computationN, covered_constsN],
@@ -592,7 +592,7 @@
fun print_computation_check ctxt =
print (fn { of_term_for_typ, ... } => fn prfx =>
- enclose "(" ")" (space_implode " " [
+ enclose "(" ")" (implode_space [
mount_computation_checkN,
"(Context.proof_of (Context.the_generic_context ()))",
Long_Name.implode [prfx, generated_computationN, covered_constsN],
--- a/src/Tools/Haskell/Haskell.thy Fri Sep 20 13:30:55 2024 +0200
+++ b/src/Tools/Haskell/Haskell.thy Fri Sep 20 14:28:13 2024 +0200
@@ -1564,7 +1564,7 @@
show_tree (Text s) = Buffer.add (encode_text s)
show_elem name atts =
- space_implode " " (name : map (\(a, x) -> a <> "=\"" <> encode_text x <> "\"") atts)
+ implode_space (name : map (\(a, x) -> a <> "=\"" <> encode_text x <> "\"") atts)
\<close>
generate_file "Isabelle/XML/Encode.hs" = \<open>
@@ -3473,7 +3473,7 @@
else "\\" <> Bytes.singleton b
strings :: [Bytes] -> Bytes
-strings = space_implode " " . map string
+strings = implode_space . map string
{- server parameters -}
--- a/src/Tools/nbe.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/Tools/nbe.ML Fri Sep 20 14:28:13 2024 +0200
@@ -203,7 +203,7 @@
infix 9 `$` `$$`;
fun e1 `$` e2 = "(" ^ e1 ^ " " ^ e2 ^ ")";
fun e `$$` [] = e
- | e `$$` es = "(" ^ e ^ " " ^ space_implode " " es ^ ")";
+ | e `$$` es = "(" ^ e ^ " " ^ implode_space es ^ ")";
fun ml_abs v e = "(fn " ^ v ^ " => " ^ e ^ ")";
fun ml_cases t cs =
@@ -224,7 +224,7 @@
let
fun fundef (name, eqs) =
let
- fun eqn (es, e) = name ^ " " ^ space_implode " " es ^ " = " ^ e
+ fun eqn (es, e) = name ^ " " ^ implode_space es ^ " = " ^ e
in space_implode "\n | " (map eqn eqs) end;
in
(prefix "fun " o fundef) eqs :: map (prefix "and " o fundef) eqss
--- a/src/Tools/try.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/Tools/try.ML Fri Sep 20 14:28:13 2024 +0200
@@ -55,7 +55,7 @@
else
get_tools (Proof.theory_of state)
|> tap (fn tools =>
- "Trying " ^ space_implode " "
+ "Trying " ^ implode_space
(serial_commas "and" (map (quote o #name) tools)) ^ "..."
|> writeln)
|> Par_List.get_some