--- 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 "^
--- 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) =
--- 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 =
--- 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
--- 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;
--- 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 =