tuned;
authorwenzelm
Fri Dec 29 18:46:06 2006 +0100 (2006-12-29)
changeset 219454dd9a5fc7fc3
parent 21944 e877a5a78522
child 21946 78e018d1f845
tuned;
src/Pure/ProofGeneral/proof_general_emacs.ML
     1.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Dec 29 18:46:04 2006 +0100
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Dec 29 18:46:06 2006 +0100
     1.3 @@ -18,6 +18,7 @@
     1.4  
     1.5  structure P = OuterParse;
     1.6  
     1.7 +
     1.8  (* print modes *)
     1.9  
    1.10  val proof_generalN = "ProofGeneralEmacs";  (*token markup (colouring vars, etc.)*)
    1.11 @@ -138,18 +139,18 @@
    1.12    setmp Display.current_goals_markers (special "366", special "367", "") f ();
    1.13  
    1.14  fun print_current_goals n m st =
    1.15 -    tmp_markers (fn () => Display.print_current_goals_default n m st);
    1.16 +  tmp_markers (fn () => Display.print_current_goals_default n m st);
    1.17  
    1.18  fun print_state b st =
    1.19 -    tmp_markers (fn () => Toplevel.print_state_default b st);
    1.20 +  tmp_markers (fn () => Toplevel.print_state_default b st);
    1.21  
    1.22  in
    1.23  
    1.24  fun setup_state () =
    1.25    (Display.print_current_goals_fn := print_current_goals;
    1.26     Toplevel.print_state_fn := print_state;
    1.27 -   Toplevel.prompt_state_fn := (fn s => suffix (special "372")
    1.28 -     (Toplevel.prompt_state_default s)));
    1.29 +   Toplevel.prompt_state_fn :=
    1.30 +     (fn s => suffix (special "372") (Toplevel.prompt_state_default s)));
    1.31  
    1.32  end;
    1.33  
    1.34 @@ -311,8 +312,6 @@
    1.35  
    1.36  val initialized = ref false;
    1.37  
    1.38 -fun set_prompts () = ml_prompts "ML> " "ML# "
    1.39 -
    1.40  fun init false =
    1.41        Output.panic "Interface support no longer available for Isabelle/classic mode."
    1.42    | init true =
    1.43 @@ -327,7 +326,7 @@
    1.44          set initialized; ()));
    1.45        sync_thy_loader ();
    1.46        change print_mode (cons proof_generalN o remove (op =) proof_generalN);
    1.47 -      set_prompts ();
    1.48 +      ml_prompts "ML> " "ML# ";
    1.49        Isar.sync_main ());
    1.50  
    1.51  fun init_pgip false = init true