# HG changeset patch # User wenzelm # Date 1726835293 -7200 # Node ID 406a85a25189241992b97941f08acf478c28b641 # Parent 6ddbfad8ca208cd1d5785006df5d32732fb046b0 clarified signature: more explicit operations; diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/Library/Sum_of_Squares/sum_of_squares.ML --- 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) diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/SPARK/Tools/fdl_parser.ML --- 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 = diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML --- 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 ^ "[" ^ diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/TPTP/TPTP_Proof_Reconstruction.thy --- 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 ^)) diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/TPTP/atp_theory_export.ML --- 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 diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/TPTP/mash_eval.ML --- 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) = diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/TPTP/mash_export.ML --- 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 = diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/Tools/ATP/atp_proof.ML --- 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" diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/Tools/Argo/argo_tactic.ML --- 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 diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/Tools/Metis/metis_reconstruct.ML --- 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 diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/Tools/Nitpick/nitpick.ML --- 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 diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/Tools/Nitpick/nitpick_commands.ML --- 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 diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/Tools/Nunchaku/nunchaku_commands.ML --- 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)) diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/Tools/Nunchaku/nunchaku_display.ML --- 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 diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/Tools/Nunchaku/nunchaku_problem.ML --- 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 diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- 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 ^ ";" diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/Tools/Quotient/quotient_term.ML --- 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 diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/Tools/SMT/smt_config.ML --- 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: " ^ diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/Tools/SMT/smt_solver.ML --- 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 diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/Tools/SMT/smt_translate.ML --- 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 = diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/Tools/SMT/smtlib_interface.ML --- 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] diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/Tools/SMT/z3_proof.ML --- 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 diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/Tools/Sledgehammer/async_manager_legacy.ML --- 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 ( diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- 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 diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- 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 diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML --- 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 diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- 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; diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML --- 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 diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- 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 () diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- 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 ()) diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- 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 = diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/Tools/try0.ML --- 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 diff -r 6ddbfad8ca20 -r 406a85a25189 src/HOL/ex/Sketch_and_Explore.thy --- 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] diff -r 6ddbfad8ca20 -r 406a85a25189 src/Pure/General/graph_display.ML --- 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 diff -r 6ddbfad8ca20 -r 406a85a25189 src/Pure/Isar/locale.ML --- 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 diff -r 6ddbfad8ca20 -r 406a85a25189 src/Pure/Isar/obtain.ML --- 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 = diff -r 6ddbfad8ca20 -r 406a85a25189 src/Pure/Isar/proof_context.ML --- 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); diff -r 6ddbfad8ca20 -r 406a85a25189 src/Pure/Isar/token.ML --- 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 ()))) diff -r 6ddbfad8ca20 -r 406a85a25189 src/Pure/ML/ml_syntax.ML --- 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; diff -r 6ddbfad8ca20 -r 406a85a25189 src/Pure/PIDE/xml.ML --- 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 diff -r 6ddbfad8ca20 -r 406a85a25189 src/Pure/System/bash.ML --- 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 *) diff -r 6ddbfad8ca20 -r 406a85a25189 src/Pure/Thy/document_antiquotation.ML --- 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 = diff -r 6ddbfad8ca20 -r 406a85a25189 src/Pure/Thy/document_output.ML --- 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; diff -r 6ddbfad8ca20 -r 406a85a25189 src/Pure/library.ML --- 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 "\" "\"; 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; diff -r 6ddbfad8ca20 -r 406a85a25189 src/Pure/pattern.ML --- 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 diff -r 6ddbfad8ca20 -r 406a85a25189 src/Tools/Code/code_haskell.ML --- 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; diff -r 6ddbfad8ca20 -r 406a85a25189 src/Tools/Code/code_runtime.ML --- 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], diff -r 6ddbfad8ca20 -r 406a85a25189 src/Tools/Haskell/Haskell.thy --- 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) \ generate_file "Isabelle/XML/Encode.hs" = \ @@ -3473,7 +3473,7 @@ else "\\" <> Bytes.singleton b strings :: [Bytes] -> Bytes -strings = space_implode " " . map string +strings = implode_space . map string {- server parameters -} diff -r 6ddbfad8ca20 -r 406a85a25189 src/Tools/nbe.ML --- 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 diff -r 6ddbfad8ca20 -r 406a85a25189 src/Tools/try.ML --- 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