Output.output;
authorwenzelm
Sat May 29 14:57:39 2004 +0200 (2004-05-29)
changeset 14818ad83019a66a4
parent 14817 321ff6bf29d1
child 14819 4dae1cb304a4
Output.output;
src/HOL/Import/hol4rews.ML
src/HOL/Import/import_package.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/shuffler.ML
src/HOL/Modelcheck/MuCalculus.ML
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/Tools/refute.ML
src/Pure/codegen.ML
     1.1 --- a/src/HOL/Import/hol4rews.ML	Sat May 29 14:55:56 2004 +0200
     1.2 +++ b/src/HOL/Import/hol4rews.ML	Sat May 29 14:57:39 2004 +0200
     1.3 @@ -650,7 +650,7 @@
     1.4  	val _ = app (fn (hol,(internal,isa,opt_ty)) =>
     1.5  			(out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy)));
     1.6  			 case opt_ty of
     1.7 -			     Some ty => out (" :: \"" ^ (string_of_ctyp (ctyp_of sg ty)) ^ "\"")
     1.8 +			     Some ty => out (" :: \"" ^ (Output.output (string_of_ctyp (ctyp_of sg ty))) ^ "\"")
     1.9  			   | None => ())) constmaps
    1.10  	val _ = if null constmaps
    1.11  		then ()
     2.1 --- a/src/HOL/Import/import_package.ML	Sat May 29 14:55:56 2004 +0200
     2.2 +++ b/src/HOL/Import/import_package.ML	Sat May 29 14:57:39 2004 +0200
     2.3 @@ -30,8 +30,8 @@
     2.4  val debug = ref false
     2.5  fun message s = if !debug then writeln s else ()
     2.6  
     2.7 -val string_of_thm = Library.setmp print_mode [] string_of_thm
     2.8 -val string_of_cterm = Library.setmp print_mode [] string_of_cterm
     2.9 +val string_of_thm = Library.setmp print_mode [] (Output.output o string_of_thm);
    2.10 +val string_of_cterm = Library.setmp print_mode [] (Output.output o string_of_cterm);
    2.11  
    2.12  fun import_tac (thyname,thmname) =
    2.13      if !SkipProof.quick_and_dirty
     3.1 --- a/src/HOL/Import/proof_kernel.ML	Sat May 29 14:55:56 2004 +0200
     3.2 +++ b/src/HOL/Import/proof_kernel.ML	Sat May 29 14:57:39 2004 +0200
     3.3 @@ -190,7 +190,7 @@
     3.4  	  | G _ = error ("ProofKernel.smart_string_of_cterm internal error: " ^ (G 2 string_of_cterm ct))
     3.5  	fun F sh_br n =
     3.6  	    let
     3.7 -		val str = Library.setmp show_brackets sh_br (G n string_of_cterm) ct
     3.8 +		val str = Library.setmp show_brackets sh_br (G n (Output.output o string_of_cterm)) ct
     3.9  		val cu  = transform_error (read_cterm sign) (str,T)
    3.10  	    in
    3.11  		if match cu
    3.12 @@ -208,7 +208,7 @@
    3.13      handle ERROR_MESSAGE mesg =>
    3.14  	   (writeln "Exception in smart_string_of_cterm!";
    3.15  	    writeln mesg;
    3.16 -	    quote (string_of_cterm ct))
    3.17 +	    quote (Output.output (string_of_cterm ct)))
    3.18  
    3.19  val smart_string_of_thm = smart_string_of_cterm o cprop_of
    3.20  
    3.21 @@ -1898,9 +1898,9 @@
    3.22  	val crhs = cterm_of sg (#2 (Logic.dest_equals (prop_of rew)))
    3.23  	val thy22 = if (def_name constname) = thmname andalso not redeclared andalso csyn = NoSyn
    3.24  		    then
    3.25 -			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''
    3.26 +			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''
    3.27  		    else
    3.28 -			add_dump ("consts\n  " ^ (quotename constname) ^ " :: \"" ^ (string_of_ctyp (ctyp_of sg ctype)) ^
    3.29 +			add_dump ("consts\n  " ^ (quotename constname) ^ " :: \"" ^ Output.output (string_of_ctyp (ctyp_of sg ctype)) ^
    3.30  				  "\" " ^ (Syntax.string_of_mixfix csyn) ^ "\n\ndefs\n  " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs))
    3.31  				 thy''
    3.32  
    3.33 @@ -1964,7 +1964,7 @@
    3.34  							  end) (([],HOLogic.dest_Trueprop (concl_of th)),names)
    3.35  			       val sg = sign_of thy
    3.36  			       val str = foldl (fn (acc,(c,T,csyn)) =>
    3.37 -						   acc ^ "\n  " ^ (quotename c) ^ " :: \"" ^ (string_of_ctyp (ctyp_of sg T)) ^ "\" " ^ (Syntax.string_of_mixfix csyn)) ("consts",consts)
    3.38 +						   acc ^ "\n  " ^ (quotename c) ^ " :: \"" ^ Output.output (string_of_ctyp (ctyp_of sg T)) ^ "\" " ^ (Syntax.string_of_mixfix csyn)) ("consts",consts)
    3.39  			       val thy' = add_dump str thy
    3.40  			   in
    3.41  			       Theory.add_consts_i consts thy'
     4.1 --- a/src/HOL/Import/shuffler.ML	Sat May 29 14:55:56 2004 +0200
     4.2 +++ b/src/HOL/Import/shuffler.ML	Sat May 29 14:57:39 2004 +0200
     4.3 @@ -58,10 +58,8 @@
     4.4  (*Prints an exception, then fails*)
     4.5  fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e)
     4.6  
     4.7 -val string_of_thm = Library.setmp print_mode [] string_of_thm
     4.8 -val string_of_cterm = Library.setmp print_mode [] string_of_cterm
     4.9 -
    4.10 -val commafy = String.concat o separate ", "
    4.11 +val string_of_thm = Library.setmp print_mode [] (Output.output o string_of_thm);
    4.12 +val string_of_cterm = Library.setmp print_mode [] (Output.output o string_of_cterm);
    4.13  
    4.14  fun mk_meta_eq th =
    4.15      (case concl_of th of
     5.1 --- a/src/HOL/Modelcheck/MuCalculus.ML	Sat May 29 14:55:56 2004 +0200
     5.2 +++ b/src/HOL/Modelcheck/MuCalculus.ML	Sat May 29 14:57:39 2004 +0200
     5.3 @@ -13,8 +13,7 @@
     5.4  local
     5.5  
     5.6  fun termtext sign term =
     5.7 -  setmp print_mode ["Eindhoven"]
     5.8 -    (Sign.string_of_term sign) term;
     5.9 +  setmp print_mode ["Eindhoven"] (Output.output o Sign.string_of_term sign) term;
    5.10  
    5.11  fun call_mc s =
    5.12    execute ( "echo \"" ^ s ^ "\" | pmu -w" );
     6.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Sat May 29 14:55:56 2004 +0200
     6.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Sat May 29 14:57:39 2004 +0200
     6.3 @@ -486,8 +486,8 @@
     6.4  
     6.5  fun string_of_terms sign terms =
     6.6  let fun make_string sign [] = "" |
     6.7 - 	make_string sign (trm::list) = 
     6.8 -           ((Sign.string_of_term sign trm) ^ "\n" ^(make_string sign list))
     6.9 + 	make_string sign (trm::list) =
    6.10 +           ((Output.output (Sign.string_of_term sign trm)) ^ "\n" ^(make_string sign list))
    6.11  in
    6.12  (setmp print_mode ["Mucke"] (make_string sign) terms)
    6.13  end;
     7.1 --- a/src/HOL/Tools/refute.ML	Sat May 29 14:55:56 2004 +0200
     7.2 +++ b/src/HOL/Tools/refute.ML	Sat May 29 14:57:39 2004 +0200
     7.3 @@ -59,6 +59,9 @@
     7.4  structure Refute : REFUTE =
     7.5  struct
     7.6  
     7.7 +	(* FIXME comptibility -- should avoid std_output altogether *)
     7.8 +	val std_output = Output.std_output o Output.output;
     7.9 +
    7.10  	open PropLogic;
    7.11  
    7.12  	(* We use 'REFUTE' only for internal error conditions that should    *)
     8.1 --- a/src/Pure/codegen.ML	Sat May 29 14:55:56 2004 +0200
     8.2 +++ b/src/Pure/codegen.ML	Sat May 29 14:57:39 2004 +0200
     8.3 @@ -449,11 +449,11 @@
     8.4                          (Graph.new_node (id, (None, "")) gr'), rhs');
     8.5                     val (gr2, xs) = codegens false (gr1, args');
     8.6                     val (gr3, ty) = invoke_tycodegen thy id false (gr2, T);
     8.7 -                 in Graph.map_node id (K (None, Pretty.string_of (Pretty.block
     8.8 +                 in Graph.map_node id (K (None, Output.output (Pretty.string_of (Pretty.block
     8.9                     (separate (Pretty.brk 1) (if null args' then
    8.10                         [Pretty.str ("val " ^ id ^ " :"), ty]
    8.11                       else Pretty.str ("fun " ^ id) :: xs) @
    8.12 -                    [Pretty.str " =", Pretty.brk 1, p, Pretty.str ";"])) ^ "\n\n")) gr3
    8.13 +                    [Pretty.str " =", Pretty.brk 1, p, Pretty.str ";"])) ^ "\n\n"))) gr3
    8.14                   end, mk_app brack (Pretty.str id) ps)
    8.15               end))
    8.16  
    8.17 @@ -499,13 +499,13 @@
    8.18      val (gr', ps) = foldl_map (fn (gr, (s, t)) => apsnd (pair s)
    8.19        (invoke_codegen thy "<Top>" false (gr, t)))
    8.20          (gr, map (apsnd (prep_term sg)) xs)
    8.21 -  in
    8.22 -    "structure Generated =\nstruct\n\n" ^
    8.23 -    output_code gr' ["<Top>"] ^
    8.24 -    space_implode "\n\n" (map (fn (s', p) => Pretty.string_of (Pretty.block
    8.25 -      [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, p, Pretty.str ";"])) ps) ^
    8.26 -    "\n\nend;\n\nopen Generated;\n"
    8.27 -  end));
    8.28 +    val code =
    8.29 +      "structure Generated =\nstruct\n\n" ^
    8.30 +      output_code gr' ["<Top>"] ^
    8.31 +      space_implode "\n\n" (map (fn (s', p) => Pretty.string_of (Pretty.block
    8.32 +        [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, p, Pretty.str ";"])) ps) ^
    8.33 +      "\n\nend;\n\nopen Generated;\n";
    8.34 +  in Output.output code end));
    8.35  
    8.36  val generate_code_i = gen_generate_code (K I);
    8.37  val generate_code = gen_generate_code
    8.38 @@ -559,7 +559,7 @@
    8.39      val s = "structure TestTerm =\nstruct\n\n" ^
    8.40        setmp mode ["term_of", "test"] (generate_code_i thy)
    8.41          [("testf", list_abs_free (frees, t))] ^
    8.42 -      "\n" ^ Pretty.string_of
    8.43 +      "\n" ^ Output.output (Pretty.string_of
    8.44          (Pretty.block [Pretty.str "val () = Codegen.test_fn :=",
    8.45            Pretty.brk 1, Pretty.str ("(fn " ^ szname ^ " =>"), Pretty.brk 1,
    8.46            Pretty.blk (0, [Pretty.str "let", Pretty.brk 1,
    8.47 @@ -579,7 +579,7 @@
    8.48                       mk_app false (mk_term_of sg false T)
    8.49                         [Pretty.str s], Pretty.str ")"]]) frees)) @
    8.50                    [Pretty.str "]"])]],
    8.51 -            Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^
    8.52 +            Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"])) ^
    8.53        "\n\nend;\n";
    8.54      val _ = use_text Context.ml_output false s;
    8.55      fun iter f k = if k > i then None