src/Pure/ProofGeneral/proof_general_pgip.ML

   val nonfatal_error : string -> unit     (* recoverable (batch) error: carry on scripting *)
   val log_msg : string -> unit            (* for internal log messages *)
   val error_with_pos : PgipTypes.displayarea -> PgipTypes.fatality -> Position.T -> string -> unit
 
   val get_currently_open_file : unit -> Path.T option  (* interface focus *)
-  val add_preference: string -> Preferences.isa_preference -> unit
+  val add_preference: string -> Preferences.preference -> unit
 end
 
 structure ProofGeneralPgip : PROOF_GENERAL_PGIP =
 struct
 

 end
 
 
 (* Preferences: tweak for PGIP interfaces *)
 
-val preferences = ref Preferences.preferences;
+val preferences = ref Preferences.pure_preferences;
 
 fun add_preference cat pref =
-    preferences := Preferences.add cat pref (!preferences);
-
-fun setup_preferences_tweak() =
-    preferences :=
-     (!preferences |> Preferences.set_default ("show-question-marks","false")
-                   |> Preferences.remove "show-question-marks"    (* we use markup, not ?s *)
-                   |> Preferences.remove "theorem-dependencies"   (* set internally *)
-                   |> Preferences.remove "full-proofs")           (* set internally *)
+  CRITICAL (fn () => change preferences (Preferences.add cat pref));
+
+fun setup_preferences_tweak () =
+  CRITICAL (fn () => change preferences
+   (Preferences.set_default ("show-question-marks", "false") #>
+    Preferences.remove "show-question-marks" #>   (* we use markup, not ?s *)
+    Preferences.remove "theorem-dependencies" #>  (* set internally *)
+    Preferences.remove "full-proofs"));           (* set internally *)
 
 
 
 (* Sending commands to Isar *)