Re: [isabelle] PG/Isabelle: Problem with Auto-Trace options (with workaround)



Am 19.09.2012 15:49, schrieb Makarius:
> On Wed, 19 Sep 2012, René Neumann wrote:
> 
>>> Now in PG 4.1 with GNU Emacs 23.x it seems that it never works: I see
>>> only the initial askprefs by the prover, without any readjustments by
>>> PG. This means that more basic things like quick-and-dirty also don't
>>> work, i.e. it is off (the usual default of Isabelle), but Proof General
>>> displays it as on, while leaving it de-facto off.
>>
>> So in essence Isabelle states some setting being defaulted to, but
>> relies on an explicit message to actually set it to this default? And PG
>> 4.x does not send this message anymore?
> 
> I don't know for sure.  This part of PGIP is due to David Aspinall, both
> the older and newer behaviour.
> 
> 
>     Makarius

Ok - I skimmed the sources in Isabelle. And as far as I see it, the
defaults of boolean preferences are the actual values of the variables.
Hence this should be ok. BUT: Some preferences are set in an
Unsynchronized.setmp block which cancels this assumption.

So probably the easiest solution would be to just cycle through the
preferences on PG-startup and set them explicitly to their default.

This I did in the attached patch and it fixes the issue :). It is
probably saner to actually ensure defaults are set, instead of relying
on the other side to explicitly set them.

- René

P.S.: I'm not sure, whether the call of 'enforce_preference_defaults' is
actually at the right place in the whole startup process. So it probably
needs to be moved around.
-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055
diff -r 4e4bdd12280f src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Sep 20 06:48:37 2012 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Sep 20 10:14:09 2012 +0200
@@ -240,6 +240,7 @@
          ProofGeneralPgip.pgip_channel_emacs (! Output.Private_Hooks.urgent_message_fn);
          setup_thy_loader ();
          setup_present_hook ();
+         ProofGeneralPgip.enforce_preference_defaults ();
          initialized := true);
        sync_thy_loader ();
        Unsynchronized.change print_mode (update (op =) ProofGeneralPgip.proof_general_emacsN);
diff -r 4e4bdd12280f src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Sep 20 06:48:37 2012 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Sep 20 10:14:09 2012 +0200
@@ -21,6 +21,7 @@
 
   val get_currently_open_file : unit -> Path.T option  (* interface focus *)
   val add_preference: string -> Preferences.preference -> unit
+  val enforce_preference_defaults : unit -> unit
 end
 
 structure ProofGeneralPgip : PROOF_GENERAL_PGIP =
@@ -377,6 +378,13 @@
     Preferences.remove "theorem-dependencies" #>  (* set internally *)
     Preferences.remove "full-proofs"));           (* set internally *)
 
+fun enforce_preference_defaults () =
+  let
+    fun set_pre { name, descr, default, pgiptype, get, set } =
+      set default
+    in
+      List.app (fn (_, prefs) => List.app set_pre prefs) (!preferences)
+  end
 
 
 (* Sending commands to Isar *)
@@ -1001,6 +1009,7 @@
          setup_thy_loader ();
          setup_present_hook ();
          init_pgip_session_id ();
+         enforce_preference_defaults ();
          welcome ();
          initialized := true);
        sync_thy_loader ();


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.