# HG changeset patch # User wenzelm # Date 1283769525 -7200 # Node ID 14b16b380ca18c5535eb9cd811e2635d65a0b885 # Parent b1c2c03fd9d702a3f9640258dde2578d6abe726e# Parent 8a2fb4ce1f3907d0fed63b4ad74a073ec65560dd merged; diff -r b1c2c03fd9d7 -r 14b16b380ca1 NEWS --- 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 diff -r b1c2c03fd9d7 -r 14b16b380ca1 doc-src/IsarRef/Thy/Inner_Syntax.thy --- 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} \\ diff -r b1c2c03fd9d7 -r 14b16b380ca1 doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- 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| \\ diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/HOL/Groups.thy --- 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; diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/HOL/Import/proof_kernel.ML --- 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 diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/HOL/Mutabelle/mutabelle_extra.ML --- 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 diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/HOL/Statespace/state_space.ML --- 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 => diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/HOL/Tools/Function/function_common.ML --- 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 diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/HOL/Tools/Nitpick/nitpick_util.ML --- 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 diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- 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 ^ " :: " ^ diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/HOL/Tools/numeral_syntax.ML --- 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; diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/HOL/Tools/record.ML --- 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 diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/HOL/ex/Numeral.thy --- 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 diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/Pure/Isar/attrib.ML --- 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 #> diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/Pure/Isar/class.ML --- 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 =) diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/Pure/Isar/code.ML --- 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) diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/Pure/Isar/local_defs.ML --- 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; diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/Pure/Isar/locale.ML --- 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; diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/Pure/Isar/obtain.ML --- 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); diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/Pure/Isar/proof_context.ML --- 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; diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/Pure/ML/ml_context.ML --- 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); diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/Pure/ProofGeneral/preferences.ML --- 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") (), diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/Pure/ProofGeneral/proof_general_pgip.ML --- 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 diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/Pure/Syntax/printer.ML --- 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)) diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/Pure/Syntax/syntax.ML --- 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; diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/Pure/Thy/thy_output.ML --- 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); diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/Pure/axclass.ML --- 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; diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/Pure/goal_display.ML --- 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 = diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/Pure/more_thm.ML --- 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); diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/Pure/sign.ML --- 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); diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/Pure/theory.ML --- 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; diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/Tools/Code/code_preproc.ML --- 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'; diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/Tools/auto_solve.ML --- 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.") ()); diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/Tools/jEdit/src/jedit/document_view.scala --- 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 diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/Tools/nbe.ML --- 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) diff -r b1c2c03fd9d7 -r 14b16b380ca1 src/Tools/quickcheck.ML --- 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.") ());