Init outer syntax after message setup to avoid spurious output.
authoraspinall
Mon, 19 Nov 2007 13:42:09 +0100
changeset 25445 01f3686f4304
parent 25444 270242f7a27d
child 25446 c1be3072ea8f
Init outer syntax after message setup to avoid spurious output.
src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Nov 19 12:06:10 2007 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Nov 19 13:42:09 2007 +0100
@@ -1139,15 +1139,15 @@
 fun init_pgip false = panic "No Proof General interface support for Isabelle/classic mode."
   | init_pgip true =
       (! initialized orelse
-        (Output.no_warnings init_outer_syntax ();
-          setup_preferences_tweak ();
-          setup_proofgeneral_output ();
-          setup_messages ();
-          setup_thy_loader ();
-          setup_present_hook ();
-          init_pgip_session_id ();
-          welcome ();
-          set initialized);
+        (setup_preferences_tweak ();
+         setup_proofgeneral_output ();
+         setup_messages ();
+         Output.no_warnings init_outer_syntax ();
+         setup_thy_loader ();
+         setup_present_hook ();
+         init_pgip_session_id ();
+         welcome ();
+         set initialized);
         sync_thy_loader ();
        change print_mode (cons proof_generalN o remove (op =) proof_generalN);
        pgip_toplevel tty_src);