# HG changeset patch
# User wenzelm
# Date 1283528624 -7200
# Node ID 12f3788be67be8f146d4dc23e456cb39c76bcf82
# Parent  399977145846687a92668590e5af2aaacc5b1fdc
turned show_all_types into proper configuration option;

diff -r 399977145846 -r 12f3788be67b src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Fri Sep 03 16:36:33 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Fri Sep 03 17:43:44 2010 +0200
@@ -187,43 +187,40 @@
 fun quotename c =
   if Syntax.is_identifier c andalso not (Keyword.is_keyword c) then c else quote c
 
-fun simple_smart_string_of_cterm ct =
+fun simple_smart_string_of_cterm ctxt0 ct =
     let
-        val thy = Thm.theory_of_cterm ct;
+        val ctxt = Config.put show_all_types true ctxt0;
         val {t,T,...} = rep_cterm ct
         (* Hack to avoid parse errors with Trueprop *)
-        val ct  = (cterm_of thy (HOLogic.dest_Trueprop t)
-                           handle TERM _ => ct)
+        val ct  = cterm_of (Thm.theory_of_cterm ct) (HOLogic.dest_Trueprop t)
+                           handle TERM _ => ct
     in
         quote (
         Print_Mode.setmp [] (
         setmp_CRITICAL show_brackets false (
-        setmp_CRITICAL show_all_types true (
         setmp_CRITICAL Syntax.ambiguity_is_error false (
-        setmp_CRITICAL show_sorts true (Syntax.string_of_term_global thy o Thm.term_of)))))
+        setmp_CRITICAL show_sorts true (Syntax.string_of_term ctxt o Thm.term_of))))
         ct)
     end
 
 exception SMART_STRING
 
-fun smart_string_of_cterm ct =
+fun smart_string_of_cterm ctxt ct =
     let
-        val thy = Thm.theory_of_cterm ct
-        val ctxt = ProofContext.init_global thy
         val {t,T,...} = rep_cterm ct
         (* Hack to avoid parse errors with Trueprop *)
-        val ct  = (cterm_of thy (HOLogic.dest_Trueprop t)
-                   handle TERM _ => ct)
+        val ct  = cterm_of (Thm.theory_of_cterm ct) (HOLogic.dest_Trueprop t)
+                   handle TERM _ => ct
         fun match u = t aconv u
-        fun G 0 = setmp_CRITICAL show_types true (setmp_CRITICAL show_sorts true)
-          | G 1 = setmp_CRITICAL show_brackets true (G 0)
-          | G 2 = setmp_CRITICAL show_all_types true (G 0)
-          | G 3 = setmp_CRITICAL show_brackets true (G 2)
-          | G _ = raise SMART_STRING
+        fun G 0 f ctxt x = setmp_CRITICAL show_types true (setmp_CRITICAL show_sorts true) (f ctxt) x
+          | G 1 f ctxt x = setmp_CRITICAL show_brackets true (G 0) f ctxt x
+          | G 2 f ctxt x = G 0 f (Config.put show_all_types true ctxt) x
+          | G 3 f ctxt x = setmp_CRITICAL show_brackets true (G 2) f ctxt x
+          | G _ _ _ _ = raise SMART_STRING
         fun F n =
             let
                 val str =
-                  setmp_CRITICAL show_brackets false (G n (Syntax.string_of_term ctxt o term_of)) ct
+                  setmp_CRITICAL show_brackets false (G n Syntax.string_of_term ctxt) (term_of ct)
                 val u = Syntax.parse_term ctxt str
                   |> Type_Infer.constrain T |> Syntax.check_term ctxt
             in
@@ -233,13 +230,13 @@
             end
             handle ERROR mesg => F (n + 1)
               | SMART_STRING =>
-                  error ("smart_string failed for: "^ G 0 (Syntax.string_of_term ctxt o term_of) ct)
+                  error ("smart_string failed for: "^ G 0 Syntax.string_of_term ctxt (term_of ct))
     in
       Print_Mode.setmp [] (setmp_CRITICAL Syntax.ambiguity_is_error true F) 0
     end
-    handle ERROR mesg => simple_smart_string_of_cterm ct
+    handle ERROR mesg => simple_smart_string_of_cterm ctxt ct
 
