--- a/src/HOL/Import/hol4rews.ML Sat May 29 14:55:56 2004 +0200
+++ b/src/HOL/Import/hol4rews.ML Sat May 29 14:57:39 2004 +0200
@@ -650,7 +650,7 @@
val _ = app (fn (hol,(internal,isa,opt_ty)) =>
(out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy)));
case opt_ty of
- Some ty => out (" :: \"" ^ (string_of_ctyp (ctyp_of sg ty)) ^ "\"")
+ Some ty => out (" :: \"" ^ (Output.output (string_of_ctyp (ctyp_of sg ty))) ^ "\"")
| None => ())) constmaps
val _ = if null constmaps
then ()
--- a/src/HOL/Import/import_package.ML Sat May 29 14:55:56 2004 +0200
+++ b/src/HOL/Import/import_package.ML Sat May 29 14:57:39 2004 +0200
@@ -30,8 +30,8 @@
val debug = ref false
fun message s = if !debug then writeln s else ()
-val string_of_thm = Library.setmp print_mode [] string_of_thm
-val string_of_cterm = Library.setmp print_mode [] string_of_cterm
+val string_of_thm = Library.setmp print_mode [] (Output.output o string_of_thm);
+val string_of_cterm = Library.setmp print_mode [] (Output.output o string_of_cterm);
fun import_tac (thyname,thmname) =
if !SkipProof.quick_and_dirty
--- a/src/HOL/Import/proof_kernel.ML Sat May 29 14:55:56 2004 +0200
+++ b/src/HOL/Import/proof_kernel.ML Sat May 29 14:57:39 2004 +0200
@@ -190,7 +190,7 @@
| G _ = error ("ProofKernel.smart_string_of_cterm internal error: " ^ (G 2 string_of_cterm ct))
fun F sh_br n =
let
- val str = Library.setmp show_brackets sh_br (G n string_of_cterm) ct
+ val str = Library.setmp show_brackets sh_br (G n (Output.output o string_of_cterm)) ct
val cu = transform_error (read_cterm sign) (str,T)
in
if match cu
@@ -208,7 +208,7 @@
handle ERROR_MESSAGE mesg =>
(writeln "Exception in smart_string_of_cterm!";
writeln mesg;
- quote (string_of_cterm ct))
+ quote (Output.output (string_of_cterm ct)))
val smart_string_of_thm = smart_string_of_cterm o cprop_of
@@ -1898,9 +1898,9 @@
val crhs = cterm_of sg (#2 (Logic.dest_equals (prop_of rew)))
val thy22 = if (def_name constname) = thmname andalso not redeclared andalso csyn = NoSyn
then
- add_dump ("constdefs\n " ^ (quotename constname) ^ " :: \"" ^ (string_of_ctyp (ctyp_of sg ctype)) ^ "\" " ^ (Syntax.string_of_mixfix csyn) ^ "\n " ^ (smart_string_of_cterm crhs)) thy''
+ add_dump ("constdefs\n " ^ (quotename constname) ^ " :: \"" ^ Output.output (string_of_ctyp (ctyp_of sg ctype)) ^ "\" " ^ (Syntax.string_of_mixfix csyn) ^ "\n " ^ (smart_string_of_cterm crhs)) thy''
else
- add_dump ("consts\n " ^ (quotename constname) ^ " :: \"" ^ (string_of_ctyp (ctyp_of sg ctype)) ^
+ add_dump ("consts\n " ^ (quotename constname) ^ " :: \"" ^ Output.output (string_of_ctyp (ctyp_of sg ctype)) ^
"\" " ^ (Syntax.string_of_mixfix csyn) ^ "\n\ndefs\n " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs))
thy''
@@ -1964,7 +1964,7 @@
end) (([],HOLogic.dest_Trueprop (concl_of th)),names)
val sg = sign_of thy
val str = foldl (fn (acc,(c,T,csyn)) =>
- acc ^ "\n " ^ (quotename c) ^ " :: \"" ^ (string_of_ctyp (ctyp_of sg T)) ^ "\" " ^ (Syntax.string_of_mixfix csyn)) ("consts",consts)
+ acc ^ "\n " ^ (quotename c) ^ " :: \"" ^ Output.output (string_of_ctyp (ctyp_of sg T)) ^ "\" " ^ (Syntax.string_of_mixfix csyn)) ("consts",consts)
val thy' = add_dump str thy
in
Theory.add_consts_i consts thy'
--- a/src/HOL/Import/shuffler.ML Sat May 29 14:55:56 2004 +0200
+++ b/src/HOL/Import/shuffler.ML Sat May 29 14:57:39 2004 +0200
@@ -58,10 +58,8 @@
(*Prints an exception, then fails*)
fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e)
-val string_of_thm = Library.setmp print_mode [] string_of_thm
-val string_of_cterm = Library.setmp print_mode [] string_of_cterm
-
-val commafy = String.concat o separate ", "
+val string_of_thm = Library.setmp print_mode [] (Output.output o string_of_thm);
+val string_of_cterm = Library.setmp print_mode [] (Output.output o string_of_cterm);
fun mk_meta_eq th =
(case concl_of th of
--- a/src/HOL/Modelcheck/MuCalculus.ML Sat May 29 14:55:56 2004 +0200
+++ b/src/HOL/Modelcheck/MuCalculus.ML Sat May 29 14:57:39 2004 +0200
@@ -13,8 +13,7 @@
local
fun termtext sign term =
- setmp print_mode ["Eindhoven"]
- (Sign.string_of_term sign) term;
+ setmp print_mode ["Eindhoven"] (Output.output o Sign.string_of_term sign) term;
fun call_mc s =
execute ( "echo \"" ^ s ^ "\" | pmu -w" );
--- a/src/HOL/Modelcheck/mucke_oracle.ML Sat May 29 14:55:56 2004 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Sat May 29 14:57:39 2004 +0200
@@ -486,8 +486,8 @@
fun string_of_terms sign terms =
let fun make_string sign [] = "" |
- make_string sign (trm::list) =
- ((Sign.string_of_term sign trm) ^ "\n" ^(make_string sign list))
+ make_string sign (trm::list) =
+ ((Output.output (Sign.string_of_term sign trm)) ^ "\n" ^(make_string sign list))
in
(setmp print_mode ["Mucke"] (make_string sign) terms)
end;
--- a/src/HOL/Tools/refute.ML Sat May 29 14:55:56 2004 +0200
+++ b/src/HOL/Tools/refute.ML Sat May 29 14:57:39 2004 +0200
@@ -59,6 +59,9 @@
structure Refute : REFUTE =
struct
+ (* FIXME comptibility -- should avoid std_output altogether *)
+ val std_output = Output.std_output o Output.output;
+
open PropLogic;
(* We use 'REFUTE' only for internal error conditions that should *)
--- a/src/Pure/codegen.ML Sat May 29 14:55:56 2004 +0200
+++ b/src/Pure/codegen.ML Sat May 29 14:57:39 2004 +0200
@@ -449,11 +449,11 @@
(Graph.new_node (id, (None, "")) gr'), rhs');
val (gr2, xs) = codegens false (gr1, args');
val (gr3, ty) = invoke_tycodegen thy id false (gr2, T);
- in Graph.map_node id (K (None, Pretty.string_of (Pretty.block
+ in Graph.map_node id (K (None, Output.output (Pretty.string_of (Pretty.block
(separate (Pretty.brk 1) (if null args' then
[Pretty.str ("val " ^ id ^ " :"), ty]
else Pretty.str ("fun " ^ id) :: xs) @
- [Pretty.str " =", Pretty.brk 1, p, Pretty.str ";"])) ^ "\n\n")) gr3
+ [Pretty.str " =", Pretty.brk 1, p, Pretty.str ";"])) ^ "\n\n"))) gr3
end, mk_app brack (Pretty.str id) ps)
end))
@@ -499,13 +499,13 @@
val (gr', ps) = foldl_map (fn (gr, (s, t)) => apsnd (pair s)
(invoke_codegen thy "<Top>" false (gr, t)))
(gr, map (apsnd (prep_term sg)) xs)
- in
- "structure Generated =\nstruct\n\n" ^
- output_code gr' ["<Top>"] ^
- space_implode "\n\n" (map (fn (s', p) => Pretty.string_of (Pretty.block
- [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, p, Pretty.str ";"])) ps) ^
- "\n\nend;\n\nopen Generated;\n"
- end));
+ val code =
+ "structure Generated =\nstruct\n\n" ^
+ output_code gr' ["<Top>"] ^
+ space_implode "\n\n" (map (fn (s', p) => Pretty.string_of (Pretty.block
+ [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, p, Pretty.str ";"])) ps) ^
+ "\n\nend;\n\nopen Generated;\n";
+ in Output.output code end));
val generate_code_i = gen_generate_code (K I);
val generate_code = gen_generate_code
@@ -559,7 +559,7 @@
val s = "structure TestTerm =\nstruct\n\n" ^
setmp mode ["term_of", "test"] (generate_code_i thy)
[("testf", list_abs_free (frees, t))] ^
- "\n" ^ Pretty.string_of
+ "\n" ^ Output.output (Pretty.string_of
(Pretty.block [Pretty.str "val () = Codegen.test_fn :=",
Pretty.brk 1, Pretty.str ("(fn " ^ szname ^ " =>"), Pretty.brk 1,
Pretty.blk (0, [Pretty.str "let", Pretty.brk 1,
@@ -579,7 +579,7 @@
mk_app false (mk_term_of sg false T)
[Pretty.str s], Pretty.str ")"]]) frees)) @
[Pretty.str "]"])]],
- Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^
+ Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"])) ^
"\n\nend;\n";
val _ = use_text Context.ml_output false s;
fun iter f k = if k > i then None