eliminated obsolete Output.no_warnings, where no warnings were produced anyway;
authorwenzelm
Fri, 27 Aug 2010 20:28:58 +0200
changeset 38833 9ff5ce3580c1
parent 38832 fc0aa40a1b08
child 38834 658fcba35ed7
eliminated obsolete Output.no_warnings, where no warnings were produced anyway;
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Aug 27 20:09:36 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Aug 27 20:28:58 2010 +0200
@@ -234,15 +234,15 @@
   | init true =
       (if ! initialized then ()
        else
-        (Output.no_warnings_CRITICAL init_outer_syntax ();
-          Output.add_mode Symbol.xsymbolsN Symbol.output Output.default_escape;
-          Output.add_mode proof_generalN Output.default_output Output.default_escape;
-          Markup.add_mode proof_generalN YXML.output_markup;
-          setup_messages ();
-          ProofGeneralPgip.init_pgip_channel (! Output.priority_fn);
-          setup_thy_loader ();
-          setup_present_hook ();
-          initialized := true);
+        (init_outer_syntax ();
+         Output.add_mode Symbol.xsymbolsN Symbol.output Output.default_escape;
+         Output.add_mode proof_generalN Output.default_output Output.default_escape;
+         Markup.add_mode proof_generalN YXML.output_markup;
+         setup_messages ();
+         ProofGeneralPgip.init_pgip_channel (! Output.priority_fn);
+         setup_thy_loader ();
+         setup_present_hook ();
+         initialized := true);
        sync_thy_loader ();
        Unsynchronized.change print_mode (update (op =) proof_generalN);
        Secure.PG_setup ();
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Aug 27 20:09:36 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Aug 27 20:28:58 2010 +0200
@@ -802,7 +802,7 @@
       val filepath = PgipTypes.path_of_pgipurl url
       val filedir = Path.dir filepath
       val thy_name = Path.implode o #1 o Path.split_ext o Path.base
-      val openfile_retract = Output.no_warnings_CRITICAL Thy_Info.kill_thy o thy_name;
+      val openfile_retract = Thy_Info.kill_thy o thy_name;
   in
       case !currently_open_file of
           SOME f => raise PGIP ("<openfile> when a file is already open!\nCurrently open file: " ^
@@ -1027,7 +1027,7 @@
          Output.add_mode proof_generalN Output.default_output Output.default_escape;
          Markup.add_mode proof_generalN YXML.output_markup;
          setup_messages ();
-         Output.no_warnings_CRITICAL init_outer_syntax ();
+         init_outer_syntax ();
          setup_thy_loader ();
          setup_present_hook ();
          init_pgip_session_id ();