--- a/NEWS Mon Sep 06 11:53:42 2010 +0200
+++ b/NEWS Mon Sep 06 12:38:45 2010 +0200
@@ -31,6 +31,9 @@
ML (Config.T) Isar (attribute)
eta_contract eta_contract
+ show_brackets show_brackets
+ show_sorts show_sorts
+ show_types show_types
show_question_marks show_question_marks
show_consts show_consts
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Mon Sep 06 11:53:42 2010 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Mon Sep 06 12:38:45 2010 +0200
@@ -96,13 +96,13 @@
text {*
\begin{mldecls}
- @{index_ML show_types: "bool Unsynchronized.ref"} & default @{ML false} \\
- @{index_ML show_sorts: "bool Unsynchronized.ref"} & default @{ML false} \\
+ @{index_ML show_types: "bool Config.T"} & default @{ML false} \\
+ @{index_ML show_sorts: "bool Config.T"} & default @{ML false} \\
@{index_ML show_consts: "bool Config.T"} & default @{ML false} \\
@{index_ML long_names: "bool Unsynchronized.ref"} & default @{ML false} \\
@{index_ML short_names: "bool Unsynchronized.ref"} & default @{ML false} \\
@{index_ML unique_names: "bool Unsynchronized.ref"} & default @{ML true} \\
- @{index_ML show_brackets: "bool Unsynchronized.ref"} & default @{ML false} \\
+ @{index_ML show_brackets: "bool Config.T"} & default @{ML false} \\
@{index_ML eta_contract: "bool Config.T"} & default @{ML true} \\
@{index_ML Goal_Display.goals_limit: "int Config.T"} & default @{ML 10} \\
@{index_ML Goal_Display.show_main_goal: "bool Config.T"} & default @{ML false} \\
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Mon Sep 06 11:53:42 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Mon Sep 06 12:38:45 2010 +0200
@@ -118,13 +118,13 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexdef{}{ML}{show\_types}\verb|show_types: bool Unsynchronized.ref| & default \verb|false| \\
- \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Unsynchronized.ref| & default \verb|false| \\
+ \indexdef{}{ML}{show\_types}\verb|show_types: bool Config.T| & default \verb|false| \\
+ \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Config.T| & default \verb|false| \\
\indexdef{}{ML}{show\_consts}\verb|show_consts: bool Config.T| & default \verb|false| \\
\indexdef{}{ML}{long\_names}\verb|long_names: bool Unsynchronized.ref| & default \verb|false| \\
\indexdef{}{ML}{short\_names}\verb|short_names: bool Unsynchronized.ref| & default \verb|false| \\
\indexdef{}{ML}{unique\_names}\verb|unique_names: bool Unsynchronized.ref| & default \verb|true| \\
- \indexdef{}{ML}{show\_brackets}\verb|show_brackets: bool Unsynchronized.ref| & default \verb|false| \\
+ \indexdef{}{ML}{show\_brackets}\verb|show_brackets: bool Config.T| & default \verb|false| \\
\indexdef{}{ML}{eta\_contract}\verb|eta_contract: bool Config.T| & default \verb|true| \\
\indexdef{}{ML}{Goal\_Display.goals\_limit}\verb|Goal_Display.goals_limit: int Config.T| & default \verb|10| \\
\indexdef{}{ML}{Goal\_Display.show\_main\_goal}\verb|Goal_Display.show_main_goal: bool Config.T| & default \verb|false| \\
--- a/src/HOL/Groups.thy Mon Sep 06 11:53:42 2010 +0200
+++ b/src/HOL/Groups.thy Mon Sep 06 12:38:45 2010 +0200
@@ -124,11 +124,11 @@
simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
-typed_print_translation {*
+typed_print_translation (advanced) {*
let
- fun tr' c = (c, fn show_sorts => fn T => fn ts =>
- if (not o null) ts orelse T = dummyT
- orelse not (! show_types) andalso can Term.dest_Type T
+ fun tr' c = (c, fn ctxt => fn show_sorts => fn T => fn ts =>
+ if not (null ts) orelse T = dummyT
+ orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T
then raise Match
else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
--- a/src/HOL/Import/proof_kernel.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML Mon Sep 06 12:38:45 2010 +0200
@@ -190,18 +190,16 @@
fun simple_smart_string_of_cterm ctxt0 ct =
let
val ctxt = ctxt0
+ |> Config.put show_brackets false
|> Config.put show_all_types true
+ |> Config.put show_sorts true
|> Config.put Syntax.ambiguity_enabled true;
val {t,T,...} = rep_cterm ct
(* Hack to avoid parse errors with Trueprop *)
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_sorts true (Syntax.string_of_term ctxt o Thm.term_of)))
- ct)
+ quote (Print_Mode.setmp [] (Syntax.string_of_term ctxt o Thm.term_of) ct)
end
exception SMART_STRING
@@ -214,15 +212,15 @@
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 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
+ fun G 0 f ctxt x = f (Config.put show_types true (Config.put show_sorts true ctxt)) x
+ | G 1 f ctxt x = G 0 f (Config.put show_brackets true 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 3 f ctxt x = G 2 f (Config.put show_brackets true ctxt) x
| G _ _ _ _ = raise SMART_STRING
fun F n =
let
val str =
- setmp_CRITICAL show_brackets false (G n Syntax.string_of_term ctxt) (term_of ct)
+ G n Syntax.string_of_term (Config.put show_brackets false ctxt) (term_of ct)
val u = Syntax.parse_term ctxt str
|> Type_Infer.constrain T |> Syntax.check_term ctxt
in
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Mon Sep 06 12:38:45 2010 +0200
@@ -315,7 +315,6 @@
(* (theory -> thm -> bool -> term list -> mtd list -> 'a) -> theory -> mtd list -> thm -> 'a *)
fun mutate_theorem create_entry thy mtds thm =
let
- val pp = Syntax.pp_global thy
val exec = is_executable_thm thy thm
val _ = priority (if exec then "EXEC" else "NOEXEC")
val mutants =
@@ -343,7 +342,7 @@
|> map Mutabelle.freeze |> map freezeT
(* |> filter (not o is_forbidden_mutant) *)
|> List.mapPartial (try (Sign.cert_term thy))
- val _ = map (fn t => priority ("MUTANT: " ^ Pretty.string_of (Pretty.term pp t))) mutants
+ val _ = map (fn t => priority ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
in
create_entry thy thm exec mutants mtds
end
--- a/src/HOL/Statespace/state_space.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML Mon Sep 06 12:38:45 2010 +0200
@@ -439,8 +439,8 @@
in Context.mapping I upd_prf ctxt end;
fun string_of_typ T =
- setmp_CRITICAL show_sorts true
- (Print_Mode.setmp [] (Syntax.string_of_typ (ProofContext.init_global thy))) T;
+ Print_Mode.setmp []
+ (Syntax.string_of_typ (Config.put show_sorts true (Syntax.init_pretty_global thy))) T;
val fixestate = (case state_type of
NONE => []
| SOME s =>
--- a/src/HOL/Tools/Function/function_common.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/HOL/Tools/Function/function_common.ML Mon Sep 06 12:38:45 2010 +0200
@@ -288,7 +288,7 @@
Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
orelse error (cat_lines
["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
- setmp_CRITICAL show_sorts true (Syntax.string_of_typ ctxt) fT])
+ Syntax.string_of_typ (Config.put show_sorts true ctxt) fT])
val _ = map check_sorts fixes
in
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Sep 06 12:38:45 2010 +0200
@@ -281,7 +281,8 @@
fun set_show_all_types ctxt =
Config.put show_all_types
- (!show_types orelse !show_sorts orelse Config.get ctxt show_all_types) ctxt
+ (Config.get ctxt show_types orelse Config.get ctxt show_sorts
+ orelse Config.get ctxt show_all_types) ctxt
val indent_size = 2
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Sep 06 12:38:45 2010 +0200
@@ -947,11 +947,12 @@
fun string_for_proof ctxt0 full_types i n =
let
- val ctxt = Config.put show_free_types false ctxt0
+ val ctxt = ctxt0
+ |> Config.put show_free_types false
+ |> Config.put show_types true
fun fix_print_mode f x =
- setmp_CRITICAL show_types true
- (Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
- (print_mode_value ())) f) x
+ Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
+ (print_mode_value ())) f x
fun do_indent ind = replicate_string (ind * indent_size) " "
fun do_free (s, T) =
maybe_quote s ^ " :: " ^
--- a/src/HOL/Tools/numeral_syntax.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML Mon Sep 06 12:38:45 2010 +0200
@@ -69,15 +69,15 @@
in
-fun numeral_tr' show_sorts (*"number_of"*) (Type (@{type_name fun}, [_, T])) (t :: ts) =
+fun numeral_tr' ctxt show_sorts (*"number_of"*) (Type (@{type_name fun}, [_, T])) (t :: ts) =
let val t' =
- if not (! show_types) andalso can Term.dest_Type T then syntax_numeral t
+ if not (Config.get ctxt show_types) andalso can Term.dest_Type T then syntax_numeral t
else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T
in list_comb (t', ts) end
- | numeral_tr' _ (*"number_of"*) T (t :: ts) =
+ | numeral_tr' _ _ (*"number_of"*) T (t :: ts) =
if T = dummyT then list_comb (syntax_numeral t, ts)
else raise Match
- | numeral_tr' _ (*"number_of"*) _ _ = raise Match;
+ | numeral_tr' _ _ (*"number_of"*) _ _ = raise Match;
end;
@@ -86,6 +86,6 @@
val setup =
Sign.add_trfuns ([], [(@{syntax_const "_Numeral"}, numeral_tr)], [], []) #>
- Sign.add_trfunsT [(@{const_syntax Int.number_of}, numeral_tr')];
+ Sign.add_advanced_trfunsT [(@{const_syntax Int.number_of}, numeral_tr')];
end;
--- a/src/HOL/Tools/record.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/HOL/Tools/record.ML Mon Sep 06 12:38:45 2010 +0200
@@ -699,9 +699,9 @@
val subst = Type.raw_matches (vartypes, argtypes) Vartab.empty
handle Type.TYPE_MATCH => err "type is no proper record (extension)";
+ val term_of_typ = Syntax.term_of_typ (Config.get ctxt show_sorts);
val alphas' =
- map (Syntax.term_of_typ (! Syntax.show_sorts) o Envir.norm_type subst o varifyT)
- (but_last alphas);
+ map (term_of_typ o Envir.norm_type subst o varifyT) (but_last alphas);
val more' = mk_ext rest;
in
@@ -810,7 +810,7 @@
val T = decode_type thy t;
val varifyT = varifyT (Term.maxidx_of_typ T);
- val term_of_type = Syntax.term_of_typ (! Syntax.show_sorts);
+ val term_of_type = Syntax.term_of_typ (Config.get ctxt show_sorts);
fun strip_fields T =
(case T of
@@ -856,7 +856,7 @@
fun mk_type_abbr subst name args =
let val abbrT = Type (name, map (varifyT o TFree) args)
- in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;
+ in Syntax.term_of_typ (Config.get ctxt show_sorts) (Envir.norm_type subst abbrT) end;
fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
in
--- a/src/HOL/ex/Numeral.thy Mon Sep 06 11:53:42 2010 +0200
+++ b/src/HOL/ex/Numeral.thy Mon Sep 06 12:38:45 2010 +0200
@@ -293,7 +293,7 @@
in [(@{syntax_const "_Numerals"}, numeral_tr)] end
*}
-typed_print_translation {*
+typed_print_translation (advanced) {*
let
fun dig b n = b + 2 * n;
fun int_of_num' (Const (@{const_syntax Dig0}, _) $ n) =
@@ -301,14 +301,15 @@
| int_of_num' (Const (@{const_syntax Dig1}, _) $ n) =
dig 1 (int_of_num' n)
| int_of_num' (Const (@{const_syntax One}, _)) = 1;
- fun num_tr' show_sorts T [n] =
+ fun num_tr' ctxt show_sorts T [n] =
let
val k = int_of_num' n;
val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k);
- in case T
- of Type (@{type_name fun}, [_, T']) =>
- if not (! show_types) andalso can Term.dest_Type T' then t'
- else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T'
+ in
+ case T of
+ Type (@{type_name fun}, [_, T']) =>
+ if not (Config.get ctxt show_types) andalso can Term.dest_Type T' then t'
+ else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T'
| T' => if T' = dummyT then t' else raise Match
end;
in [(@{const_syntax of_num}, num_tr')] end
--- a/src/Pure/Isar/attrib.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/Pure/Isar/attrib.ML Mon Sep 06 12:38:45 2010 +0200
@@ -392,7 +392,10 @@
(* theory setup *)
val _ = Context.>> (Context.map_theory
- (register_config Syntax.show_structs_value #>
+ (register_config Syntax.show_brackets_value #>
+ register_config Syntax.show_sorts_value #>
+ register_config Syntax.show_types_value #>
+ register_config Syntax.show_structs_value #>
register_config Syntax.show_question_marks_value #>
register_config Syntax.ambiguity_level_value #>
register_config Syntax.eta_contract_value #>
--- a/src/Pure/Isar/class.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/Pure/Isar/class.ML Mon Sep 06 12:38:45 2010 +0200
@@ -164,7 +164,7 @@
val Ss = Sorts.mg_domain algebra tyco [class];
in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "
- ^ setmp_CRITICAL show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty);
+ ^ (Syntax.string_of_typ (Config.put show_sorts false ctxt) o Type.strip_sorts) ty);
fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
(SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"),
(SOME o Pretty.block) [Pretty.str "supersort: ",
@@ -525,9 +525,8 @@
val params = map_product get_param tycos class_params |> map_filter I;
val primary_constraints = map (apsnd
(map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params;
- val pp = Syntax.pp_global thy;
val algebra = Sign.classes_of thy
- |> fold (fn tyco => Sorts.add_arities pp
+ |> fold (fn tyco => Sorts.add_arities (Syntax.pp_global thy)
(tyco, map (fn class => (class, map snd vs)) sort)) tycos;
val consts = Sign.consts_of thy;
val improve_constraints = AList.lookup (op =)
--- a/src/Pure/Isar/code.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/Pure/Isar/code.ML Mon Sep 06 12:38:45 2010 +0200
@@ -110,7 +110,8 @@
(* printing *)
-fun string_of_typ thy = setmp_CRITICAL show_sorts true (Syntax.string_of_typ_global thy);
+fun string_of_typ thy =
+ Syntax.string_of_typ (Config.put show_sorts true (Syntax.init_pretty_global thy));
fun string_of_const thy c = case AxClass.inst_of_param thy c
of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco)
--- a/src/Pure/Isar/local_defs.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/Pure/Isar/local_defs.ML Mon Sep 06 12:38:45 2010 +0200
@@ -47,7 +47,7 @@
fun err msg = cat_error msg ("The error(s) above occurred in definition: " ^
quote (Syntax.string_of_term ctxt eq));
val ((lhs, _), eq') = eq
- |> Sign.no_vars (Syntax.pp ctxt)
+ |> Sign.no_vars ctxt
|> Primitive_Defs.dest_def ctxt Term.is_Free (Variable.is_fixed ctxt) (K true)
handle TERM (msg, _) => err msg | ERROR msg => err msg;
in (Term.dest_Free (Term.head_of lhs), eq') end;
--- a/src/Pure/Isar/locale.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/Pure/Isar/locale.ML Mon Sep 06 12:38:45 2010 +0200
@@ -180,7 +180,8 @@
fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
- fun prt_term' t = if !show_types
+ fun prt_term' t =
+ if Config.get ctxt show_types
then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::",
Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)]
else prt_term t;
--- a/src/Pure/Isar/obtain.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/Pure/Isar/obtain.ML Mon Sep 06 12:38:45 2010 +0200
@@ -215,7 +215,7 @@
val thy = ProofContext.theory_of ctxt;
val certT = Thm.ctyp_of thy;
val cert = Thm.cterm_of thy;
- val string_of_term = setmp_CRITICAL show_types true (Syntax.string_of_term ctxt);
+ val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
fun err msg th = error (msg ^ ":\n" ^ Display.string_of_thm ctxt th);
--- a/src/Pure/Isar/proof_context.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML Mon Sep 06 12:38:45 2010 +0200
@@ -763,7 +763,7 @@
fun check t = (Syntax.check_term ctxt (Type_Infer.constrain T' t); NONE)
handle ERROR msg => SOME msg;
val t =
- Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
+ Syntax.standard_parse_term check get_sort map_const map_free
ctxt (Type.is_logtype (tsig_of ctxt)) (syn_of ctxt) T' (syms, pos)
handle ERROR msg => cat_error msg ("Failed to parse " ^ kind);
in t end;
--- a/src/Pure/ML/ml_context.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/Pure/ML/ml_context.ML Mon Sep 06 12:38:45 2010 +0200
@@ -19,9 +19,10 @@
val the_global_context: unit -> theory
val the_local_context: unit -> Proof.context
val exec: (unit -> unit) -> Context.generic -> Context.generic
- val stored_thms: thm list Unsynchronized.ref
+ val get_stored_thms: unit -> thm list
+ val get_stored_thm: unit -> thm
+ val ml_store_thms: string * thm list -> unit
val ml_store_thm: string * thm -> unit
- val ml_store_thms: string * thm list -> unit
type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context
val add_antiq: string -> (Position.T -> antiq context_parser) -> unit
val trace: bool Unsynchronized.ref
@@ -56,23 +57,34 @@
(* theorem bindings *)
-val stored_thms: thm list Unsynchronized.ref = Unsynchronized.ref []; (* FIXME via context!? *)
+structure Stored_Thms = Theory_Data
+(
+ type T = thm list;
+ val empty = [];
+ fun extend _ = [];
+ fun merge _ = [];
+);
-fun ml_store sel (name, ths) =
+fun get_stored_thms () = Stored_Thms.get (the_global_context ());
+val get_stored_thm = hd o get_stored_thms;
+
+fun ml_store get (name, ths) =
let
val ths' = Context.>>> (Context.map_theory_result
(PureThy.store_thms (Binding.name name, ths)));
+ val _ = Context.>> (Context.map_theory (Stored_Thms.put ths'));
val _ =
if name = "" then ()
else if not (ML_Syntax.is_identifier name) then
error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
- else setmp_CRITICAL stored_thms ths' (fn () =>
+ else
ML_Compiler.eval true Position.none
- (ML_Lex.tokenize ("val " ^ name ^ " = " ^ sel ^ "(! ML_Context.stored_thms);"))) ();
+ (ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();"));
+ val _ = Context.>> (Context.map_theory (Stored_Thms.put []));
in () end;
-val ml_store_thms = ml_store "";
-fun ml_store_thm (name, th) = ml_store "hd" (name, [th]);
+val ml_store_thms = ml_store "ML_Context.get_stored_thms";
+fun ml_store_thm (name, th) = ml_store "ML_Context.get_stored_thm" (name, [th]);
fun bind_thm (name, thm) = ml_store_thm (name, Drule.export_without_context thm);
fun bind_thms (name, thms) = ml_store_thms (name, map Drule.export_without_context thms);
--- a/src/Pure/ProofGeneral/preferences.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML Mon Sep 06 12:38:45 2010 +0200
@@ -78,7 +78,7 @@
(* preferences of Pure *)
-val proof_pref = setmp_CRITICAL Proofterm.proofs 1 (fn () =>
+val proof_pref = setmp_noncritical Proofterm.proofs 1 (fn () =>
let
fun get () = PgipTypes.bool_to_pgstring (! Proofterm.proofs >= 2);
fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1);
@@ -111,10 +111,10 @@
val display_preferences =
- [bool_pref show_types
+ [bool_pref show_types_default
"show-types"
"Include types in display of Isabelle terms",
- bool_pref show_sorts
+ bool_pref show_sorts_default
"show-sorts"
"Include sorts in display of Isabelle terms",
bool_pref show_consts_default
@@ -123,7 +123,7 @@
bool_pref long_names
"long-names"
"Show fully qualified names in Isabelle terms",
- bool_pref show_brackets
+ bool_pref show_brackets_default
"show-brackets"
"Show full bracketing in Isabelle terms",
bool_pref Goal_Display.show_main_goal_default
@@ -167,7 +167,7 @@
thm_deps_pref];
val proof_preferences =
- [setmp_CRITICAL quick_and_dirty true (fn () =>
+ [setmp_noncritical quick_and_dirty true (fn () =>
bool_pref quick_and_dirty
"quick-and-dirty"
"Take a few short cuts") (),
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Sep 06 12:38:45 2010 +0200
@@ -1044,7 +1044,7 @@
This works for preferences but not generally guaranteed
because we haven't done full setup here (e.g., no pgml mode) *)
fun process_pgip_emacs str =
- setmp_CRITICAL output_xml_fn (!pgip_output_channel) process_pgip_plain str
+ setmp_noncritical output_xml_fn (!pgip_output_channel) process_pgip_plain str
end
--- a/src/Pure/Syntax/printer.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/Pure/Syntax/printer.ML Mon Sep 06 12:38:45 2010 +0200
@@ -6,9 +6,15 @@
signature PRINTER0 =
sig
- val show_brackets: bool Unsynchronized.ref
- val show_sorts: bool Unsynchronized.ref
- val show_types: bool Unsynchronized.ref
+ val show_brackets_default: bool Unsynchronized.ref
+ val show_brackets_value: Config.value Config.T
+ val show_brackets: bool Config.T
+ val show_types_default: bool Unsynchronized.ref
+ val show_types_value: Config.value Config.T
+ val show_types: bool Config.T
+ val show_sorts_default: bool Unsynchronized.ref
+ val show_sorts_value: Config.value Config.T
+ val show_sorts: bool Config.T
val show_free_types: bool Config.T
val show_all_types: bool Config.T
val show_structs_value: Config.value Config.T
@@ -16,7 +22,6 @@
val show_question_marks_default: bool Unsynchronized.ref
val show_question_marks_value: Config.value Config.T
val show_question_marks: bool Config.T
- val pp_show_brackets: Pretty.pp -> Pretty.pp
end;
signature PRINTER =
@@ -49,9 +54,19 @@
(** options for printing **)
-val show_types = Unsynchronized.ref false;
-val show_sorts = Unsynchronized.ref false;
-val show_brackets = Unsynchronized.ref false;
+val show_brackets_default = Unsynchronized.ref false;
+val show_brackets_value =
+ Config.declare "show_brackets" (fn _ => Config.Bool (! show_brackets_default));
+val show_brackets = Config.bool show_brackets_value;
+
+val show_types_default = Unsynchronized.ref false;
+val show_types_value = Config.declare "show_types" (fn _ => Config.Bool (! show_types_default));
+val show_types = Config.bool show_types_value;
+
+val show_sorts_default = Unsynchronized.ref false;
+val show_sorts_value = Config.declare "show_sorts" (fn _ => Config.Bool (! show_sorts_default));
+val show_sorts = Config.bool show_sorts_value;
+
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));
@@ -63,9 +78,6 @@
Config.declare "show_question_marks" (fn _ => Config.Bool (! show_question_marks_default));
val show_question_marks = Config.bool show_question_marks_value;
-fun pp_show_brackets pp = Pretty.pp (setmp_CRITICAL show_brackets true (Pretty.term pp),
- Pretty.typ pp, Pretty.sort pp, Pretty.classrel pp, Pretty.arity pp);
-
(** misc utils **)
@@ -78,7 +90,7 @@
| app_first (f :: fs) = f ctxt args handle Match => app_first fs;
in app_first fns end;
-fun apply_typed x y fs = map (fn f => fn ctxt => f ctxt x y) fs;
+fun apply_typed x fs = map (fn f => fn ctxt => f ctxt (Config.get ctxt show_sorts) x) fs;
(* simple_ast_of *)
@@ -102,6 +114,7 @@
fun ast_of_termT ctxt trf tm =
let
+ val ctxt' = Config.put show_sorts false ctxt;
fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t
| ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t
| ast_of (Const (a, _)) = trans a []
@@ -111,19 +124,24 @@
| (f, args) => Ast.Appl (map ast_of (f :: args)))
| ast_of t = simple_ast_of ctxt t
and trans a args =
- ast_of (apply_trans ctxt (apply_typed false dummyT (trf a)) args)
+ ast_of (apply_trans ctxt' (apply_typed dummyT (trf a)) args)
handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
in ast_of tm end;
fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (Type_Ext.term_of_sort S);
-fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (Type_Ext.term_of_typ (! show_sorts) T);
+fun typ_to_ast ctxt trf T =
+ ast_of_termT ctxt trf (Type_Ext.term_of_typ (Config.get ctxt show_sorts) T);
(** term_to_ast **)
-fun ast_of_term idents consts ctxt trf show_types show_sorts tm =
+fun term_to_ast idents consts ctxt trf tm =
let
+ val show_types =
+ Config.get ctxt show_types orelse Config.get ctxt show_sorts orelse
+ Config.get ctxt show_all_types;
+ val show_sorts = Config.get ctxt show_sorts;
val show_structs = Config.get ctxt show_structs;
val show_free_types = Config.get ctxt show_free_types;
val show_all_types = Config.get ctxt show_all_types;
@@ -188,7 +206,7 @@
| (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
and trans a T args =
- ast_of (apply_trans ctxt (apply_typed show_sorts T (trf a)) args)
+ ast_of (apply_trans ctxt (apply_typed T (trf a)) args)
handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
and constrain t T =
@@ -204,10 +222,6 @@
|> ast_of
end;
-fun term_to_ast idents consts ctxt trf tm =
- ast_of_term idents consts ctxt trf
- (! show_types orelse ! show_sorts orelse Config.get ctxt show_all_types) (! show_sorts) tm;
-
(** type prtabs **)
@@ -303,6 +317,7 @@
fun pretty extern ctxt tabs trf tokentrf type_mode curried ast0 p0 =
let
val {extern_class, extern_type, extern_const} = extern;
+ val show_brackets = Config.get ctxt show_brackets;
fun token_trans a x =
(case tokentrf a of
@@ -349,8 +364,7 @@
in (T :: Ts, args') end
and parT markup (pr, args, p, p': int) = #1 (synT markup
- (if p > p' orelse
- (! show_brackets andalso p' <> Syn_Ext.max_pri andalso not (is_chain pr))
+ (if p > p' orelse (show_brackets andalso p' <> Syn_Ext.max_pri andalso not (is_chain pr))
then [Block (1, Space "(" :: pr @ [Space ")"])]
else pr, args))
--- a/src/Pure/Syntax/syntax.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML Mon Sep 06 12:38:45 2010 +0200
@@ -22,65 +22,7 @@
include SYN_TRANS1
include MIXFIX1
include PRINTER0
- type syntax
- val eq_syntax: syntax * syntax -> bool
- val is_keyword: syntax -> string -> bool
- type mode
- val mode_default: mode
- val mode_input: mode
- val merge_syntaxes: syntax -> syntax -> syntax
- val basic_syntax: syntax
- val basic_nonterms: string list
- val print_gram: syntax -> unit
- val print_trans: syntax -> unit
- val print_syntax: syntax -> unit
- val guess_infix: syntax -> string -> mixfix option
val read_token: string -> Symbol_Pos.T list * Position.T
- val ambiguity_enabled: bool Config.T
- val ambiguity_level_value: Config.value Config.T
- val ambiguity_level: int Config.T
- val ambiguity_limit: int Config.T
- val standard_parse_term: Pretty.pp -> (term -> string option) ->
- (((string * int) * sort) list -> string * int -> Term.sort) ->
- (string -> bool * string) -> (string -> string option) -> Proof.context ->
- (string -> bool) -> syntax -> typ -> Symbol_Pos.T list * Position.T -> term
- val standard_parse_typ: Proof.context -> syntax ->
- ((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ
- val standard_parse_sort: Proof.context -> syntax -> Symbol_Pos.T list * Position.T -> sort
- datatype 'a trrule =
- ParseRule of 'a * 'a |
- PrintRule of 'a * 'a |
- ParsePrintRule of 'a * 'a
- val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
- val is_const: syntax -> string -> bool
- val standard_unparse_term: {structs: string list, fixes: string list} ->
- {extern_class: string -> xstring, extern_type: string -> xstring,
- extern_const: string -> xstring} -> Proof.context -> syntax -> bool -> term -> Pretty.T
- val standard_unparse_typ: {extern_class: string -> xstring, extern_type: string -> xstring} ->
- Proof.context -> syntax -> typ -> Pretty.T
- val standard_unparse_sort: {extern_class: string -> xstring} ->
- Proof.context -> syntax -> sort -> Pretty.T
- val update_trfuns:
- (string * ((ast list -> ast) * stamp)) list *
- (string * ((term list -> term) * stamp)) list *
- (string * ((bool -> typ -> term list -> term) * stamp)) list *
- (string * ((ast list -> ast) * stamp)) list -> syntax -> syntax
- val update_advanced_trfuns:
- (string * ((Proof.context -> ast list -> ast) * stamp)) list *
- (string * ((Proof.context -> term list -> term) * stamp)) list *
- (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
- (string * ((Proof.context -> ast list -> ast) * stamp)) list -> syntax -> syntax
- val extend_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list ->
- syntax -> syntax
- val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax
- val update_const_gram: bool -> (string -> bool) ->
- mode -> (string * typ * mixfix) list -> syntax -> syntax
- val update_trrules: Proof.context -> (string -> bool) -> syntax ->
- (string * string) trrule list -> syntax -> syntax
- val remove_trrules: Proof.context -> (string -> bool) -> syntax ->
- (string * string) trrule list -> syntax -> syntax
- val update_trrules_i: ast trrule list -> syntax -> syntax
- val remove_trrules_i: ast trrule list -> syntax -> syntax
val parse_token: Proof.context -> Markup.T -> string -> Symbol_Pos.T list * Position.T
val parse_sort: Proof.context -> string -> sort
val parse_typ: Proof.context -> string -> typ
@@ -155,11 +97,302 @@
val string_of_sort_global: theory -> sort -> string
val pp: Proof.context -> Pretty.pp
val pp_global: theory -> Pretty.pp
+ type syntax
+ val eq_syntax: syntax * syntax -> bool
+ val is_keyword: syntax -> string -> bool
+ type mode
+ val mode_default: mode
+ val mode_input: mode
+ val merge_syntaxes: syntax -> syntax -> syntax
+ val basic_syntax: syntax
+ val basic_nonterms: string list
+ val print_gram: syntax -> unit
+ val print_trans: syntax -> unit
+ val print_syntax: syntax -> unit
+ val guess_infix: syntax -> string -> mixfix option
+ val ambiguity_enabled: bool Config.T
+ val ambiguity_level_value: Config.value Config.T
+ val ambiguity_level: int Config.T
+ val ambiguity_limit: int Config.T
+ val standard_parse_term: (term -> string option) ->
+ (((string * int) * sort) list -> string * int -> Term.sort) ->
+ (string -> bool * string) -> (string -> string option) -> Proof.context ->
+ (string -> bool) -> syntax -> typ -> Symbol_Pos.T list * Position.T -> term
+ val standard_parse_typ: Proof.context -> syntax ->
+ ((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ
+ val standard_parse_sort: Proof.context -> syntax -> Symbol_Pos.T list * Position.T -> sort
+ datatype 'a trrule =
+ ParseRule of 'a * 'a |
+ PrintRule of 'a * 'a |
+ ParsePrintRule of 'a * 'a
+ val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
+ val is_const: syntax -> string -> bool
+ val standard_unparse_term: {structs: string list, fixes: string list} ->
+ {extern_class: string -> xstring, extern_type: string -> xstring,
+ extern_const: string -> xstring} -> Proof.context -> syntax -> bool -> term -> Pretty.T
+ val standard_unparse_typ: {extern_class: string -> xstring, extern_type: string -> xstring} ->
+ Proof.context -> syntax -> typ -> Pretty.T
+ val standard_unparse_sort: {extern_class: string -> xstring} ->
+ Proof.context -> syntax -> sort -> Pretty.T
+ val update_trfuns:
+ (string * ((ast list -> ast) * stamp)) list *
+ (string * ((term list -> term) * stamp)) list *
+ (string * ((bool -> typ -> term list -> term) * stamp)) list *
+ (string * ((ast list -> ast) * stamp)) list -> syntax -> syntax
+ val update_advanced_trfuns:
+ (string * ((Proof.context -> ast list -> ast) * stamp)) list *
+ (string * ((Proof.context -> term list -> term) * stamp)) list *
+ (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
+ (string * ((Proof.context -> ast list -> ast) * stamp)) list -> syntax -> syntax
+ val extend_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list ->
+ syntax -> syntax
+ val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax
+ val update_const_gram: bool -> (string -> bool) ->
+ mode -> (string * typ * mixfix) list -> syntax -> syntax
+ val update_trrules: Proof.context -> (string -> bool) -> syntax ->
+ (string * string) trrule list -> syntax -> syntax
+ val remove_trrules: Proof.context -> (string -> bool) -> syntax ->
+ (string * string) trrule list -> syntax -> syntax
+ val update_trrules_i: ast trrule list -> syntax -> syntax
+ val remove_trrules_i: ast trrule list -> syntax -> syntax
end;
structure Syntax: SYNTAX =
struct
+(** inner syntax operations **)
+
+(* read token -- with optional YXML encoding of position *)
+
+fun read_token str =
+ let
+ val tree = YXML.parse str handle Fail msg => error msg;
+ val text = Buffer.empty |> XML.add_content tree |> Buffer.content;
+ val pos =
+ (case tree of
+ XML.Elem ((name, props), _) =>
+ if name = Markup.tokenN then Position.of_properties props
+ else Position.none
+ | XML.Text _ => Position.none);
+ in (Symbol_Pos.explode (text, pos), pos) end;
+
+
+(* (un)parsing *)
+
+fun parse_token ctxt markup str =
+ let
+ val (syms, pos) = read_token str;
+ val _ = Context_Position.report ctxt markup pos;
+ in (syms, pos) end;
+
+local
+
+type operations =
+ {parse_sort: Proof.context -> string -> sort,
+ parse_typ: Proof.context -> string -> typ,
+ parse_term: Proof.context -> string -> term,
+ parse_prop: Proof.context -> string -> term,
+ unparse_sort: Proof.context -> sort -> Pretty.T,
+ unparse_typ: Proof.context -> typ -> Pretty.T,
+ unparse_term: Proof.context -> term -> Pretty.T};
+
+val operations: operations Single_Assignment.var = Single_Assignment.var "Syntax.operations";
+
+fun operation which ctxt x =
+ (case Single_Assignment.peek operations of
+ NONE => raise Fail "Inner syntax operations not installed"
+ | SOME ops => which ops ctxt x);
+
+in
+
+val parse_sort = operation #parse_sort;
+val parse_typ = operation #parse_typ;
+val parse_term = operation #parse_term;
+val parse_prop = operation #parse_prop;
+val unparse_sort = operation #unparse_sort;
+val unparse_typ = operation #unparse_typ;
+val unparse_term = operation #unparse_term;
+
+fun install_operations ops = Single_Assignment.assign operations ops;
+
+end;
+
+
+(* context-sensitive (un)checking *)
+
+local
+
+type key = int * bool;
+type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
+
+structure Checks = Generic_Data
+(
+ type T =
+ ((key * ((string * typ check) * stamp) list) list *
+ (key * ((string * term check) * stamp) list) list);
+ val empty = ([], []);
+ val extend = I;
+ fun merge ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T =
+ (AList.join (op =) (K (Library.merge (eq_snd (op =)))) (typ_checks1, typ_checks2),
+ AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2));
+);
+
+fun gen_add which (key: key) name f =
+ Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
+
+fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs));
+
+fun gen_check which uncheck ctxt0 xs0 =
+ let
+ val funs = which (Checks.get (Context.Proof ctxt0))
+ |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE)
+ |> Library.sort (int_ord o pairself fst) |> map snd
+ |> not uncheck ? map rev;
+ val check_all = perhaps_apply (map check_stage funs);
+ in #1 (perhaps check_all (xs0, ctxt0)) end;
+
+fun map_sort f S =
+ (case f (TFree ("", S)) of
+ TFree ("", S') => S'
+ | _ => raise TYPE ("map_sort", [TFree ("", S)], []));
+
+in
+
+fun print_checks ctxt =
+ let
+ fun split_checks checks =
+ List.partition (fn ((_, un), _) => not un) checks
+ |> pairself (map (fn ((i, _), fs) => (i, map (fst o fst) fs))
+ #> sort (int_ord o pairself fst));
+ fun pretty_checks kind checks =
+ checks |> map (fn (i, names) => Pretty.block
+ [Pretty.str (kind ^ " (stage " ^ signed_string_of_int i ^ "):"),
+ Pretty.brk 1, Pretty.strs names]);
+
+ val (typs, terms) = Checks.get (Context.Proof ctxt);
+ val (typ_checks, typ_unchecks) = split_checks typs;
+ val (term_checks, term_unchecks) = split_checks terms;
+ in
+ pretty_checks "typ_checks" typ_checks @
+ pretty_checks "term_checks" term_checks @
+ pretty_checks "typ_unchecks" typ_unchecks @
+ pretty_checks "term_unchecks" term_unchecks
+ end |> Pretty.chunks |> Pretty.writeln;
+
+fun add_typ_check stage = gen_add apfst (stage, false);
+fun add_term_check stage = gen_add apsnd (stage, false);
+fun add_typ_uncheck stage = gen_add apfst (stage, true);
+fun add_term_uncheck stage = gen_add apsnd (stage, true);
+
+val check_typs = gen_check fst false;
+val check_terms = gen_check snd false;
+fun check_props ctxt = map (Type_Ext.type_constraint propT) #> check_terms ctxt;
+
+val check_typ = singleton o check_typs;
+val check_term = singleton o check_terms;
+val check_prop = singleton o check_props;
+val check_sort = map_sort o check_typ;
+
+val uncheck_typs = gen_check fst true;
+val uncheck_terms = gen_check snd true;
+val uncheck_sort = map_sort o singleton o uncheck_typs;
+
+end;
+
+
+(* derived operations for classrel and arity *)
+
+val uncheck_classrel = map o singleton o uncheck_sort;
+
+fun unparse_classrel ctxt cs = Pretty.block (flat
+ (separate [Pretty.str " <", Pretty.brk 1] (map (single o unparse_sort ctxt o single) cs)));
+
+fun uncheck_arity ctxt (a, Ss, S) =
+ let
+ val T = Type (a, replicate (length Ss) dummyT);
+ val a' =
+ (case singleton (uncheck_typs ctxt) T of
+ Type (a', _) => a'
+ | T => raise TYPE ("uncheck_arity", [T], []));
+ val Ss' = map (uncheck_sort ctxt) Ss;
+ val S' = uncheck_sort ctxt S;
+ in (a', Ss', S') end;
+
+fun unparse_arity ctxt (a, Ss, S) =
+ let
+ val prtT = unparse_typ ctxt (Type (a, []));
+ val dom =
+ if null Ss then []
+ else [Pretty.list "(" ")" (map (unparse_sort ctxt) Ss), Pretty.brk 1];
+ in Pretty.block ([prtT, Pretty.str " ::", Pretty.brk 1] @ dom @ [unparse_sort ctxt S]) end;
+
+
+(* read = parse + check *)
+
+fun read_sort ctxt = parse_sort ctxt #> check_sort ctxt;
+fun read_typ ctxt = parse_typ ctxt #> singleton (check_typs ctxt);
+
+fun read_terms ctxt = map (parse_term ctxt) #> check_terms ctxt;
+fun read_props ctxt = map (parse_prop ctxt) #> check_props ctxt;
+
+val read_term = singleton o read_terms;
+val read_prop = singleton o read_props;
+
+val read_sort_global = read_sort o ProofContext.init_global;
+val read_typ_global = read_typ o ProofContext.init_global;
+val read_term_global = read_term o ProofContext.init_global;
+val read_prop_global = read_prop o ProofContext.init_global;
+
+
+(* pretty = uncheck + unparse *)
+
+fun pretty_term ctxt = singleton (uncheck_terms ctxt) #> unparse_term ctxt;
+fun pretty_typ ctxt = singleton (uncheck_typs ctxt) #> unparse_typ ctxt;
+fun pretty_sort ctxt = uncheck_sort ctxt #> unparse_sort ctxt;
+fun pretty_classrel ctxt = uncheck_classrel ctxt #> unparse_classrel ctxt;
+fun pretty_arity ctxt = uncheck_arity ctxt #> unparse_arity ctxt;
+
+val string_of_term = Pretty.string_of oo pretty_term;
+val string_of_typ = Pretty.string_of oo pretty_typ;
+val string_of_sort = Pretty.string_of oo pretty_sort;
+val string_of_classrel = Pretty.string_of oo pretty_classrel;
+val string_of_arity = Pretty.string_of oo pretty_arity;
+
+
+(* global pretty printing *)
+
+structure PrettyGlobal = Proof_Data(type T = bool fun init _ = false);
+val is_pretty_global = PrettyGlobal.get;
+val set_pretty_global = PrettyGlobal.put;
+val init_pretty_global = set_pretty_global true o ProofContext.init_global;
+
+val pretty_term_global = pretty_term o init_pretty_global;
+val pretty_typ_global = pretty_typ o init_pretty_global;
+val pretty_sort_global = pretty_sort o init_pretty_global;
+
+val string_of_term_global = string_of_term o init_pretty_global;
+val string_of_typ_global = string_of_typ o init_pretty_global;
+val string_of_sort_global = string_of_sort o init_pretty_global;
+
+
+(* pp operations -- deferred evaluation *)
+
+fun pp ctxt = Pretty.pp
+ (fn x => pretty_term ctxt x,
+ fn x => pretty_typ ctxt x,
+ fn x => pretty_sort ctxt x,
+ fn x => pretty_classrel ctxt x,
+ fn x => pretty_arity ctxt x);
+
+fun pp_global thy = Pretty.pp
+ (fn x => pretty_term_global thy x,
+ fn x => pretty_typ_global thy x,
+ fn x => pretty_sort_global thy x,
+ fn x => pretty_classrel (init_pretty_global thy) x,
+ fn x => pretty_arity (init_pretty_global thy) x);
+
+
+
(** tables of translation functions **)
(* parse (ast) translations *)
@@ -456,21 +689,6 @@
(** read **)
-(* read token -- with optional YXML encoding of position *)
-
-fun read_token str =
- let
- val tree = YXML.parse str handle Fail msg => error msg;
- val text = Buffer.empty |> XML.add_content tree |> Buffer.content;
- val pos =
- (case tree of
- XML.Elem ((name, props), _) =>
- if name = Markup.tokenN then Position.of_properties props
- else Position.none
- | XML.Text _ => Position.none);
- in (Symbol_Pos.explode (text, pos), pos) end;
-
-
(* read_ast *)
val ambiguity_enabled =
@@ -525,8 +743,8 @@
(* read terms *)
(*brute-force disambiguation via type-inference*)
-fun disambig _ _ _ [t] = t
- | disambig ctxt pp check ts =
+fun disambig _ _ [t] = t
+ | disambig ctxt check ts =
let
val level = Config.get ctxt ambiguity_level;
val limit = Config.get ctxt ambiguity_limit;
@@ -541,6 +759,8 @@
val errs = Par_List.map check ts;
val results = map_filter (fn (t, NONE) => SOME t | _ => NONE) (ts ~~ errs);
val len = length results;
+
+ val show_term = string_of_term (Config.put Printer.show_brackets true ctxt);
in
if null results then cat_error (ambig_msg ()) (cat_lines (map_filter I errs))
else if len = 1 then
@@ -552,13 +772,13 @@
else cat_error (ambig_msg ()) (cat_lines
(("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
(if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
- map (Pretty.string_of_term pp) (take limit results)))
+ map show_term (take limit results)))
end;
-fun standard_parse_term pp check get_sort map_const map_free ctxt is_logtype syn ty (syms, pos) =
+fun standard_parse_term check get_sort map_const map_free ctxt is_logtype syn ty (syms, pos) =
read ctxt is_logtype syn ty (syms, pos)
|> map (Type_Ext.decode_term get_sort map_const map_free)
- |> disambig ctxt (Printer.pp_show_brackets pp) check;
+ |> disambig ctxt check;
(* read types *)
@@ -696,224 +916,6 @@
val remove_trrules_i = remove_syntax mode_default o Syn_Ext.syn_ext_rules o cert_rules;
-
-(** inner syntax operations **)
-
-(* (un)parsing *)
-
-fun parse_token ctxt markup str =
- let
- val (syms, pos) = read_token str;
- val _ = Context_Position.report ctxt markup pos;
- in (syms, pos) end;
-
-local
-
-type operations =
- {parse_sort: Proof.context -> string -> sort,
- parse_typ: Proof.context -> string -> typ,
- parse_term: Proof.context -> string -> term,
- parse_prop: Proof.context -> string -> term,
- unparse_sort: Proof.context -> sort -> Pretty.T,
- unparse_typ: Proof.context -> typ -> Pretty.T,
- unparse_term: Proof.context -> term -> Pretty.T};
-
-val operations: operations Single_Assignment.var = Single_Assignment.var "Syntax.operations";
-
-fun operation which ctxt x =
- (case Single_Assignment.peek operations of
- NONE => raise Fail "Inner syntax operations not installed"
- | SOME ops => which ops ctxt x);
-
-in
-
-val parse_sort = operation #parse_sort;
-val parse_typ = operation #parse_typ;
-val parse_term = operation #parse_term;
-val parse_prop = operation #parse_prop;
-val unparse_sort = operation #unparse_sort;
-val unparse_typ = operation #unparse_typ;
-val unparse_term = operation #unparse_term;
-
-fun install_operations ops = Single_Assignment.assign operations ops;
-
-end;
-
-
-(* context-sensitive (un)checking *)
-
-local
-
-type key = int * bool;
-type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
-
-structure Checks = Generic_Data
-(
- type T =
- ((key * ((string * typ check) * stamp) list) list *
- (key * ((string * term check) * stamp) list) list);
- val empty = ([], []);
- val extend = I;
- fun merge ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T =
- (AList.join (op =) (K (Library.merge (eq_snd (op =)))) (typ_checks1, typ_checks2),
- AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2));
-);
-
-fun gen_add which (key: key) name f =
- Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
-
-fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs));
-
-fun gen_check which uncheck ctxt0 xs0 =
- let
- val funs = which (Checks.get (Context.Proof ctxt0))
- |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE)
- |> Library.sort (int_ord o pairself fst) |> map snd
- |> not uncheck ? map rev;
- val check_all = perhaps_apply (map check_stage funs);
- in #1 (perhaps check_all (xs0, ctxt0)) end;
-
-fun map_sort f S =
- (case f (TFree ("", S)) of
- TFree ("", S') => S'
- | _ => raise TYPE ("map_sort", [TFree ("", S)], []));
-
-in
-
-fun print_checks ctxt =
- let
- fun split_checks checks =
- List.partition (fn ((_, un), _) => not un) checks
- |> pairself (map (fn ((i, _), fs) => (i, map (fst o fst) fs))
- #> sort (int_ord o pairself fst));
- fun pretty_checks kind checks =
- checks |> map (fn (i, names) => Pretty.block
- [Pretty.str (kind ^ " (stage " ^ signed_string_of_int i ^ "):"),
- Pretty.brk 1, Pretty.strs names]);
-
- val (typs, terms) = Checks.get (Context.Proof ctxt);
- val (typ_checks, typ_unchecks) = split_checks typs;
- val (term_checks, term_unchecks) = split_checks terms;
- in
- pretty_checks "typ_checks" typ_checks @
- pretty_checks "term_checks" term_checks @
- pretty_checks "typ_unchecks" typ_unchecks @
- pretty_checks "term_unchecks" term_unchecks
- end |> Pretty.chunks |> Pretty.writeln;
-
-fun add_typ_check stage = gen_add apfst (stage, false);
-fun add_term_check stage = gen_add apsnd (stage, false);
-fun add_typ_uncheck stage = gen_add apfst (stage, true);
-fun add_term_uncheck stage = gen_add apsnd (stage, true);
-
-val check_typs = gen_check fst false;
-val check_terms = gen_check snd false;
-fun check_props ctxt = map (Type_Ext.type_constraint propT) #> check_terms ctxt;
-
-val check_typ = singleton o check_typs;
-val check_term = singleton o check_terms;
-val check_prop = singleton o check_props;
-val check_sort = map_sort o check_typ;
-
-val uncheck_typs = gen_check fst true;
-val uncheck_terms = gen_check snd true;
-val uncheck_sort = map_sort o singleton o uncheck_typs;
-
-end;
-
-
-(* derived operations for classrel and arity *)
-
-val uncheck_classrel = map o singleton o uncheck_sort;
-
-fun unparse_classrel ctxt cs = Pretty.block (flat
- (separate [Pretty.str " <", Pretty.brk 1] (map (single o unparse_sort ctxt o single) cs)));
-
-fun uncheck_arity ctxt (a, Ss, S) =
- let
- val T = Type (a, replicate (length Ss) dummyT);
- val a' =
- (case singleton (uncheck_typs ctxt) T of
- Type (a', _) => a'
- | T => raise TYPE ("uncheck_arity", [T], []));
- val Ss' = map (uncheck_sort ctxt) Ss;
- val S' = uncheck_sort ctxt S;
- in (a', Ss', S') end;
-
-fun unparse_arity ctxt (a, Ss, S) =
- let
- val prtT = unparse_typ ctxt (Type (a, []));
- val dom =
- if null Ss then []
- else [Pretty.list "(" ")" (map (unparse_sort ctxt) Ss), Pretty.brk 1];
- in Pretty.block ([prtT, Pretty.str " ::", Pretty.brk 1] @ dom @ [unparse_sort ctxt S]) end;
-
-
-(* read = parse + check *)
-
-fun read_sort ctxt = parse_sort ctxt #> check_sort ctxt;
-fun read_typ ctxt = parse_typ ctxt #> singleton (check_typs ctxt);
-
-fun read_terms ctxt = map (parse_term ctxt) #> check_terms ctxt;
-fun read_props ctxt = map (parse_prop ctxt) #> check_props ctxt;
-
-val read_term = singleton o read_terms;
-val read_prop = singleton o read_props;
-
-val read_sort_global = read_sort o ProofContext.init_global;
-val read_typ_global = read_typ o ProofContext.init_global;
-val read_term_global = read_term o ProofContext.init_global;
-val read_prop_global = read_prop o ProofContext.init_global;
-
-
-(* pretty = uncheck + unparse *)
-
-fun pretty_term ctxt = singleton (uncheck_terms ctxt) #> unparse_term ctxt;
-fun pretty_typ ctxt = singleton (uncheck_typs ctxt) #> unparse_typ ctxt;
-fun pretty_sort ctxt = uncheck_sort ctxt #> unparse_sort ctxt;
-fun pretty_classrel ctxt = uncheck_classrel ctxt #> unparse_classrel ctxt;
-fun pretty_arity ctxt = uncheck_arity ctxt #> unparse_arity ctxt;
-
-val string_of_term = Pretty.string_of oo pretty_term;
-val string_of_typ = Pretty.string_of oo pretty_typ;
-val string_of_sort = Pretty.string_of oo pretty_sort;
-val string_of_classrel = Pretty.string_of oo pretty_classrel;
-val string_of_arity = Pretty.string_of oo pretty_arity;
-
-
-(* global pretty printing *)
-
-structure PrettyGlobal = Proof_Data(type T = bool fun init _ = false);
-val is_pretty_global = PrettyGlobal.get;
-val set_pretty_global = PrettyGlobal.put;
-val init_pretty_global = set_pretty_global true o ProofContext.init_global;
-
-val pretty_term_global = pretty_term o init_pretty_global;
-val pretty_typ_global = pretty_typ o init_pretty_global;
-val pretty_sort_global = pretty_sort o init_pretty_global;
-
-val string_of_term_global = string_of_term o init_pretty_global;
-val string_of_typ_global = string_of_typ o init_pretty_global;
-val string_of_sort_global = string_of_sort o init_pretty_global;
-
-
-(* pp operations -- deferred evaluation *)
-
-fun pp ctxt = Pretty.pp
- (fn x => pretty_term ctxt x,
- fn x => pretty_typ ctxt x,
- fn x => pretty_sort ctxt x,
- fn x => pretty_classrel ctxt x,
- fn x => pretty_arity ctxt x);
-
-fun pp_global thy = Pretty.pp
- (fn x => pretty_term_global thy x,
- fn x => pretty_typ_global thy x,
- fn x => pretty_sort_global thy x,
- fn x => pretty_classrel (init_pretty_global thy) x,
- fn x => pretty_arity (init_pretty_global thy) x);
-
-
(*export parts of internal Syntax structures*)
open Lexicon Syn_Ext Ast Parser Type_Ext Syn_Trans Mixfix Printer;
--- a/src/Pure/Thy/thy_output.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML Mon Sep 06 12:38:45 2010 +0200
@@ -444,8 +444,8 @@
(* options *)
-val _ = add_option "show_types" (add_wrapper o setmp_CRITICAL Syntax.show_types o boolean);
-val _ = add_option "show_sorts" (add_wrapper o setmp_CRITICAL Syntax.show_sorts o boolean);
+val _ = add_option "show_types" (Config.put show_types o boolean);
+val _ = add_option "show_sorts" (Config.put show_sorts o boolean);
val _ = add_option "show_structs" (Config.put show_structs o boolean);
val _ = add_option "show_question_marks" (Config.put show_question_marks o boolean);
val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean);
--- a/src/Pure/axclass.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/Pure/axclass.ML Mon Sep 06 12:38:45 2010 +0200
@@ -507,8 +507,7 @@
fun define_class (bclass, raw_super) raw_params raw_specs thy =
let
- val ctxt = ProofContext.init_global thy;
- val pp = Syntax.pp ctxt;
+ val ctxt = Syntax.init_pretty_global thy;
(* class *)
@@ -520,8 +519,8 @@
fun check_constraint (a, S) =
if Sign.subsort thy (super, S) then ()
else error ("Sort constraint of type variable " ^
- setmp_CRITICAL show_sorts true (Pretty.string_of_typ pp) (TFree (a, S)) ^
- " needs to be weaker than " ^ Pretty.string_of_sort pp super);
+ Syntax.string_of_typ (Config.put show_sorts true ctxt) (TFree (a, S)) ^
+ " needs to be weaker than " ^ Syntax.string_of_sort ctxt super);
(* params *)
@@ -543,7 +542,7 @@
(case Term.add_tfrees t [] of
[(a, S)] => check_constraint (a, S)
| [] => ()
- | _ => error ("Multiple type variables in class axiom:\n" ^ Pretty.string_of_term pp t);
+ | _ => error ("Multiple type variables in class axiom:\n" ^ Syntax.string_of_term ctxt t);
t
|> Term.map_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U))
|> Logic.close_form);
@@ -590,7 +589,7 @@
|> PureThy.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> #2
|> Sign.restore_naming facts_thy
|> map_axclasses (Symtab.update (class, axclass))
- |> map_params (fold (fn (x, _) => add_param pp (x, class)) params);
+ |> map_params (fold (fn (x, _) => add_param (Syntax.pp ctxt) (x, class)) params);
in (class, result_thy) end;
--- a/src/Pure/goal_display.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/Pure/goal_display.ML Mon Sep 06 12:38:45 2010 +0200
@@ -77,12 +77,20 @@
fun pretty_goals ctxt0 state =
let
- val ctxt = Config.put show_free_types false ctxt0;
+ val ctxt = ctxt0
+ |> Config.put show_free_types false
+ |> Config.put show_types
+ (Config.get ctxt0 show_types orelse
+ Config.get ctxt0 show_sorts orelse
+ Config.get ctxt0 show_all_types)
+ |> Config.put show_sorts false;
- val show_all_types = Config.get ctxt show_all_types;
+ val show_sorts0 = Config.get ctxt0 show_sorts;
+ val show_types = Config.get ctxt show_types;
+ val show_consts = Config.get ctxt show_consts
+ val show_main_goal = Config.get ctxt show_main_goal;
val goals_limit = Config.get ctxt goals_limit;
val goals_total = Config.get ctxt goals_total;
- val show_main_goal = Config.get ctxt show_main_goal;
val prt_sort = Syntax.pretty_sort ctxt;
val prt_typ = Syntax.pretty_typ ctxt;
@@ -120,23 +128,18 @@
val {prop, tpairs, ...} = Thm.rep_thm state;
val (As, B) = Logic.strip_horn prop;
val ngoals = length As;
-
- fun pretty_gs (types, sorts) =
- (if show_main_goal then [prt_term B] else []) @
- (if ngoals = 0 then [Pretty.str "No subgoals!"]
- else if ngoals > goals_limit then
- pretty_subgoals (take goals_limit As) @
- (if goals_total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
- else [])
- else pretty_subgoals As) @
- pretty_ffpairs tpairs @
- (if Config.get ctxt show_consts then pretty_consts prop else []) @
- (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_sorts false pretty_gs)
- (! show_types orelse ! show_sorts orelse show_all_types, ! show_sorts)
+ (if show_main_goal then [prt_term B] else []) @
+ (if ngoals = 0 then [Pretty.str "No subgoals!"]
+ else if ngoals > goals_limit then
+ pretty_subgoals (take goals_limit As) @
+ (if goals_total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
+ else [])
+ else pretty_subgoals As) @
+ pretty_ffpairs tpairs @
+ (if show_consts then pretty_consts prop else []) @
+ (if show_types then pretty_vars prop else []) @
+ (if show_sorts0 then pretty_varsT prop else [])
end;
fun pretty_goals_without_context th =
--- a/src/Pure/more_thm.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/Pure/more_thm.ML Mon Sep 06 12:38:45 2010 +0200
@@ -348,7 +348,7 @@
let
val b' = if Binding.is_empty b then Binding.name ("unnamed_axiom_" ^ serial_string ()) else b;
- val _ = Sign.no_vars (Syntax.pp_global thy) prop;
+ val _ = Sign.no_vars (Syntax.init_pretty_global thy) prop;
val (strip, recover, prop') = stripped_sorts thy prop;
val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of thy T, S)) strip;
@@ -365,7 +365,7 @@
fun add_def unchecked overloaded (b, prop) thy =
let
- val _ = Sign.no_vars (Syntax.pp_global thy) prop;
+ val _ = Sign.no_vars (Syntax.init_pretty_global thy) prop;
val prems = map (Thm.cterm_of thy) (Logic.strip_imp_prems prop);
val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop);
--- a/src/Pure/sign.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/Pure/sign.ML Mon Sep 06 12:38:45 2010 +0200
@@ -67,8 +67,8 @@
val certify_term: theory -> term -> term * typ * int
val cert_term: theory -> term -> term
val cert_prop: theory -> term -> term
- val no_frees: Pretty.pp -> term -> term
- val no_vars: Pretty.pp -> term -> term
+ val no_frees: Proof.context -> term -> term
+ val no_vars: Proof.context -> term -> term
val add_types: (binding * int * mixfix) list -> theory -> theory
val add_nonterminals: binding list -> theory -> theory
val add_type_abbrev: binding * string list * typ -> theory -> theory
@@ -270,8 +270,7 @@
val xs = map Free bs; (*we do not rename here*)
val t' = subst_bounds (xs, t);
val u' = subst_bounds (xs, u);
- val msg = cat_lines
- (Type_Infer.appl_error (Syntax.pp_show_brackets pp) why t' T u' U);
+ val msg = cat_lines (Type_Infer.appl_error pp why t' T u' U);
in raise TYPE (msg, [T, U], [t', u']) end;
fun typ_of (_, Const (_, T)) = T
@@ -320,12 +319,13 @@
(* specifications *)
-fun no_variables kind add addT mk mkT pp tm =
+fun no_variables kind add addT mk mkT ctxt tm =
(case (add tm [], addT tm []) of
([], []) => tm
| (frees, tfrees) => error (Pretty.string_of (Pretty.block
(Pretty.str ("Illegal " ^ kind ^ " variable(s) in term:") :: Pretty.brk 1 ::
- Pretty.commas (map (Pretty.term pp o mk) frees @ map (Pretty.typ pp o mkT) tfrees)))));
+ Pretty.commas
+ (map (Syntax.pretty_term ctxt o mk) frees @ map (Syntax.pretty_typ ctxt o mkT) tfrees)))));
val no_frees = no_variables "free" Term.add_frees Term.add_tfrees Free TFree;
val no_vars = no_variables "schematic" Term.add_vars Term.add_tvars Var TVar;
@@ -434,12 +434,12 @@
fun add_abbrev mode (b, raw_t) thy =
let
- val pp = Syntax.pp_global thy;
- val prep_tm = no_frees pp o Term.no_dummy_patterns o cert_term_abbrev thy;
+ val ctxt = Syntax.init_pretty_global thy;
+ val prep_tm = no_frees ctxt o Term.no_dummy_patterns o cert_term_abbrev thy;
val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.str_of b));
val (res, consts') = consts_of thy
- |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode (b, t);
+ |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of thy) (naming_of thy) mode (b, t);
in (res, thy |> map_consts (K consts')) end;
fun revert_abbrev mode c = map_consts (Consts.revert_abbrev mode c);
--- a/src/Pure/theory.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/Pure/theory.ML Mon Sep 06 12:38:45 2010 +0200
@@ -161,13 +161,15 @@
| TERM (msg, _) => error msg;
val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
+ val ctxt = Syntax.init_pretty_global thy
+ |> Config.put show_sorts true;
val bad_sorts =
rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I | (T, _) => insert (op =) T) t []);
val _ = null bad_sorts orelse
error ("Illegal sort constraints in primitive specification: " ^
- commas (map (setmp_CRITICAL show_sorts true (Syntax.string_of_typ_global thy)) bad_sorts));
+ commas (map (Syntax.string_of_typ ctxt) bad_sorts));
in
- (b, Sign.no_vars (Syntax.pp_global thy) t)
+ (b, Sign.no_vars (Syntax.init_pretty_global thy) t)
end handle ERROR msg =>
cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b));
@@ -182,10 +184,10 @@
fun dependencies thy unchecked def description lhs rhs =
let
- val pp = Syntax.pp_global thy;
+ val ctxt = Syntax.init_pretty_global thy;
val consts = Sign.consts_of thy;
fun prep const =
- let val Const (c, T) = Sign.no_vars pp (Const const)
+ let val Const (c, T) = Sign.no_vars ctxt (Const const)
in (c, Consts.typargs consts (c, Logic.varifyT_global T)) end;
val lhs_vars = Term.add_tfreesT (#2 lhs) [];
@@ -194,9 +196,9 @@
val _ =
if null rhs_extras then ()
else error ("Specification depends on extra type variables: " ^
- commas_quote (map (Pretty.string_of_typ pp o TFree) rhs_extras) ^
+ commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^
"\nThe error(s) above occurred in " ^ quote description);
- in Defs.define pp unchecked def description (prep lhs) (map prep rhs) end;
+ in Defs.define (Syntax.pp ctxt) unchecked def description (prep lhs) (map prep rhs) end;
fun add_deps a raw_lhs raw_rhs thy =
let
@@ -217,18 +219,18 @@
handle TYPE (msg, _, _) => error msg;
val T' = Logic.varifyT_global T;
- fun message txt =
+ val ctxt = Syntax.init_pretty_global thy;
+ fun message sorts txt =
[Pretty.block [Pretty.str "Specification of constant ",
- Pretty.str c, Pretty.str " ::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ_global thy T)],
+ Pretty.str c, Pretty.str " ::", Pretty.brk 1,
+ Pretty.quote (Syntax.pretty_typ (Config.put show_sorts sorts ctxt) T)],
Pretty.str txt] |> Pretty.chunks |> Pretty.string_of;
in
if Sign.typ_instance thy (declT, T') then ()
else if Type.raw_instance (declT, T') then
- error (setmp_CRITICAL show_sorts true
- message "imposes additional sort constraints on the constant declaration")
+ error (message true "imposes additional sort constraints on the constant declaration")
else if overloaded then ()
- else warning (message "is strictly less general than the declared type");
- (c, T)
+ else warning (message false "is strictly less general than the declared type")
end;
@@ -272,7 +274,7 @@
| const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)"
| const_of _ = error "Attempt to finalize non-constant term";
fun specify (c, T) = dependencies thy false NONE (c ^ " axiom") (c, T) [];
- val finalize = specify o check_overloading thy overloaded o const_of o
+ val finalize = specify o tap (check_overloading thy overloaded) o const_of o
Sign.cert_term thy o prep_term thy;
in thy |> map_defs (fold finalize args) end;
--- a/src/Tools/Code/code_preproc.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML Mon Sep 06 12:38:45 2010 +0200
@@ -429,10 +429,9 @@
fun dynamic_eval thy cterm_of conclude_evaluation evaluator proto_ct =
let
- val pp = Syntax.pp_global thy;
+ val ctxt = Syntax.init_pretty_global thy;
val ct = cterm_of proto_ct;
- val _ = (Sign.no_frees pp o map_types (K dummyT) o Sign.no_vars pp)
- (Thm.term_of ct);
+ val _ = (Sign.no_frees ctxt o map_types (K dummyT) o Sign.no_vars ctxt) (Thm.term_of ct);
val thm = preprocess_conv thy ct;
val ct' = Thm.rhs_of thm;
val (vs', t') = dest_cterm ct';
--- a/src/Tools/auto_solve.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/Tools/auto_solve.ML Mon Sep 06 12:38:45 2010 +0200
@@ -33,7 +33,7 @@
val _ =
ProofGeneralPgip.add_preference Preferences.category_tracing
- (setmp_CRITICAL auto true (fn () =>
+ (setmp_noncritical auto true (fn () =>
Preferences.bool_pref auto
"auto-solve"
"Try to solve newly declared lemmas with existing theorems.") ());
--- a/src/Tools/jEdit/src/jedit/document_view.scala Mon Sep 06 11:53:42 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Mon Sep 06 12:38:45 2010 +0200
@@ -12,11 +12,12 @@
import scala.actors.Actor._
-import java.awt.event.{MouseAdapter, MouseEvent}
+import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent, FocusAdapter, FocusEvent}
import java.awt.{BorderLayout, Graphics, Dimension, Color, Graphics2D}
import javax.swing.{JPanel, ToolTipManager}
import javax.swing.event.{CaretListener, CaretEvent}
+import org.gjt.sp.jedit.OperatingSystem
import org.gjt.sp.jedit.gui.RolloverButton
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
import org.gjt.sp.jedit.syntax.SyntaxStyle
@@ -123,6 +124,13 @@
proper_line_range(start, if (raw_end >= 0) raw_end else model.buffer.getLength)
}
+ def invalidate_line_range(range: Text.Range)
+ {
+ text_area.invalidateLineRange(
+ model.buffer.getLineOfOffset(range.start),
+ model.buffer.getLineOfOffset(range.stop))
+ }
+
/* commands_changed_actor */
@@ -161,6 +169,41 @@
}
+ /* subexpression highlighting */
+
+ private def subexp_range(snapshot: Document.Snapshot, x: Int, y: Int): Option[Text.Range] =
+ {
+ val subexp_markup: PartialFunction[Text.Info[Any], Option[Text.Range]] =
+ {
+ case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), _)) =>
+ Some(snapshot.convert(range))
+ }
+ val offset = text_area.xyToOffset(x, y)
+ val markup = snapshot.select_markup(Text.Range(offset, offset + 1))(subexp_markup)(None)
+ if (markup.hasNext) markup.next.info else None
+ }
+
+ private var highlight_range: Option[Text.Range] = None
+
+ private val focus_listener = new FocusAdapter {
+ override def focusLost(e: FocusEvent) { highlight_range = None }
+ }
+
+ private val mouse_motion_listener = new MouseMotionAdapter {
+ override def mouseMoved(e: MouseEvent) {
+ val control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
+ if (!model.buffer.isLoaded) highlight_range = None
+ else
+ Isabelle.swing_buffer_lock(model.buffer) {
+ highlight_range.map(invalidate_line_range(_))
+ highlight_range =
+ if (control) subexp_range(model.snapshot(), e.getX(), e.getY()) else None
+ highlight_range.map(invalidate_line_range(_))
+ }
+ }
+ }
+
+
/* text_area_extension */
private val text_area_extension = new TextAreaExtension
@@ -173,6 +216,7 @@
val snapshot = model.snapshot()
val saved_color = gfx.getColor
val ascent = text_area.getPainter.getFontMetrics.getAscent
+
try {
for (i <- 0 until physical_lines.length) {
if (physical_lines(i) != -1) {
@@ -189,6 +233,18 @@
gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
}
+ // subexpression highlighting -- potentially from other snapshot
+ if (highlight_range.isDefined) {
+ if (line_range.overlaps(highlight_range.get)) {
+ Isabelle.gfx_range(text_area, line_range.restrict(highlight_range.get)) match {
+ case None =>
+ case Some(r) =>
+ gfx.setColor(Color.black)
+ gfx.drawRect(r.x, y + i * line_height, r.length, line_height - 1)
+ }
+ }
+ }
+
// squiggly underline
for {
Text.Info(range, color) <-
@@ -315,6 +371,8 @@
{
text_area.getPainter.
addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
+ text_area.addFocusListener(focus_listener)
+ text_area.getPainter.addMouseMotionListener(mouse_motion_listener)
text_area.addCaretListener(caret_listener)
text_area.addLeftOfScrollBar(overview)
session.commands_changed += commands_changed_actor
@@ -323,8 +381,10 @@
private def deactivate()
{
session.commands_changed -= commands_changed_actor
+ text_area.removeFocusListener(focus_listener)
+ text_area.getPainter.removeMouseMotionListener(mouse_motion_listener)
+ text_area.removeCaretListener(caret_listener)
text_area.removeLeftOfScrollBar(overview)
- text_area.removeCaretListener(caret_listener)
text_area.getPainter.removeExtension(text_area_extension)
}
}
\ No newline at end of file
--- a/src/Tools/nbe.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/Tools/nbe.ML Mon Sep 06 12:38:45 2010 +0200
@@ -552,10 +552,11 @@
singleton (Type_Infer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
(try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0)
(Type_Infer.constrain ty' t);
- fun check_tvars t = if null (Term.add_tvars t []) then t else
- error ("Illegal schematic type variables in normalized term: "
- ^ setmp_CRITICAL show_types true (Syntax.string_of_term_global thy) t);
- val string_of_term = setmp_CRITICAL show_types true (Syntax.string_of_term_global thy);
+ val string_of_term =
+ Syntax.string_of_term (Config.put show_types true (Syntax.init_pretty_global thy));
+ fun check_tvars t =
+ if null (Term.add_tvars t []) then t
+ else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t);
in
compile_eval thy program (vs, t) deps
|> traced (fn t => "Normalized:\n" ^ string_of_term t)
--- a/src/Tools/quickcheck.ML Mon Sep 06 11:53:42 2010 +0200
+++ b/src/Tools/quickcheck.ML Mon Sep 06 12:38:45 2010 +0200
@@ -40,7 +40,7 @@
val _ =
ProofGeneralPgip.add_preference Preferences.category_tracing
- (setmp_CRITICAL auto true (fn () =>
+ (setmp_noncritical auto true (fn () =>
Preferences.bool_pref auto
"auto-quickcheck"
"Whether to run Quickcheck automatically.") ());