# HG changeset patch
# User wenzelm
# Date 1160415425 -7200
# Node ID b2f67b947200c3d161e3a2131c7ae3b1a0656039
# Parent  2d19e511fe2c584591dbbae1fa0ae2c670e66f28
moved Context.ml_output to Output.ml_output;

diff -r 2d19e511fe2c -r b2f67b947200 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Mon Oct 09 19:37:04 2006 +0200
+++ b/src/Pure/General/output.ML	Mon Oct 09 19:37:05 2006 +0200
@@ -54,6 +54,7 @@
   val info: string -> unit
   val debug: string -> unit
   val error_msg: string -> unit
+  val ml_output: (string -> unit) * (string -> unit)
   val add_mode: string ->
     (string -> string * real) * (bool -> string -> string * real) *
     (string * int -> string) * (string -> string) -> unit
@@ -134,6 +135,8 @@
 fun panic_msg s = ! panic_fn (output s);
 fun panic s = (panic_msg ("## SYSTEM EXIT ##\n" ^ s); exit 1);
 
+val ml_output = (writeln, error_msg);
+
 
 (* toplevel errors *)
 
diff -r 2d19e511fe2c -r b2f67b947200 src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Mon Oct 09 19:37:04 2006 +0200
+++ b/src/Pure/Thy/thm_database.ML	Mon Oct 09 19:37:05 2006 +0200
@@ -62,7 +62,7 @@
   else if name = "" then true
   else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true);
 
-val use_text_verbose = use_text Context.ml_output true;
+val use_text_verbose = use_text Output.ml_output true;
 
 fun ml_store_thm (name, thm) =
   let val thm' = store_thm (name, thm) in
diff -r 2d19e511fe2c -r b2f67b947200 src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Mon Oct 09 19:37:04 2006 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML	Mon Oct 09 19:37:05 2006 +0200
@@ -1123,7 +1123,7 @@
 fun parse_internal serializer =
   parse_args (Args.name
   >> (fn "-" => serializer
-        (fn "" => (fn p => (use_text Context.ml_output false (Pretty.output p); NONE))
+        (fn "" => (fn p => (use_text Output.ml_output false (Pretty.output p); NONE))
           | _ => SOME)
        | _ => Scan.fail ()));
 
@@ -1241,13 +1241,13 @@
       else Pretty.output p;
     val serializer = ml_serializer struct_name "SML" [[nsp_module], [nsp_class, nsp_tyco],
       [nsp_fun, nsp_dtco, nsp_class, nsp_classop, nsp_inst], [nsp_eval]]
-      (fn "" => (fn p => (use_text Context.ml_output (!eval_verbose) (output p); NONE))
+      (fn "" => (fn p => (use_text Output.ml_output (!eval_verbose) (output p); NONE))
         | _ => SOME) data
         (hidden, SOME [NameSpace.pack [nsp_eval, val_name]]);
     val _ = serializer code';
     val val_name_struct = NameSpace.append struct_name val_name;
     val _ = reff := NONE;
-    val _ = use_text Context.ml_output (!eval_verbose) ("val _ = (" ^ ref_name ^ " := SOME (" ^ val_name_struct ^ "))");
+    val _ = use_text Output.ml_output (!eval_verbose) ("val _ = (" ^ ref_name ^ " := SOME (" ^ val_name_struct ^ "))");
   in case !reff
    of NONE => error ("Could not retrieve value of ML reference " ^ quote ref_name
         ^ " (reference probably has been shadowed)")
diff -r 2d19e511fe2c -r b2f67b947200 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Mon Oct 09 19:37:04 2006 +0200
+++ b/src/Pure/codegen.ML	Mon Oct 09 19:37:05 2006 +0200
@@ -993,7 +993,7 @@
                   [Pretty.str "]"])]],
             Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^
       "\n\nend;\n") ();
-    val _ = use_text Context.ml_output false s;
+    val _ = use_text Output.ml_output false s;
     fun iter f k = if k > i then NONE
       else (case (f () handle Match =>
           (warning "Exception Match raised in generated code"; NONE)) of
@@ -1045,7 +1045,7 @@
             [Pretty.str "result"],
           Pretty.str ";"])  ^
       "\n\nend;\n";
-    val _ = use_text Context.ml_output false s
+    val _ = use_text Output.ml_output false s
   in !eval_result end);
 
 fun print_evaluated_term s = Toplevel.keep (fn state =>
@@ -1152,7 +1152,7 @@
        val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode');
        val (code, gr) = setmp mode mode'' (generate_code thy modules module) xs
      in ((case opt_fname of
-         NONE => use_text Context.ml_output false
+         NONE => use_text Output.ml_output false
            (space_implode "\n" (map snd code))
        | SOME fname =>
            if lib then
diff -r 2d19e511fe2c -r b2f67b947200 src/Pure/context.ML
--- a/src/Pure/context.ML	Mon Oct 09 19:37:04 2006 +0200
+++ b/src/Pure/context.ML	Mon Oct 09 19:37:05 2006 +0200
@@ -58,7 +58,6 @@
   val pass_theory: theory -> ('a -> 'b) -> 'a -> 'b * theory
   val save: ('a -> 'b) -> 'a -> 'b
   val >> : (theory -> theory) -> unit
-  val ml_output: (string -> unit) * (string -> unit)
   val use_mltext: string -> bool -> theory option -> unit
   val use_mltext_theory: string -> bool -> theory -> theory
   val use_let: string -> string -> string -> theory -> theory
@@ -482,10 +481,8 @@
 
 (* use ML text *)
 
-val ml_output = (writeln, Output.error_msg);
-
 fun use_output verbose txt =
-  Output.ML_errors (use_text ml_output verbose) (Symbol.escape txt);
+  Output.ML_errors (use_text Output.ml_output verbose) (Symbol.escape txt);
 
 fun use_mltext txt verbose opt_thy = setmp opt_thy (fn () => use_output verbose txt) ();
 fun use_mltext_theory txt verbose thy = #2 (pass_theory thy (use_output verbose) txt);