# HG changeset patch
# User wenzelm
# Date 1368644533 -7200
# Node ID ebb119a9f7122f5fc71ed20a2e9162ca13d46825
# Parent  9ebf2da69b293689a6bfdd3a91525022c9d573d0
more basic print mode "ProofGeneral" (again);

diff -r 9ebf2da69b29 -r ebb119a9f712 src/Pure/Tools/proof_general.ML
--- a/src/Pure/Tools/proof_general.ML	Wed May 15 20:53:42 2013 +0200
+++ b/src/Pure/Tools/proof_general.ML	Wed May 15 21:02:13 2013 +0200
@@ -27,6 +27,7 @@
   val preference_option: category -> string -> string -> string -> unit
   structure ThyLoad: sig val add_path: string -> unit end
   val thm_deps: bool Unsynchronized.ref
+  val proof_generalN: string
   val init: unit -> unit
 end;
 
@@ -393,7 +394,7 @@
 
 (* init *)
 
-val proof_general_emacsN = "ProofGeneralEmacs";
+val proof_generalN = "ProofGeneral";
 
 val initialized = Unsynchronized.ref false;
 
@@ -401,15 +402,14 @@
   (if ! initialized then ()
    else
     (Output.add_mode Symbol.xsymbolsN Symbol.output Output.default_escape;
-     Output.add_mode proof_general_emacsN
-      Output.default_output Output.default_escape;
-     Markup.add_mode proof_general_emacsN YXML.output_markup;
+     Output.add_mode proof_generalN Output.default_output Output.default_escape;
+     Markup.add_mode proof_generalN YXML.output_markup;
      setup_messages ();
      setup_thy_loader ();
      setup_present_hook ();
      initialized := true);
    sync_thy_loader ();
-   Unsynchronized.change print_mode (update (op =) proof_general_emacsN);
+   Unsynchronized.change print_mode (update (op =) proof_generalN);
    Secure.PG_setup ();
    welcome ();
    Isar.toplevel_loop TextIO.stdIn