# HG changeset patch
# User aspinall
# Date 1170159422 -3600
# Node ID c3f5aa951a680ac6d761725fb4bab85a7bd99250
# Parent  ac81ad3436bcdaa8c86afb8a4c17cda53d8d287d
Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).

diff -r ac81ad3436bc -r c3f5aa951a68 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jan 30 13:16:58 2007 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jan 30 13:17:02 2007 +0100
@@ -433,6 +433,16 @@
 end
 
 
+(* Preferences: tweak for PGIP interfaces *)
+
+val preferences = ref Preferences.preferences;
+
+fun setup_preferences_tweak() =
+    preferences :=
+     (* PGIP uses markup for distinguishing variable types *)
+     (!preferences |> Preferences.set_default ("show-question-marks","false")
+	           |> Preferences.remove "show-question-marks");
+		 
 
 
 (* Sending commands to Isar *)
@@ -486,7 +496,7 @@
         List.app (fn (prefcat, prefs) =>
                      issue_pgip (Hasprefs {prefcategory=SOME prefcat,
                                            prefs=map preference_of prefs}))
-                 Preferences.preferences
+                 (!preferences)
     end
 
 fun askconfig (Askconfig vs) = () (* TODO: add config response *)
@@ -495,7 +505,7 @@
     fun lookuppref pref =
         case AList.lookup (op =)
                           (map (fn p => (#name p,p))
-                               (maps snd Preferences.preferences)) pref of
+                               (maps snd (!preferences))) pref of
             NONE => error ("Unknown prover preference: " ^ quote pref)
           | SOME p => p
 in
@@ -583,7 +593,7 @@
          | (NONE, SOME ObjFile)        => setids (idtable ObjFile NONE (ThyInfo.names())) (* ditto *)
          | (SOME fi, SOME ObjFile)     => setids (idtable ObjTheory (SOME fi) [fi]) (* FIXME: lookup file *)
          | (NONE, SOME ObjTheory)      => setids (idtable ObjTheory NONE (ThyInfo.names()))
-         | (SOME thy, SOME ObjTheory)  => setids (idtable ObjTheory (SOME thy) (ThyInfo.get_preds thy))
+         | (SOME thy, SOME ObjTheory)  => setids (idtable ObjTheory (SOME thy) (ThyInfo.get_succs thy))
          | (SOME thy, SOME ObjTheorem) => setids (idtable ObjTheorem (SOME thy) (thms_of_thy thy))
          (* next case is both of above.  FIXME: cleanup this *)
          | (SOME thy, NONE) => (setids (idtable ObjTheory (SOME thy) (ThyInfo.get_preds thy));
@@ -1063,6 +1073,7 @@
       (! initialized orelse
         (setmp warning_fn (K ()) init_outer_syntax ();
           PgipParser.init ();
+	  setup_preferences_tweak ();
           setup_xsymbols_output ();
           setup_pgml_output ();
           setup_messages ();