cat_lines;
authorwenzelm
Sat May 17 15:31:42 2008 +0200 (2008-05-17)
changeset 26931aa226d8405a8
parent 26930 64e50d783276
child 26932 c398a3866082
cat_lines;
src/HOL/Tools/datatype_case.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/refute_isar.ML
src/HOL/Tools/sat_funcs.ML
src/HOL/Tools/watcher.ML
src/Pure/codegen.ML
src/Tools/nbe.ML
     1.1 --- a/src/HOL/Tools/datatype_case.ML	Sat May 17 14:27:02 2008 +0200
     1.2 +++ b/src/HOL/Tools/datatype_case.ML	Sat May 17 15:31:42 2008 +0200
     1.3 @@ -291,7 +291,7 @@
     1.4          [] => ()
     1.5        | is => (if err then case_error else warning)
     1.6            ("The following clauses are redundant (covered by preceding clauses):\n" ^
     1.7 -           space_implode "\n" (map (string_of_clause o nth clauses) is));
     1.8 +           cat_lines (map (string_of_clause o nth clauses) is));
     1.9    in
    1.10      (case_tm, patts2)
    1.11    end;
     2.1 --- a/src/HOL/Tools/inductive_codegen.ML	Sat May 17 14:27:02 2008 +0200
     2.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Sat May 17 15:31:42 2008 +0200
     2.3 @@ -126,7 +126,7 @@
     2.4         (iss @ [SOME is]));
     2.5  
     2.6  fun print_modes modes = message ("Inferred modes:\n" ^
     2.7 -  space_implode "\n" (map (fn (s, ms) => s ^ ": " ^ commas (map
     2.8 +  cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
     2.9      string_of_mode ms)) modes));
    2.10  
    2.11  val term_vs = map (fst o fst o dest_Var) o term_vars;
    2.12 @@ -471,7 +471,7 @@
    2.13      (Graph.all_preds (fst gr) [dep]))));
    2.14  
    2.15  fun print_arities arities = message ("Arities:\n" ^
    2.16 -  space_implode "\n" (map (fn (s, (ks, k)) => s ^ ": " ^
    2.17 +  cat_lines (map (fn (s, (ks, k)) => s ^ ": " ^
    2.18      space_implode " -> " (map
    2.19        (fn NONE => "X" | SOME k' => string_of_int k')
    2.20          (ks @ [SOME k]))) arities));
     3.1 --- a/src/HOL/Tools/meson.ML	Sat May 17 14:27:02 2008 +0200
     3.2 +++ b/src/HOL/Tools/meson.ML	Sat May 17 15:31:42 2008 +0200
     3.3 @@ -625,9 +625,9 @@
     3.4               let val horns = make_horns (cls@ths)
     3.5                   val _ =
     3.6                       Output.debug (fn () => ("meson method called:\n" ^
     3.7 -                                  space_implode "\n" (map Display.string_of_thm (cls@ths)) ^
     3.8 +                                  cat_lines (map Display.string_of_thm (cls@ths)) ^
     3.9                                    "\nclauses:\n" ^
    3.10 -                                  space_implode "\n" (map Display.string_of_thm horns)))
    3.11 +                                  cat_lines (map Display.string_of_thm horns)))
    3.12               in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
    3.13               end
    3.14   );
     4.1 --- a/src/HOL/Tools/metis_tools.ML	Sat May 17 14:27:02 2008 +0200
     4.2 +++ b/src/HOL/Tools/metis_tools.ML	Sat May 17 15:31:42 2008 +0200
     4.3 @@ -230,9 +230,9 @@
     4.4                         else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^
     4.5                                     " but gets " ^ Int.toString (length tys) ^
     4.6                                     " type arguments\n" ^
     4.7 -                                   space_implode "\n" (map (Syntax.string_of_typ ctxt) tys) ^
     4.8 +                                   cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
     4.9                                     " the terms are \n" ^
    4.10 -                                   space_implode "\n" (map (Syntax.string_of_term ctxt) (terms_of tts)))
    4.11 +                                   cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
    4.12                         end
    4.13                  | NONE => (*Not a constant. Is it a type constructor?*)
    4.14                case Recon.strip_prefix ResClause.tconst_prefix a of
     5.1 --- a/src/HOL/Tools/refute.ML	Sat May 17 14:27:02 2008 +0200
     5.2 +++ b/src/HOL/Tools/refute.ML	Sat May 17 15:31:42 2008 +0200
     5.3 @@ -263,7 +263,7 @@
     5.4        if null terms then
     5.5          "empty interpretation (no free variables in term)\n"
     5.6        else
     5.7 -        space_implode "\n" (List.mapPartial (fn (t, intr) =>
     5.8 +        cat_lines (List.mapPartial (fn (t, intr) =>
     5.9            (* print constants only if 'show_consts' is true *)
    5.10            if (!show_consts) orelse not (is_Const t) then
    5.11              SOME (Sign.string_of_term thy t ^ ": " ^
     6.1 --- a/src/HOL/Tools/refute_isar.ML	Sat May 17 14:27:02 2008 +0200
     6.2 +++ b/src/HOL/Tools/refute_isar.ML	Sat May 17 15:31:42 2008 +0200
     6.3 @@ -87,7 +87,7 @@
     6.4  					val output             = if new_default_params=[] then
     6.5  							"none"
     6.6  						else
     6.7 -							space_implode "\n" (map (fn (name, value) => name ^ "=" ^ value)
     6.8 +							cat_lines (map (fn (name, value) => name ^ "=" ^ value)
     6.9  								new_default_params)
    6.10  				in
    6.11  					writeln ("Default parameters for 'refute':\n" ^ output);
     7.1 --- a/src/HOL/Tools/sat_funcs.ML	Sat May 17 14:27:02 2008 +0200
     7.2 +++ b/src/HOL/Tools/sat_funcs.ML	Sat May 17 15:31:42 2008 +0200
     7.3 @@ -325,12 +325,12 @@
     7.4  	(* sorted in ascending order                                          *)
     7.5  	val sorted_clauses = sort (Term.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
     7.6  	val _ = if !trace_sat then
     7.7 -			tracing ("Sorted non-trivial clauses:\n" ^ space_implode "\n" (map Display.string_of_cterm sorted_clauses))
     7.8 +			tracing ("Sorted non-trivial clauses:\n" ^ cat_lines (map Display.string_of_cterm sorted_clauses))
     7.9  		else ()
    7.10  	(* translate clauses from HOL terms to PropLogic.prop_formula *)
    7.11  	val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of) sorted_clauses Termtab.empty
    7.12  	val _ = if !trace_sat then
    7.13 -			tracing ("Invoking SAT solver on clauses:\n" ^ space_implode "\n" (map string_of_prop_formula fms))
    7.14 +			tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms))
    7.15  		else ()
    7.16  	val fm = PropLogic.all fms
    7.17  	(* unit -> Thm.thm *)
     8.1 --- a/src/HOL/Tools/watcher.ML	Sat May 17 14:27:02 2008 +0200
     8.2 +++ b/src/HOL/Tools/watcher.ML	Sat May 17 15:31:42 2008 +0200
     8.3 @@ -346,7 +346,7 @@
     8.4      Display.string_of_cterm (List.nth(cprems_of th, i-1))
     8.5      handle Subscript => "Subgoal number out of range!"
     8.6  
     8.7 -fun prems_string_of th = space_implode "\n" (map Display.string_of_cterm (cprems_of th))
     8.8 +fun prems_string_of th = cat_lines (map Display.string_of_cterm (cprems_of th))
     8.9  
    8.10  fun read_proof probfile =
    8.11    let val p = ResReconstruct.txt_path probfile
     9.1 --- a/src/Pure/codegen.ML	Sat May 17 14:27:02 2008 +0200
     9.2 +++ b/src/Pure/codegen.ML	Sat May 17 15:31:42 2008 +0200
     9.3 @@ -699,7 +699,7 @@
     9.4                     NONE => (case get_aux_code aux of
     9.5                         [] => (gr4, p module)
     9.6                       | xs => (add_edge (node_id, dep) (new_node
     9.7 -                         (node_id, (NONE, module', space_implode "\n" xs ^ "\n")) gr4),
     9.8 +                         (node_id, (NONE, module', cat_lines xs ^ "\n")) gr4),
     9.9                             p module'))
    9.10                   | SOME (_, module'', _) =>
    9.11                       (add_edge (node_id, dep) gr4, p module''))
    9.12 @@ -780,7 +780,7 @@
    9.13                     [] => (gr'', p module')
    9.14                   | xs => (fst (mk_type_id module' s
    9.15                         (add_edge (node_id, dep) (new_node (node_id,
    9.16 -                         (NONE, module', space_implode "\n" xs ^ "\n")) gr''))),
    9.17 +                         (NONE, module', cat_lines xs ^ "\n")) gr''))),
    9.18                       p module'))
    9.19               | SOME (_, module'', _) =>
    9.20                   (add_edge (node_id, dep) gr'', p module''))
    9.21 @@ -943,7 +943,7 @@
    9.22      val (code, gr) = setmp mode ["term_of", "test"]
    9.23        (generate_code_i thy [] "Generated") [("testf", list_abs_free (frees, t))];
    9.24      val s = PrintMode.setmp [] (fn () => "structure TestTerm =\nstruct\n\n" ^
    9.25 -      space_implode "\n" (map snd code) ^
    9.26 +      cat_lines (map snd code) ^
    9.27        "\nopen Generated;\n\n" ^ Pretty.string_of
    9.28          (Pretty.block [Pretty.str "val () = Codegen.test_fn :=",
    9.29            Pretty.brk 1, Pretty.str ("(fn i =>"), Pretty.brk 1,
    9.30 @@ -1044,7 +1044,7 @@
    9.31          (generate_code_i thy [] "Generated")
    9.32          [("result", Abs ("x", TFree ("'a", []), t))];
    9.33        val s = "structure EvalTerm =\nstruct\n\n" ^
    9.34 -        space_implode "\n" (map snd code) ^
    9.35 +        cat_lines (map snd code) ^
    9.36          "\nopen Generated;\n\n" ^ Pretty.string_of
    9.37            (Pretty.block [Pretty.str "val () = Codegen.eval_result := (fn () =>",
    9.38              Pretty.brk 1,
    9.39 @@ -1149,7 +1149,7 @@
    9.40       in ((case opt_fname of
    9.41           NONE =>
    9.42             ML_Context.eval_in (SOME (Context.Theory thy)) false Position.none
    9.43 -             (space_implode "\n" (map snd code))
    9.44 +             (cat_lines (map snd code))
    9.45         | SOME fname =>
    9.46             if lib then
    9.47               app (fn (name, s) => File.write
    10.1 --- a/src/Tools/nbe.ML	Sat May 17 14:27:02 2008 +0200
    10.2 +++ b/src/Tools/nbe.ML	Sat May 17 15:31:42 2008 +0200
    10.3 @@ -103,7 +103,7 @@
    10.4            in space_implode "\n  | " (map eqn eqs) end;
    10.5        in
    10.6          (prefix "fun " o fundef) eqs :: map (prefix "and " o fundef) eqss
    10.7 -        |> space_implode "\n"
    10.8 +        |> cat_lines
    10.9          |> suffix "\n"
   10.10        end;
   10.11