--- 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 ();