# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1261516248 -3600
# Node ID 54f186bb5e3e50d43528c15e36cf884c8a3f41bb
# Parent  2f72662d21f350198f9f2936cd03a86f1ec70e8a
added "Highest Priority" category; and tuned slightly code

diff -r 2f72662d21f3 -r 54f186bb5e3e FIXME-TODO
--- a/FIXME-TODO	Tue Dec 22 21:44:50 2009 +0100
+++ b/FIXME-TODO	Tue Dec 22 22:10:48 2009 +0100
@@ -1,8 +1,30 @@
+Highest Priority
+================
+
+- better lookup mechanism for quotient definition
+  (see fixme in quotient_term.ML)
+
+- check needs to be fixed in mk_resp_arg (quotient_term.ML),
+  see test for (_, Const _)
+
+- clever code in quotiet_tacs.ML needs to be turned into
+  boring code
+
+- comment about regularize tactic eeds to be adapted
+
+- Check all the places where we do "handle _"
+  (They make code changes very difficult: I sat 1/2
+  a day over simplification of calculate_inst before
+  I understood things; the reason was that my exceptions
+  where caught by the catch all. There is no problem
+  with throwing and handling exceptions...it just must
+  be clear who throws what ad what is thrown.)
+
 Higher Priority
 ===============
 
 - if the constant definition gives the wrong definition
-  term, one gets a cryptic message about get_fun
+  term, one gets a cryptic message about absrep_fun
 
 - have FSet.thy to have a simple infrastructure for 
   finite sets (syntax should be \<lbrace> \<rbrace>,
@@ -15,7 +37,7 @@
 - user should be able to give quotient_respects and 
   preserves theorems in a more natural form.
 
-- the test in the (_, Const _) needs to be fixed
+
 
 Lower Priority
 ==============
@@ -24,7 +46,7 @@
   a proof of the respectfulness (in this way one
   already excludes non-sensical definitions)
 
-- accept partial equvalence relations
+- accept partial equivalence relations
 
 - think about what happens if things go wrong (like
   theorem cannot be lifted) / proper diagnostic 
@@ -46,9 +68,6 @@
 
 - add tests for adding theorems to the various thm lists
 
-
-- Check all the places where we do "handle _"
-
 - We shouldn't use the command 'quotient' as this shadows Larry's quotient.
   Call it 'quotient_type'
 
diff -r 2f72662d21f3 -r 54f186bb5e3e Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Tue Dec 22 21:44:50 2009 +0100
+++ b/Quot/quotient_info.ML	Tue Dec 22 22:10:48 2009 +0100
@@ -90,12 +90,10 @@
 let
   fun prt_map (ty_name, {mapfun, relfun}) = 
       Pretty.block (Library.separate (Pretty.brk 2)
-          [Pretty.str "type:", 
-           Pretty.str ty_name,
-           Pretty.str "map fun:", 
-           Pretty.str mapfun,
-           Pretty.str "relation map:", 
-           Pretty.str relfun])
+        (map Pretty.str 
+          ["type:", ty_name,
+           "map fun:", mapfun,
+           "relation map:", relfun]))
 in
   MapsData.get (ProofContext.theory_of ctxt)
   |> Symtab.dest
@@ -104,11 +102,7 @@
   |> Pretty.writeln
 end
 
-val _ = 
-  OuterSyntax.improper_command "print_maps" "prints out all map functions" 
-    OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_mapsinfo o Toplevel.context_of)))
-
-
+ 
 (* info about quotient types *)
 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
 
@@ -152,10 +146,6 @@
   |> Pretty.writeln
 end
 
-val _ = 
-  OuterSyntax.improper_command "print_quotients" "prints out all quotients" 
-    OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of)))
-
 
 (* info about quotient constants *)
 type qconsts_info = {qconst: term, rconst: term, def: thm}
@@ -212,10 +202,6 @@
   |> Pretty.writeln
 end
 
-val _ = 
-  OuterSyntax.improper_command "print_quotconsts" "prints out all quotient constants" 
-    OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of)))
-
 (* FIXME/TODO: check the various lemmas conform *)
 (* with the required shape                      *)
 
@@ -257,6 +243,7 @@
 val quotient_rules_add = QuotientRules.add
 
 (* setup of the theorem lists *)
+
 val _ = Context.>> (Context.map_theory 
     (EquivRules.setup #>
      RspRules.setup #>
@@ -264,5 +251,18 @@
      IdSimps.setup #>
      QuotientRules.setup))
 
+
+(* setup of the printing commands *)
+
+fun improper_command (pp_fn, cmd_name, descr_str) =  
+  OuterSyntax.improper_command cmd_name descr_str 
+    OuterKeyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of)))
+
+val _ = map improper_command 
+         [(print_mapsinfo, "print_maps", "prints out all map functions"),
+          (print_quotinfo, "print_quotients", "prints out all quotients"), 
+          (print_qconstinfo, "print_quotconsts", "prints out all quotient constants")]
+
+
 end; (* structure *)