# HG changeset patch # User wenzelm # Date 1085835459 -7200 # Node ID ad83019a66a4b2165e75892be844465b8324ba6b # Parent 321ff6bf29d1a3f84a6b02ebd648aadd6fba252c Output.output; diff -r 321ff6bf29d1 -r ad83019a66a4 src/HOL/Import/hol4rews.ML --- 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 () diff -r 321ff6bf29d1 -r ad83019a66a4 src/HOL/Import/import_package.ML --- 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 diff -r 321ff6bf29d1 -r ad83019a66a4 src/HOL/Import/proof_kernel.ML --- 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' diff -r 321ff6bf29d1 -r ad83019a66a4 src/HOL/Import/shuffler.ML --- 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 diff -r 321ff6bf29d1 -r ad83019a66a4 src/HOL/Modelcheck/MuCalculus.ML --- 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" ); diff -r 321ff6bf29d1 -r ad83019a66a4 src/HOL/Modelcheck/mucke_oracle.ML --- 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; diff -r 321ff6bf29d1 -r ad83019a66a4 src/HOL/Tools/refute.ML --- 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 *) diff -r 321ff6bf29d1 -r ad83019a66a4 src/Pure/codegen.ML --- 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 "" false (gr, t))) (gr, map (apsnd (prep_term sg)) xs) - in - "structure Generated =\nstruct\n\n" ^ - output_code gr' [""] ^ - 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' [""] ^ + 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