1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Oct 14 15:16:12 2008 +0200
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Oct 14 15:16:13 2008 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4    val error_with_pos : PgipTypes.displayarea -> PgipTypes.fatality -> Position.T -> string -> unit
     1.5  
     1.6    val get_currently_open_file : unit -> Path.T option  (* interface focus *)
     1.7 -  val add_preference: string -> Preferences.isa_preference -> unit
     1.8 +  val add_preference: string -> Preferences.preference -> unit
     1.9  end
    1.10  
    1.11  structure ProofGeneralPgip : PROOF_GENERAL_PGIP =
    1.12 @@ -366,17 +366,17 @@
    1.13  
    1.14  (* Preferences: tweak for PGIP interfaces *)
    1.15  
    1.16 -val preferences = ref Preferences.preferences;
    1.17 +val preferences = ref Preferences.pure_preferences;
    1.18  
    1.19  fun add_preference cat pref =
    1.20 -    preferences := Preferences.add cat pref (!preferences);
    1.21 +  CRITICAL (fn () => change preferences (Preferences.add cat pref));
    1.22  
    1.23 -fun setup_preferences_tweak() =
    1.24 -    preferences :=
    1.25 -     (!preferences |> Preferences.set_default ("show-question-marks","false")
    1.26 -                   |> Preferences.remove "show-question-marks"    (* we use markup, not ?s *)
    1.27 -                   |> Preferences.remove "theorem-dependencies"   (* set internally *)
    1.28 -                   |> Preferences.remove "full-proofs")           (* set internally *)
    1.29 +fun setup_preferences_tweak () =
    1.30 +  CRITICAL (fn () => change preferences
    1.31 +   (Preferences.set_default ("show-question-marks", "false") #>
    1.32 +    Preferences.remove "show-question-marks" #>   (* we use markup, not ?s *)
    1.33 +    Preferences.remove "theorem-dependencies" #>  (* set internally *)
    1.34 +    Preferences.remove "full-proofs"));           (* set internally *)
    1.35  
    1.36  
    1.37