Output.add_mode; Output.timing;

--- a/src/Pure/proof_general.ML	Sat May 29 15:02:13 2004 +0200
+++ b/src/Pure/proof_general.ML	Sat May 29 15:02:35 2004 +0200
@@ -44,10 +44,13 @@
 
 local
 
+fun xsym_output "\\" = "\\\\"
+  | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
+
 fun xsymbols_output s =
   if xsymbolsN mem_string ! print_mode andalso exists_string (equal "\\") s then
     let val syms = Symbol.explode s
-    in (implode (map (fn "\\" => "\\\\" | c => c) syms), real (Symbol.length syms)) end
+    in (implode (map xsym_output syms), real (Symbol.length syms)) end
   else (s, real (size s));
 
 fun pgml_output (s, len) =
@@ -56,8 +59,8 @@
 
 in
 
-fun setup_xsymbols_output () =
-  Symbol.add_mode proof_generalN (pgml_output o xsymbols_output, Symbol.default_indent);
+fun setup_xsymbols_output () = Output.add_mode proof_generalN
+  (pgml_output o xsymbols_output, Symbol.default_indent, Symbol.default_raw);
 
 end;
 
@@ -239,7 +242,7 @@
     ThyInfo.if_known_thy ThyInfo.touch_child_thys name;
     if not (Toplevel.is_toplevel state) then
       warning ("Not at toplevel -- cannot register theory " ^ quote name)
-    else Library.transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg =>
+    else transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg =>
       (warning msg; warning ("Failed to register theory " ^ quote name))
   end;
 
@@ -302,7 +305,7 @@
    ("show-main-goal", ("Whether to show main goal.",
       bool_option Proof.show_main_goal)),
    ("global-timing", ("Whether to enable timing in Isabelle.",
-      bool_option Library.timing)),
+      bool_option Output.timing)),
    ("theorem-dependencies", ("Whether to track theorem dependencies within Proof General.",
       thm_deps_option)),
    ("goals-limit", ("Setting for maximum number of goals printed in Isabelle.",