# HG changeset patch
# User wenzelm
# Date 1167414366 -3600
# Node ID 4dd9a5fc7fc34ba5e622dce7631cdb5b95e7f525
# Parent  e877a5a78522d916165ac6223f37cc5afcf1b0e6
tuned;

diff -r e877a5a78522 -r 4dd9a5fc7fc3 src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Dec 29 18:46:04 2006 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Dec 29 18:46:06 2006 +0100
@@ -18,6 +18,7 @@
 
 structure P = OuterParse;
 
+
 (* print modes *)
 
 val proof_generalN = "ProofGeneralEmacs";  (*token markup (colouring vars, etc.)*)
@@ -138,18 +139,18 @@
   setmp Display.current_goals_markers (special "366", special "367", "") f ();
 
 fun print_current_goals n m st =
-    tmp_markers (fn () => Display.print_current_goals_default n m st);
+  tmp_markers (fn () => Display.print_current_goals_default n m st);
 
 fun print_state b st =
-    tmp_markers (fn () => Toplevel.print_state_default b st);
+  tmp_markers (fn () => Toplevel.print_state_default b st);
 
 in
 
 fun setup_state () =
   (Display.print_current_goals_fn := print_current_goals;
    Toplevel.print_state_fn := print_state;
-   Toplevel.prompt_state_fn := (fn s => suffix (special "372")
-     (Toplevel.prompt_state_default s)));
+   Toplevel.prompt_state_fn :=
+     (fn s => suffix (special "372") (Toplevel.prompt_state_default s)));
 
 end;
 
@@ -311,8 +312,6 @@
 
 val initialized = ref false;
 
-fun set_prompts () = ml_prompts "ML> " "ML# "
-
 fun init false =
       Output.panic "Interface support no longer available for Isabelle/classic mode."
   | init true =
@@ -327,7 +326,7 @@
         set initialized; ()));
       sync_thy_loader ();
       change print_mode (cons proof_generalN o remove (op =) proof_generalN);
-      set_prompts ();
+      ml_prompts "ML> " "ML# ";
       Isar.sync_main ());
 
 fun init_pgip false = init true