# HG changeset patch # User wenzelm # Date 1211031102 -7200 # Node ID aa226d8405a88f9bc83204de3feb23aa3a5792fc # Parent 64e50d7832768a51aea38e06979c3e4f62b56903 cat_lines; diff -r 64e50d783276 -r aa226d8405a8 src/HOL/Tools/datatype_case.ML --- a/src/HOL/Tools/datatype_case.ML Sat May 17 14:27:02 2008 +0200 +++ b/src/HOL/Tools/datatype_case.ML Sat May 17 15:31:42 2008 +0200 @@ -291,7 +291,7 @@ [] => () | is => (if err then case_error else warning) ("The following clauses are redundant (covered by preceding clauses):\n" ^ - space_implode "\n" (map (string_of_clause o nth clauses) is)); + cat_lines (map (string_of_clause o nth clauses) is)); in (case_tm, patts2) end; diff -r 64e50d783276 -r aa226d8405a8 src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Sat May 17 14:27:02 2008 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Sat May 17 15:31:42 2008 +0200 @@ -126,7 +126,7 @@ (iss @ [SOME is])); fun print_modes modes = message ("Inferred modes:\n" ^ - space_implode "\n" (map (fn (s, ms) => s ^ ": " ^ commas (map + cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map string_of_mode ms)) modes)); val term_vs = map (fst o fst o dest_Var) o term_vars; @@ -471,7 +471,7 @@ (Graph.all_preds (fst gr) [dep])))); fun print_arities arities = message ("Arities:\n" ^ - space_implode "\n" (map (fn (s, (ks, k)) => s ^ ": " ^ + cat_lines (map (fn (s, (ks, k)) => s ^ ": " ^ space_implode " -> " (map (fn NONE => "X" | SOME k' => string_of_int k') (ks @ [SOME k]))) arities)); diff -r 64e50d783276 -r aa226d8405a8 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Sat May 17 14:27:02 2008 +0200 +++ b/src/HOL/Tools/meson.ML Sat May 17 15:31:42 2008 +0200 @@ -625,9 +625,9 @@ let val horns = make_horns (cls@ths) val _ = Output.debug (fn () => ("meson method called:\n" ^ - space_implode "\n" (map Display.string_of_thm (cls@ths)) ^ + cat_lines (map Display.string_of_thm (cls@ths)) ^ "\nclauses:\n" ^ - space_implode "\n" (map Display.string_of_thm horns))) + cat_lines (map Display.string_of_thm horns))) in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) end ); diff -r 64e50d783276 -r aa226d8405a8 src/HOL/Tools/metis_tools.ML --- a/src/HOL/Tools/metis_tools.ML Sat May 17 14:27:02 2008 +0200 +++ b/src/HOL/Tools/metis_tools.ML Sat May 17 15:31:42 2008 +0200 @@ -230,9 +230,9 @@ else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^ " but gets " ^ Int.toString (length tys) ^ " type arguments\n" ^ - space_implode "\n" (map (Syntax.string_of_typ ctxt) tys) ^ + cat_lines (map (Syntax.string_of_typ ctxt) tys) ^ " the terms are \n" ^ - space_implode "\n" (map (Syntax.string_of_term ctxt) (terms_of tts))) + cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts))) end | NONE => (*Not a constant. Is it a type constructor?*) case Recon.strip_prefix ResClause.tconst_prefix a of diff -r 64e50d783276 -r aa226d8405a8 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Sat May 17 14:27:02 2008 +0200 +++ b/src/HOL/Tools/refute.ML Sat May 17 15:31:42 2008 +0200 @@ -263,7 +263,7 @@ if null terms then "empty interpretation (no free variables in term)\n" else - space_implode "\n" (List.mapPartial (fn (t, intr) => + cat_lines (List.mapPartial (fn (t, intr) => (* print constants only if 'show_consts' is true *) if (!show_consts) orelse not (is_Const t) then SOME (Sign.string_of_term thy t ^ ": " ^ diff -r 64e50d783276 -r aa226d8405a8 src/HOL/Tools/refute_isar.ML --- a/src/HOL/Tools/refute_isar.ML Sat May 17 14:27:02 2008 +0200 +++ b/src/HOL/Tools/refute_isar.ML Sat May 17 15:31:42 2008 +0200 @@ -87,7 +87,7 @@ val output = if new_default_params=[] then "none" else - space_implode "\n" (map (fn (name, value) => name ^ "=" ^ value) + cat_lines (map (fn (name, value) => name ^ "=" ^ value) new_default_params) in writeln ("Default parameters for 'refute':\n" ^ output); diff -r 64e50d783276 -r aa226d8405a8 src/HOL/Tools/sat_funcs.ML --- a/src/HOL/Tools/sat_funcs.ML Sat May 17 14:27:02 2008 +0200 +++ b/src/HOL/Tools/sat_funcs.ML Sat May 17 15:31:42 2008 +0200 @@ -325,12 +325,12 @@ (* sorted in ascending order *) val sorted_clauses = sort (Term.fast_term_ord o pairself Thm.term_of) nontrivial_clauses val _ = if !trace_sat then - tracing ("Sorted non-trivial clauses:\n" ^ space_implode "\n" (map Display.string_of_cterm sorted_clauses)) + tracing ("Sorted non-trivial clauses:\n" ^ cat_lines (map Display.string_of_cterm sorted_clauses)) else () (* translate clauses from HOL terms to PropLogic.prop_formula *) val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of) sorted_clauses Termtab.empty val _ = if !trace_sat then - tracing ("Invoking SAT solver on clauses:\n" ^ space_implode "\n" (map string_of_prop_formula fms)) + tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms)) else () val fm = PropLogic.all fms (* unit -> Thm.thm *) diff -r 64e50d783276 -r aa226d8405a8 src/HOL/Tools/watcher.ML --- a/src/HOL/Tools/watcher.ML Sat May 17 14:27:02 2008 +0200 +++ b/src/HOL/Tools/watcher.ML Sat May 17 15:31:42 2008 +0200 @@ -346,7 +346,7 @@ Display.string_of_cterm (List.nth(cprems_of th, i-1)) handle Subscript => "Subgoal number out of range!" -fun prems_string_of th = space_implode "\n" (map Display.string_of_cterm (cprems_of th)) +fun prems_string_of th = cat_lines (map Display.string_of_cterm (cprems_of th)) fun read_proof probfile = let val p = ResReconstruct.txt_path probfile diff -r 64e50d783276 -r aa226d8405a8 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Sat May 17 14:27:02 2008 +0200 +++ b/src/Pure/codegen.ML Sat May 17 15:31:42 2008 +0200 @@ -699,7 +699,7 @@ NONE => (case get_aux_code aux of [] => (gr4, p module) | xs => (add_edge (node_id, dep) (new_node - (node_id, (NONE, module', space_implode "\n" xs ^ "\n")) gr4), + (node_id, (NONE, module', cat_lines xs ^ "\n")) gr4), p module')) | SOME (_, module'', _) => (add_edge (node_id, dep) gr4, p module'')) @@ -780,7 +780,7 @@ [] => (gr'', p module') | xs => (fst (mk_type_id module' s (add_edge (node_id, dep) (new_node (node_id, - (NONE, module', space_implode "\n" xs ^ "\n")) gr''))), + (NONE, module', cat_lines xs ^ "\n")) gr''))), p module')) | SOME (_, module'', _) => (add_edge (node_id, dep) gr'', p module'')) @@ -943,7 +943,7 @@ val (code, gr) = setmp mode ["term_of", "test"] (generate_code_i thy [] "Generated") [("testf", list_abs_free (frees, t))]; val s = PrintMode.setmp [] (fn () => "structure TestTerm =\nstruct\n\n" ^ - space_implode "\n" (map snd code) ^ + cat_lines (map snd code) ^ "\nopen Generated;\n\n" ^ Pretty.string_of (Pretty.block [Pretty.str "val () = Codegen.test_fn :=", Pretty.brk 1, Pretty.str ("(fn i =>"), Pretty.brk 1, @@ -1044,7 +1044,7 @@ (generate_code_i thy [] "Generated") [("result", Abs ("x", TFree ("'a", []), t))]; val s = "structure EvalTerm =\nstruct\n\n" ^ - space_implode "\n" (map snd code) ^ + cat_lines (map snd code) ^ "\nopen Generated;\n\n" ^ Pretty.string_of (Pretty.block [Pretty.str "val () = Codegen.eval_result := (fn () =>", Pretty.brk 1, @@ -1149,7 +1149,7 @@ in ((case opt_fname of NONE => ML_Context.eval_in (SOME (Context.Theory thy)) false Position.none - (space_implode "\n" (map snd code)) + (cat_lines (map snd code)) | SOME fname => if lib then app (fn (name, s) => File.write diff -r 64e50d783276 -r aa226d8405a8 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Sat May 17 14:27:02 2008 +0200 +++ b/src/Tools/nbe.ML Sat May 17 15:31:42 2008 +0200 @@ -103,7 +103,7 @@ in space_implode "\n | " (map eqn eqs) end; in (prefix "fun " o fundef) eqs :: map (prefix "and " o fundef) eqss - |> space_implode "\n" + |> cat_lines |> suffix "\n" end;