-val smart_string_of_thm = smart_string_of_cterm o cprop_of
+fun smart_string_of_thm ctxt = smart_string_of_cterm ctxt o cprop_of
 
 fun prth th = writeln (Print_Mode.setmp [] Display.string_of_thm_without_context th);
 fun prin t = writeln (Print_Mode.setmp []
@@ -366,9 +363,6 @@
 val scan_start_of_tag = $$ #"<" |-- scan_id --
                            repeat ($$ #" " |-- scan_attribute)
 
-(* The evaluation delay introduced through the 'toks' argument is needed
-for the sake of the SML/NJ (110.9.1) compiler.  Either that or an explicit
-type :-( *)
 fun scan_end_of_tag toks = ($$ #"/" |-- $$ #">" |-- succeed []) toks
 
 val scan_end_tag = $$ #"<" |-- $$ #"/" |-- scan_id --| $$ #">"
@@ -1369,11 +1363,13 @@
         val thy' = add_hol4_pending thyname thmname args thy
         val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
         val th = disambiguate_frees th
-        val thy2 = if gen_output
-                   then add_dump ("lemma " ^ (quotename thmname) ^ ": " ^
-                                  (smart_string_of_thm th) ^ "\n  by (import " ^
-                                  thyname ^ " " ^ (quotename thmname) ^ ")") thy'
-                   else thy'
+        val thy2 =
+          if gen_output
+          then
+            add_dump ("lemma " ^ (quotename thmname) ^ ": " ^
+                (smart_string_of_thm (Syntax.init_pretty_global thy') th) ^ "\n  by (import " ^
+                thyname ^ " " ^ (quotename thmname) ^ ")") thy'
+          else thy'
     in
         (thy2,hth')
     end
@@ -1934,21 +1930,25 @@
         val (linfo,tm24) = disamb_term (mk_teq constname rhs' thy'')
         val rew = rewrite_hol4_term eq thy''
         val crhs = cterm_of thy'' (#2 (Logic.dest_equals (prop_of rew)))
-        val thy22 = if Thm.def_name constname = thmname andalso not redeclared andalso csyn = NoSyn
-                    then
-                        let
-                            val p1 = quotename constname
-                            val p2 = Syntax.string_of_typ_global thy'' ctype
-                            val p3 = string_of_mixfix csyn
-                            val p4 = smart_string_of_cterm crhs
-                        in
-                          add_dump ("definition\n  " ^ p1 ^ " :: \"" ^ p2 ^ "\" "^ p3 ^ " where\n  " ^ p4) thy''
-                        end
-                    else
-                        add_dump ("consts\n  " ^ quotename constname ^ " :: \"" ^
-                          Syntax.string_of_typ_global thy'' ctype ^
-                          "\" " ^ string_of_mixfix csyn ^ "\n\ndefs\n  " ^
-                          quotename thmname ^ ": " ^ smart_string_of_cterm crhs) thy''
+        val thy22 =
+          if Thm.def_name constname = thmname andalso not redeclared andalso csyn = NoSyn
+          then
+              let
+                  val ctxt = Syntax.init_pretty_global thy''
+                  val p1 = quotename constname
+                  val p2 = Syntax.string_of_typ ctxt ctype
+                  val p3 = string_of_mixfix csyn
+                  val p4 = smart_string_of_cterm ctxt crhs
+              in
+                add_dump ("definition\n  " ^ p1 ^ " :: \"" ^ p2 ^ "\" "^ p3 ^ " where\n  " ^ p4) thy''
+              end
+          else
+              let val ctxt = Syntax.init_pretty_global thy'' in
+                add_dump ("consts\n  " ^ quotename constname ^ " :: \"" ^
+                  Syntax.string_of_typ ctxt ctype ^
+                  "\" " ^ string_of_mixfix csyn ^ "\n\ndefs\n  " ^
+                  quotename thmname ^ ": " ^ smart_string_of_cterm ctxt crhs) thy''
+              end
         val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of
                       SOME (_,res) => HOLThm(rens_of linfo,res)
                     | NONE => raise ERR "new_definition" "Bad conclusion"
@@ -2043,9 +2043,11 @@
                                             in
                                                 (name'::names,thy')
                                             end) names ([], thy')
-            val thy'' = add_dump ("specification (" ^ (spaces new_names) ^ ") " ^ thmname ^ ": " ^ (smart_string_of_thm th) ^
-                                  "\n  by (import " ^ thyname ^ " " ^ thmname ^ ")")
-                                 thy'
+            val thy'' =
+              add_dump ("specification (" ^ (spaces new_names) ^ ") " ^ thmname ^ ": " ^
+                (smart_string_of_thm (Syntax.init_pretty_global thy') th) ^
+                "\n  by (import " ^ thyname ^ " " ^ thmname ^ ")")
+                thy'
             val _ = message "RESULT:"
             val _ = if_debug pth hth
         in
@@ -2118,9 +2120,10 @@
             val tnames_string = if null tnames
                                 then ""
                                 else "(" ^ commas tnames ^ ") "
-            val proc_prop = if null tnames
-                            then smart_string_of_cterm
-                            else setmp_CRITICAL show_all_types true smart_string_of_cterm
+            val proc_prop =
+              smart_string_of_cterm
+                (Syntax.init_pretty_global thy4
+                  |> not (null tnames) ? Config.put show_all_types true)
             val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " "
                                  ^ (string_of_mixfix tsyn) ^ "\n  by (rule typedef_helper,import " ^ thyname ^ " " ^ thmname ^ ")") thy4
 
@@ -2201,9 +2204,10 @@
             val tnames_string = if null tnames
                                 then ""
                                 else "(" ^ commas tnames ^ ") "
-            val proc_prop = if null tnames
-                            then smart_string_of_cterm
-                            else setmp_CRITICAL show_all_types true smart_string_of_cterm
+            val proc_prop =
+              smart_string_of_cterm
+                (Syntax.init_pretty_global thy4
+                  |> not (null tnames) ? Config.put show_all_types true)
             val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^
               " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " ^
               (string_of_mixfix tsyn) ^ " morphisms "^
diff -r 399977145846 -r 12f3788be67b src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Sep 03 16:36:33 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Sep 03 17:43:44 2010 +0200
@@ -949,7 +949,7 @@
                                    T T' (rep_of name)
       in
         Pretty.block (Pretty.breaks
-            [setmp_show_all_types (Syntax.pretty_term ctxt) t1,
+            [Syntax.pretty_term (set_show_all_types ctxt) t1,
              Pretty.str oper, Syntax.pretty_term ctxt t2])
       end
     fun pretty_for_datatype ({typ, card, complete, ...} : datatype_spec) =
diff -r 399977145846 -r 12f3788be67b src/HOL/Tools/Nitpick/nitpick_scope.ML
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Fri Sep 03 16:36:33 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Fri Sep 03 17:43:44 2010 +0200
@@ -142,9 +142,10 @@
    handle TYPE ("Nitpick_HOL.card_of_type", _, _) => ~1, offset_of_type ofs T)
 
 fun quintuple_for_scope code_type code_term code_string
-        ({hol_ctxt = {ctxt, stds, ...}, card_assigns, bits, bisim_depth,
+        ({hol_ctxt = {ctxt = ctxt0, stds, ...}, card_assigns, bits, bisim_depth,
          datatypes, ...} : scope) =
   let
+    val ctxt = set_show_all_types ctxt0
     val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
                      @{typ bisim_iterator}]
     val (iter_assigns, card_assigns) =
@@ -175,9 +176,8 @@
       (if bisim_depth < 0 andalso forall (not o #co) datatypes then []
        else [code_string ("bisim_depth = " ^ signed_string_of_int bisim_depth)])
   in
-    setmp_show_all_types
-        (fn () => (cards primary_card_assigns, cards secondary_card_assigns,
-                   maxes (), iters (), miscs ())) ()
+    (cards primary_card_assigns, cards secondary_card_assigns,
+     maxes (), iters (), miscs ())
   end
 
 fun pretties_for_scope scope verbose =
diff -r 399977145846 -r 12f3788be67b src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri Sep 03 16:36:33 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri Sep 03 17:43:44 2010 +0200
@@ -71,7 +71,7 @@
   val eta_expand : typ list -> term -> int -> term
   val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
   val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
-  val setmp_show_all_types : ('a -> 'b) -> 'a -> 'b
+  val set_show_all_types : Proof.context -> Proof.context
   val indent_size : int
   val pstrs : string -> Pretty.T list
   val unyxml : string -> string
@@ -279,9 +279,9 @@
 fun DETERM_TIMEOUT delay tac st =
   Seq.of_list (the_list (time_limit delay (fn () => SINGLE tac st) ()))
 
-fun setmp_show_all_types f =
-  setmp_CRITICAL show_all_types
-                 (!show_types orelse !show_sorts orelse !show_all_types) f
+fun set_show_all_types ctxt =
+  Config.put show_all_types
+    (!show_types orelse !show_sorts orelse Config.get ctxt show_all_types) ctxt
 
 val indent_size = 2
 
diff -r 399977145846 -r 12f3788be67b src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Fri Sep 03 16:36:33 2010 +0200
+++ b/src/Pure/Syntax/printer.ML	Fri Sep 03 17:43:44 2010 +0200
@@ -10,7 +10,7 @@
   val show_sorts: bool Unsynchronized.ref
   val show_types: bool Unsynchronized.ref
   val show_free_types: bool Config.T
-  val show_all_types: bool Unsynchronized.ref
+  val show_all_types: bool Config.T
   val show_structs: bool Unsynchronized.ref
   val show_question_marks_default: bool Unsynchronized.ref
   val show_question_marks_value: Config.value Config.T
@@ -51,11 +51,10 @@
 val show_types = Unsynchronized.ref false;
 val show_sorts = Unsynchronized.ref false;
 val show_brackets = Unsynchronized.ref false;
-val show_all_types = Unsynchronized.ref false;
+val show_free_types = Config.bool (Config.declare "show_free_types" (fn _ => Config.Bool true));
+val show_all_types = Config.bool (Config.declare "show_all_types" (fn _ => Config.Bool false));
 val show_structs = Unsynchronized.ref false;
 
-val show_free_types = Config.bool (Config.declare "show_free_types" (fn _ => Config.Bool true));
-
 val show_question_marks_default = Unsynchronized.ref true;
 val show_question_marks_value =
   Config.declare "show_question_marks" (fn _ => Config.Bool (! show_question_marks_default));
@@ -120,10 +119,11 @@
 
 (** term_to_ast **)
 
-fun ast_of_term idents consts ctxt trf
-    show_all_types show_types show_sorts show_structs tm =
+fun ast_of_term idents consts ctxt trf show_types show_sorts show_structs tm =
   let
     val show_free_types = Config.get ctxt show_free_types;
+    val show_all_types = Config.get ctxt show_all_types;
+
     val {structs, fixes} = idents;
 
     fun mark_atoms ((t as Const (c, T)) $ u) =
@@ -201,8 +201,9 @@
   end;
 
 fun term_to_ast idents consts ctxt trf tm =
-  ast_of_term idents consts ctxt trf (! show_all_types)
-    (! show_types orelse ! show_sorts orelse ! show_all_types) (! show_sorts) (! show_structs) tm;
+  ast_of_term idents consts ctxt trf
+    (! show_types orelse ! show_sorts orelse Config.get ctxt show_all_types)
+    (! show_sorts) (! show_structs) tm;
 
 
 
diff -r 399977145846 -r 12f3788be67b src/Pure/goal_display.ML
--- a/src/Pure/goal_display.ML	Fri Sep 03 16:36:33 2010 +0200
+++ b/src/Pure/goal_display.ML	Fri Sep 03 17:43:44 2010 +0200
@@ -65,6 +65,7 @@
 fun pretty_goals ctxt0 {total, main, maxgoals} state =
   let
     val ctxt = Config.put show_free_types false ctxt0;
+    val show_all_types = Config.get ctxt show_all_types;
 
     val prt_sort = Syntax.pretty_sort ctxt;
     val prt_typ = Syntax.pretty_typ ctxt;
@@ -116,9 +117,9 @@
       (if types then pretty_vars prop else []) @
       (if sorts then pretty_varsT prop else []);
   in
-    setmp_CRITICAL show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
+    setmp_CRITICAL show_types (! show_types orelse ! show_sorts orelse show_all_types)
       (setmp_CRITICAL show_sorts false pretty_gs)
-   (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
+   (! show_types orelse ! show_sorts orelse show_all_types, ! show_sorts)
   end;
 
 fun pretty_goals_without_context n th =