# HG changeset patch
# User wenzelm
# Date 1368303438 -7200
# Node ID 916c7fe684e3e5400452abad15a3839d71a5626e
# Parent  203a9528bf7ad328f03d13333fce4d48f3b3b75e
more direct PGIP/Emacs processing and output;

diff -r 203a9528bf7a -r 916c7fe684e3 src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat May 11 21:34:53 2013 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat May 11 22:17:18 2013 +0200
@@ -236,7 +236,7 @@
           Output.default_output Output.default_escape;
          Markup.add_mode ProofGeneralPgip.proof_general_emacsN YXML.output_markup;
          setup_messages ();
-         ProofGeneralPgip.pgip_channel_emacs (! Output.Private_Hooks.urgent_message_fn);
+         ProofGeneralPgip.init_pgip_session_id ();
          setup_thy_loader ();
          setup_present_hook ();
          initialized := true);
diff -r 203a9528bf7a -r 916c7fe684e3 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat May 11 21:34:53 2013 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat May 11 22:17:18 2013 +0200
@@ -12,7 +12,7 @@
   val new_thms_deps: theory -> theory -> string list * string list
   val init_pgip: bool -> unit             (* main PGIP loop with true; fail with false *)
 
-  val pgip_channel_emacs: (string -> unit) -> unit
+  val init_pgip_session_id: unit -> unit
 
   (* More message functions... *)
   val nonfatal_error : string -> unit     (* recoverable (batch) error: carry on scripting *)
@@ -1018,9 +1018,9 @@
 
 local
 
-val pgip_output_channel = Unsynchronized.ref Output.physical_writeln
+fun invalid_pgip () = raise PGIP "Invalid PGIP packet received";
 
-fun invalid_pgip () = raise PGIP "Invalid PGIP packet received";
+fun output_emacs pgips = Output.urgent_message (output_pgips pgips);
 
 fun process_element_emacs (XML.Elem (("askprefs", _), _)) =
       let
@@ -1028,7 +1028,7 @@
           {name = name, descr = SOME descr, default = SOME default, pgiptype = pgiptype};
       in
         ! preferences |> List.app (fn (prefcat, prefs) =>
-            issue_pgip (Hasprefs {prefcategory = SOME prefcat, prefs = map preference_of prefs}))
+            output_emacs [Hasprefs {prefcategory = SOME prefcat, prefs = map preference_of prefs}])
       end
   | process_element_emacs (XML.Elem (("setpref", attrs), data)) =
       let
@@ -1042,10 +1042,6 @@
 
 in
 
-fun pgip_channel_emacs writefn =
- (init_pgip_session_id ();
-  pgip_output_channel := writefn);
-
 fun process_pgip_emacs str =
   let
     val _ = pgip_refid := NONE;
@@ -1065,7 +1061,7 @@
            if processit then
             (pgip_refid := PgipTypes.get_attr_opt "id" attrs;
              pgip_refseq := SOME seq;
-             List.app process_pgip_element pgips)
+             List.app process_element_emacs pgips)
            else ()
          end
     | _ => invalid_pgip ())
@@ -1077,7 +1073,7 @@
     (Parse.text >>
       (fn str => Toplevel.imperative (fn () =>
         if print_mode_active proof_general_emacsN
-        then Unsynchronized.setmp output_xml_fn (! pgip_output_channel) process_pgip_emacs str
+        then process_pgip_emacs str
         else process_pgip_plain str)));
 
 end;