# HG changeset patch
# User wenzelm
# Date 1086539739 -7200
# Node ID e1f501a141593e170d2d42a3cc4783153d38b5c6
# Parent  7586233bd4bdf06008cb8d851064b85f66872309
added has_mode; handle_error: output raw;

diff -r 7586233bd4bd -r e1f501a14159 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Sun Jun 06 18:35:26 2004 +0200
+++ b/src/Pure/General/output.ML	Sun Jun 06 18:35:39 2004 +0200
@@ -47,6 +47,7 @@
 signature OUTPUT =
 sig
   include BASIC_OUTPUT
+  val has_mode: string -> bool
   exception MISSING_DEFAULT_OUTPUT
   val output_width: string -> string * real
   val output: string -> string
@@ -63,6 +64,8 @@
 
 val print_mode = ref ([]: string list);
 
+fun has_mode s = s mem_string ! print_mode;
+
 val modes = ref (Symtab.empty:
   ((string -> string * real) * (string * int -> string) * (string -> string))
     Symtab.table);
@@ -151,7 +154,7 @@
 fun handle_error f x =
   let
     val buffer = ref ([]: string list);
-    fun store_msg s = buffer := ! buffer @ [s];
+    fun store_msg s = buffer := ! buffer @ [raw s];
     fun err_msg () = if not (null (! buffer)) then error_msg (cat_lines (! buffer)) else ();
   in
     (case Result (setmp error_fn store_msg f x) handle exn => Exn exn of