more basic print mode "ProofGeneral" (again);
authorwenzelm
Wed, 15 May 2013 21:02:13 +0200
changeset 52013 ebb119a9f712
parent 52012 9ebf2da69b29
child 52014 45929e0e1d73
more basic print mode "ProofGeneral" (again);
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