# HG changeset patch # User wenzelm # Date 1452264541 -3600 # Node ID 634838f919e411bf2145b60ed57be6784b45d87e # Parent 8463e386eaec350c3980b57dd7a542eeae6e1827# Parent 8d5f2e3e836d77a54573794aebbae8b41c4dfaa1 merged diff -r 8463e386eaec -r 634838f919e4 Admin/lib/Tools/makedist_bundle --- a/Admin/lib/Tools/makedist_bundle Thu Jan 07 17:42:01 2016 +0000 +++ b/Admin/lib/Tools/makedist_bundle Fri Jan 08 15:49:01 2016 +0100 @@ -325,6 +325,7 @@ find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" \ > "contrib/cygwin/isabelle/symlinks" + find . -type l -exec rm "{}" ";" touch "contrib/cygwin/isabelle/uninitialized" ) diff -r 8463e386eaec -r 634838f919e4 NEWS --- a/NEWS Thu Jan 07 17:42:01 2016 +0000 +++ b/NEWS Fri Jan 08 15:49:01 2016 +0100 @@ -443,12 +443,17 @@ * Inductive definitions ('inductive', 'coinductive', etc.) expose low-level facts of the internal construction only if the option -"inductive_defs" is enabled. This refers to the internal predicate +"inductive_internals" is enabled. This refers to the internal predicate definition and its monotonicity result. Rare INCOMPATIBILITY. * Recursive function definitions ('fun', 'function', 'partial_function') expose low-level facts of the internal construction only if the option -"function_defs" is enabled. Rare INCOMPATIBILITY. +"function_internals" is enabled. Rare INCOMPATIBILITY. + +* BNF datatypes ('datatype', 'codatatype', etc.) expose low-level facts +of the internal construction only if the option "bnf_internals" is +enabled. This supersedes the former option "bnf_note_all". Rare +INCOMPATIBILITY. * Combinator to represent case distinction on products is named "case_prod", uniformly, discontinuing any input aliasses. Very popular diff -r 8463e386eaec -r 634838f919e4 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Thu Jan 07 17:42:01 2016 +0000 +++ b/src/Doc/Datatypes/Datatypes.thy Fri Jan 08 15:49:01 2016 +0100 @@ -693,9 +693,9 @@ the line \ - declare [[bnf_note_all]] + declare [[bnf_internals]] (*<*) - declare [[bnf_note_all = false]] + declare [[bnf_internals = false]] (*>*) text \ diff -r 8463e386eaec -r 634838f919e4 src/HOL/Complete_Partial_Order.thy --- a/src/HOL/Complete_Partial_Order.thy Thu Jan 07 17:42:01 2016 +0000 +++ b/src/HOL/Complete_Partial_Order.thy Fri Jan 08 15:49:01 2016 +0100 @@ -87,7 +87,7 @@ subsection \Transfinite iteration of a function\ -context notes [[inductive_defs]] begin +context notes [[inductive_internals]] begin inductive_set iterates :: "('a \ 'a) \ 'a set" for f :: "'a \ 'a" diff -r 8463e386eaec -r 634838f919e4 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Thu Jan 07 17:42:01 2016 +0000 +++ b/src/HOL/Finite_Set.thy Fri Jan 08 15:49:01 2016 +0100 @@ -12,7 +12,7 @@ subsection \Predicate for finite sets\ context - notes [[inductive_defs]] + notes [[inductive_internals]] begin inductive finite :: "'a set \ bool" diff -r 8463e386eaec -r 634838f919e4 src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy --- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Thu Jan 07 17:42:01 2016 +0000 +++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Fri Jan 08 15:49:01 2016 +0100 @@ -65,7 +65,7 @@ "s \ P \ HLD s aand nxt P" context - notes [[inductive_defs]] + notes [[inductive_internals]] begin inductive ev for \ where @@ -594,7 +594,7 @@ text \Strong until\ context - notes [[inductive_defs]] + notes [[inductive_internals]] begin inductive suntil (infix "suntil" 60) for \ \ where diff -r 8463e386eaec -r 634838f919e4 src/HOL/Library/RBT_Impl.thy --- a/src/HOL/Library/RBT_Impl.thy Thu Jan 07 17:42:01 2016 +0000 +++ b/src/HOL/Library/RBT_Impl.thy Fri Jan 08 15:49:01 2016 +0100 @@ -1758,9 +1758,7 @@ Rep_compare Rep_compare_cases Rep_compare_induct Rep_compare_inject Rep_compare_inverse compare.simps compare.exhaust compare.induct compare.rec compare.simps compare.size compare.case_cong compare.case_cong_weak compare.case - compare.nchotomy compare.split compare.split_asm rec_compare_def - compare.eq.refl compare.eq.simps - compare.EQ_def compare.GT_def compare.LT_def + compare.nchotomy compare.split compare.split_asm compare.eq.refl compare.eq.simps equal_compare_def skip_red.simps skip_red.cases skip_red.induct skip_black_def diff -r 8463e386eaec -r 634838f919e4 src/HOL/Library/Stream.thy --- a/src/HOL/Library/Stream.thy Thu Jan 07 17:42:01 2016 +0000 +++ b/src/HOL/Library/Stream.thy Fri Jan 08 15:49:01 2016 +0100 @@ -69,7 +69,7 @@ subsection \set of streams with elements in some fixed set\ context - notes [[inductive_defs]] + notes [[inductive_internals]] begin coinductive_set diff -r 8463e386eaec -r 634838f919e4 src/HOL/List.thy --- a/src/HOL/List.thy Thu Jan 07 17:42:01 2016 +0000 +++ b/src/HOL/List.thy Fri Jan 08 15:49:01 2016 +0100 @@ -5586,7 +5586,7 @@ begin context - notes [[inductive_defs]] + notes [[inductive_internals]] begin inductive lexordp :: "'a list \ 'a list \ bool" diff -r 8463e386eaec -r 634838f919e4 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Jan 07 17:42:01 2016 +0000 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Jan 08 15:49:01 2016 +0100 @@ -5976,7 +5976,7 @@ (is "?int = convex hull ?points") proof - have One[simp]: "\i. i \ Basis \ One \ i = 1" - by (simp add: One_def inner_setsum_left setsum.If_cases inner_Basis) + by (simp add: inner_setsum_left setsum.If_cases inner_Basis) have "?int = {x. \i\Basis. x \ i \ cbox 0 1}" by (auto simp: cbox_def) also have "\ = (\i\Basis. (\x. x *\<^sub>R i) ` cbox 0 1)" diff -r 8463e386eaec -r 634838f919e4 src/HOL/Probability/Bochner_Integration.thy --- a/src/HOL/Probability/Bochner_Integration.thy Thu Jan 07 17:42:01 2016 +0000 +++ b/src/HOL/Probability/Bochner_Integration.thy Fri Jan 08 15:49:01 2016 +0100 @@ -887,7 +887,7 @@ qed context - notes [[inductive_defs]] + notes [[inductive_internals]] begin inductive integrable for M f where diff -r 8463e386eaec -r 634838f919e4 src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Thu Jan 07 17:42:01 2016 +0000 +++ b/src/HOL/Tools/BNF/bnf_def.ML Fri Jan 08 15:49:01 2016 +0100 @@ -119,7 +119,7 @@ datatype inline_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline datatype fact_policy = Dont_Note | Note_Some | Note_All - val bnf_note_all: bool Config.T + val bnf_internals: bool Config.T val bnf_timing: bool Config.T val user_policy: fact_policy -> Proof.context -> fact_policy val note_bnf_thms: fact_policy -> (binding -> binding) -> binding -> bnf -> Proof.context -> @@ -725,10 +725,10 @@ datatype fact_policy = Dont_Note | Note_Some | Note_All; -val bnf_note_all = Attrib.setup_config_bool @{binding bnf_note_all} (K false); +val bnf_internals = Attrib.setup_config_bool @{binding bnf_internals} (K false); val bnf_timing = Attrib.setup_config_bool @{binding bnf_timing} (K false); -fun user_policy policy ctxt = if Config.get ctxt bnf_note_all then Note_All else policy; +fun user_policy policy ctxt = if Config.get ctxt bnf_internals then Note_All else policy; val smart_max_inline_term_size = 25; (*FUDGE*) diff -r 8463e386eaec -r 634838f919e4 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Jan 07 17:42:01 2016 +0000 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Jan 08 15:49:01 2016 +0100 @@ -1283,12 +1283,10 @@ let val thy = Proof_Context.theory_of lthy0; - val maybe_conceal_def_binding = Thm.def_binding - #> not (Config.get lthy0 bnf_note_all) ? Binding.concealed; - val ((cst, (_, def)), (lthy', lthy)) = lthy0 |> Local_Theory.open_target |> snd - |> Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs)) + |> Local_Theory.define + ((b, NoSyn), ((Thm.make_def_binding (Config.get lthy0 bnf_internals) b, []), rhs)) ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy lthy'; @@ -2201,14 +2199,12 @@ map2 (fn k => fn xs => fold_rev Term.lambda xs (ctor $ mk_absumprod ctr_absT abs n k xs)) ks xss; - val maybe_conceal_def_binding = Thm.def_binding - #> not (Config.get no_defs_lthy bnf_note_all) ? Binding.concealed; - val ((raw_ctrs, raw_ctr_defs), (lthy', lthy)) = no_defs_lthy |> Local_Theory.open_target |> snd |> apfst split_list o @{fold_map 3} (fn b => fn mx => fn rhs => - Local_Theory.define ((b, mx), ((maybe_conceal_def_binding b, []), rhs)) #>> apsnd snd) - ctr_bindings ctr_mixfixes ctr_rhss + Local_Theory.define + ((b, mx), ((Thm.make_def_binding (Config.get no_defs_lthy bnf_internals) b, []), rhs)) + #>> apsnd snd) ctr_bindings ctr_mixfixes ctr_rhss ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy lthy'; diff -r 8463e386eaec -r 634838f919e4 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Jan 07 17:42:01 2016 +0000 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Jan 08 15:49:01 2016 +0100 @@ -646,7 +646,7 @@ val Dss = @{map 3} (uncurry append oo curry swap oo map o nth) livess kill_poss deadss; fun pre_qualify b = Binding.qualify false (Binding.name_of b) - #> not (Config.get lthy' bnf_note_all) ? Binding.concealed; + #> not (Config.get lthy' bnf_internals) ? Binding.concealed; val ((pre_bnfs, (deadss, absT_infos)), lthy'') = @{fold_map 4} (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b)) diff -r 8463e386eaec -r 634838f919e4 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Thu Jan 07 17:42:01 2016 +0000 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Fri Jan 08 15:49:01 2016 +0100 @@ -66,7 +66,7 @@ val m = live - n; (*passive, if 0 don't generate a new BNF*) val ls = 1 upto m; - val note_all = Config.get lthy bnf_note_all; + val internals = Config.get lthy bnf_internals; val b_names = map Binding.name_of bs; val b_name = mk_common_name b_names; val b = Binding.name b_name; @@ -76,7 +76,7 @@ fun mk_internal_b name = mk_internal_of_b name b; fun mk_internal_bs name = map (mk_internal_of_b name) bs; val external_bs = map2 (Binding.prefix false) b_names bs - |> not note_all ? map Binding.concealed; + |> not internals ? map Binding.concealed; val deads = fold (union (op =)) Dss resDs; val names_lthy = fold Variable.declare_typ deads lthy; @@ -2680,7 +2680,7 @@ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) bs thmss); - val lthy' = lthy |> note_all ? snd o Local_Theory.notes (common_notes @ notes @ Jbnf_notes); + val lthy' = lthy |> internals ? snd o Local_Theory.notes (common_notes @ notes @ Jbnf_notes); val fp_res = {Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_un_folds = unfolds, diff -r 8463e386eaec -r 634838f919e4 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Thu Jan 07 17:42:01 2016 +0000 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Fri Jan 08 15:49:01 2016 +0100 @@ -36,7 +36,7 @@ val ks = 1 upto n; val m = live - n; (*passive, if 0 don't generate a new BNF*) - val note_all = Config.get lthy bnf_note_all; + val internals = Config.get lthy bnf_internals; val b_names = map Binding.name_of bs; val b_name = mk_common_name b_names; val b = Binding.name b_name; @@ -46,7 +46,7 @@ fun mk_internal_b name = mk_internal_of_b name b; fun mk_internal_bs name = map (mk_internal_of_b name) bs; val external_bs = map2 (Binding.prefix false) b_names bs - |> not note_all ? map Binding.concealed; + |> not internals ? map Binding.concealed; val deads = fold (union (op =)) Dss resDs; val names_lthy = fold Variable.declare_typ deads lthy; @@ -1940,7 +1940,7 @@ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) bs thmss); - val lthy' = lthy |> note_all ? snd o Local_Theory.notes (common_notes @ notes @ Ibnf_notes); + val lthy' = lthy |> internals ? snd o Local_Theory.notes (common_notes @ notes @ Ibnf_notes); val fp_res = {Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_un_folds = folds, diff -r 8463e386eaec -r 634838f919e4 src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Thu Jan 07 17:42:01 2016 +0000 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Jan 08 15:49:01 2016 +0100 @@ -200,7 +200,7 @@ #>> (fn args => fold_rev Term.lambda fs (Term.list_comb (substCnatT recx, args))); val maybe_conceal_def_binding = Thm.def_binding - #> not (Config.get lthy0 bnf_note_all) ? Binding.concealed; + #> not (Config.get lthy0 bnf_internals) ? Binding.concealed; val (size_rhss, nested_size_gen_o_mapss) = fold_map mk_size_rhs recs []; val size_Ts = map fastype_of size_rhss; diff -r 8463e386eaec -r 634838f919e4 src/HOL/Tools/Function/function_core.ML --- a/src/HOL/Tools/Function/function_core.ML Thu Jan 07 17:42:01 2016 +0000 +++ b/src/HOL/Tools/Function/function_core.ML Fri Jan 08 15:49:01 2016 +0100 @@ -499,7 +499,7 @@ $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0)) |> Syntax.check_term lthy val def_binding = - if Config.get lthy function_defs then (Binding.name fdefname, []) + if Config.get lthy function_internals then (Binding.name fdefname, []) else Attrib.empty_binding in Local_Theory.define diff -r 8463e386eaec -r 634838f919e4 src/HOL/Tools/Function/function_lib.ML --- a/src/HOL/Tools/Function/function_lib.ML Thu Jan 07 17:42:01 2016 +0000 +++ b/src/HOL/Tools/Function/function_lib.ML Fri Jan 08 15:49:01 2016 +0100 @@ -7,7 +7,7 @@ signature FUNCTION_LIB = sig - val function_defs: bool Config.T + val function_internals: bool Config.T val plural: string -> string -> 'a list -> string @@ -32,7 +32,7 @@ structure Function_Lib: FUNCTION_LIB = struct -val function_defs = Attrib.setup_config_bool @{binding function_defs} (K false) +val function_internals = Attrib.setup_config_bool @{binding function_internals} (K false) (* "The variable" ^ plural " is" "s are" vs *) diff -r 8463e386eaec -r 634838f919e4 src/HOL/Tools/Function/mutual.ML --- a/src/HOL/Tools/Function/mutual.ML Thu Jan 07 17:42:01 2016 +0000 +++ b/src/HOL/Tools/Function/mutual.ML Fri Jan 08 15:49:01 2016 +0100 @@ -129,7 +129,7 @@ fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy = let val def_binding = - if Config.get lthy function_defs then (Binding.name (Thm.def_name fname), []) + if Config.get lthy function_internals then (Binding.name (Thm.def_name fname), []) else Attrib.empty_binding val ((f, (_, f_defthm)), lthy') = Local_Theory.define diff -r 8463e386eaec -r 634838f919e4 src/HOL/Tools/Function/partial_function.ML --- a/src/HOL/Tools/Function/partial_function.ML Thu Jan 07 17:42:01 2016 +0000 +++ b/src/HOL/Tools/Function/partial_function.ML Fri Jan 08 15:49:01 2016 +0100 @@ -257,7 +257,8 @@ val f_def_rhs = curry_n arity (apply_inst lthy fixp F_uc); val f_def_binding = - if Config.get lthy Function_Lib.function_defs then (Binding.name (Thm.def_name fname), []) + if Config.get lthy Function_Lib.function_internals + then (Binding.name (Thm.def_name fname), []) else Attrib.empty_binding; val ((f, (_, f_def)), lthy') = Local_Theory.define ((f_binding, mixfix), (f_def_binding, f_def_rhs)) lthy; diff -r 8463e386eaec -r 634838f919e4 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Jan 07 17:42:01 2016 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jan 08 15:49:01 2016 +0100 @@ -23,7 +23,7 @@ val fact_of_ref : Proof.context -> Keyword.keywords -> thm list -> status Termtab.table -> Facts.ref * Token.src list -> ((string * stature) * thm) list - val backquote_thm : Proof.context -> thm -> string + val cartouche_thm : Proof.context -> thm -> string val is_blacklisted_or_something : Proof.context -> bool -> string -> bool val clasimpset_rule_table_of : Proof.context -> status Termtab.table val build_name_tables : (thm -> string) -> ('a * thm) list -> @@ -81,11 +81,6 @@ | explode_interval max (Facts.From i) = i upto i + max - 1 | explode_interval _ (Facts.Single i) = [i] -val backquote = enclose "\" "\" - -(* unfolding these can yield really huge terms *) -val risky_defs = @{thms Bit0_def Bit1_def} - fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs)) fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t @@ -168,7 +163,7 @@ fun nth_name j = (case xref of - Facts.Fact s => backquote (simplify_spaces (YXML.content_of s)) ^ bracket + Facts.Fact s => cartouche (simplify_spaces (YXML.content_of s)) ^ bracket | Facts.Named (("", _), _) => "[" ^ bracket ^ "]" | Facts.Named ((name, _), NONE) => make_name keywords (length ths > 1) (j + 1) name ^ bracket | Facts.Named ((name, _), SOME intervals) => @@ -301,8 +296,8 @@ (Term.add_vars t [] |> sort_by (fst o fst)) |> fst -fun backquote_term ctxt = close_form #> hackish_string_of_term ctxt #> backquote -fun backquote_thm ctxt = backquote_term ctxt o Thm.prop_of +fun cartouche_term ctxt = close_form #> hackish_string_of_term ctxt #> cartouche +fun cartouche_thm ctxt = cartouche_term ctxt o Thm.prop_of (* TODO: rewrite to use nets and/or to reuse existing data structures *) fun clasimpset_rule_table_of ctxt = @@ -324,7 +319,6 @@ val (rec_defs, nonrec_defs) = specs |> filter (curry (op =) Spec_Rules.Equational o fst) |> maps (snd o snd) - |> filter_out (member Thm.eq_thm_prop risky_defs) |> List.partition (is_rec_def o Thm.prop_of) val spec_intros = specs |> filter (member (op =) [Spec_Rules.Inductive, Spec_Rules.Co_Inductive] o fst) @@ -509,7 +503,7 @@ let fun get_name () = if name0 = "" orelse name0 = local_thisN then - backquote_thm ctxt th + cartouche_thm ctxt th else let val short_name = Facts.extern ctxt facts name0 in if check_thms short_name then diff -r 8463e386eaec -r 634838f919e4 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Thu Jan 07 17:42:01 2016 +0000 +++ b/src/HOL/Tools/inductive.ML Fri Jan 08 15:49:01 2016 +0100 @@ -71,7 +71,7 @@ signature INDUCTIVE = sig include BASIC_INDUCTIVE - val inductive_defs: bool Config.T + val inductive_internals: bool Config.T val select_disj_tac: Proof.context -> int -> int -> int -> tactic type add_ind_def = inductive_flags -> @@ -122,7 +122,7 @@ (** misc utilities **) -val inductive_defs = Attrib.setup_config_bool @{binding inductive_defs} (K false); +val inductive_internals = Attrib.setup_config_bool @{binding inductive_internals} (K false); fun message quiet_mode s = if quiet_mode then () else writeln s; @@ -849,16 +849,13 @@ else alt_name; val rec_name = Binding.name_of rec_binding; - val inductive_defs = Config.get lthy inductive_defs; - fun cond_def_binding b = - if inductive_defs then Binding.reset_pos (Thm.def_binding b) - else Binding.empty; + val internals = Config.get lthy inductive_internals; val ((rec_const, (_, fp_def)), lthy') = lthy |> is_auxiliary ? Proof_Context.concealed |> Local_Theory.define ((rec_binding, case cnames_syn of [(_, mx)] => mx | _ => NoSyn), - ((cond_def_binding rec_binding, @{attributes [nitpick_unfold]}), + ((Thm.make_def_binding internals rec_binding, @{attributes [nitpick_unfold]}), fold_rev lambda params (Const (fp_name, (predT --> predT) --> predT) $ fp_fun))) ||> Proof_Context.restore_naming lthy; @@ -874,7 +871,7 @@ map Free (Variable.variant_frees lthy' intr_ts (mk_names "x" (length Ts) ~~ Ts)); in ((b, mx), - ((cond_def_binding b, []), fold_rev lambda (params @ xs) + ((Thm.make_def_binding internals b, []), fold_rev lambda (params @ xs) (list_comb (rec_const, params @ make_bool_args' bs i @ make_args argTs (xs ~~ Ts))))) end) (cnames_syn ~~ cs) @@ -887,7 +884,7 @@ val mono = prove_mono quiet_mode skip_mono predT fp_fun monos ctxt''; val (_, lthy''') = lthy'' |> Local_Theory.note - ((if inductive_defs + ((if internals then Binding.qualify true rec_name (Binding.name "mono") else Binding.empty, []), Proof_Context.export ctxt'' lthy'' [mono]); diff -r 8463e386eaec -r 634838f919e4 src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Thu Jan 07 17:42:01 2016 +0000 +++ b/src/HOL/Transitive_Closure.thy Fri Jan 08 15:49:01 2016 +0100 @@ -21,7 +21,7 @@ \ context - notes [[inductive_defs]] + notes [[inductive_internals]] begin inductive_set rtrancl :: "('a \ 'a) set \ ('a \ 'a) set" ("(_\<^sup>*)" [1000] 999) diff -r 8463e386eaec -r 634838f919e4 src/Pure/General/pretty.ML --- a/src/Pure/General/pretty.ML Thu Jan 07 17:42:01 2016 +0000 +++ b/src/Pure/General/pretty.ML Fri Jan 08 15:49:01 2016 +0100 @@ -45,7 +45,6 @@ val paragraph: T list -> T val para: string -> T val quote: T -> T - val backquote: T -> T val cartouche: T -> T val separate: string -> T list -> T list val commas: T list -> T list @@ -168,7 +167,6 @@ val para = paragraph o text; fun quote prt = blk (1, [str "\"", prt, str "\""]); -fun backquote prt = blk (1, [str "`", prt, str "`"]); fun cartouche prt = blk (1, [str "\\", prt, str "\\"]); fun separate sep prts = diff -r 8463e386eaec -r 634838f919e4 src/Pure/Isar/bundle.ML --- a/src/Pure/Isar/bundle.ML Thu Jan 07 17:42:01 2016 +0000 +++ b/src/Pure/Isar/bundle.ML Fri Jan 08 15:49:01 2016 +0100 @@ -124,7 +124,7 @@ fun print_bundles verbose ctxt = let - val prt_thm = Pretty.backquote o Thm.pretty_thm ctxt; + val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt; fun prt_fact (ths, []) = map prt_thm ths | prt_fact (ths, atts) = Pretty.enclose "(" ")" diff -r 8463e386eaec -r 634838f919e4 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Thu Jan 07 17:42:01 2016 +0000 +++ b/src/Pure/Isar/element.ML Fri Jan 08 15:49:01 2016 +0100 @@ -152,7 +152,7 @@ let val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt; val prt_term = Pretty.quote o Syntax.pretty_term ctxt; - val prt_thm = Pretty.backquote o Thm.pretty_thm ctxt; + val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt; fun prt_binding (b, atts) = Attrib.pretty_binding ctxt (b, if show_attribs then atts else []); diff -r 8463e386eaec -r 634838f919e4 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Thu Jan 07 17:42:01 2016 +0000 +++ b/src/Pure/Isar/token.ML Fri Jan 08 15:49:01 2016 +0100 @@ -471,7 +471,7 @@ | SOME (Typ T) => Syntax.pretty_typ ctxt T | SOME (Term t) => Syntax.pretty_term ctxt t | SOME (Fact (_, ths)) => - Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.backquote o Thm.pretty_thm ctxt) ths)) + Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.cartouche o Thm.pretty_thm ctxt) ths)) | _ => Pretty.marks_str (markups Keyword.empty_keywords tok, unparse tok)); diff -r 8463e386eaec -r 634838f919e4 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Thu Jan 07 17:42:01 2016 +0000 +++ b/src/Pure/more_thm.ML Fri Jan 08 15:49:01 2016 +0100 @@ -92,6 +92,7 @@ val def_name_optional: string -> string -> string val def_binding: Binding.binding -> Binding.binding val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding + val make_def_binding: bool -> Binding.binding -> Binding.binding val has_name_hint: thm -> bool val get_name_hint: thm -> string val put_name_hint: string -> thm -> thm @@ -570,6 +571,9 @@ fun def_binding_optional b name = if Binding.is_empty name then def_binding b else name; +fun make_def_binding cond b = + if cond then Binding.reset_pos (def_binding b) else Binding.empty; + (* unofficial theorem names *) diff -r 8463e386eaec -r 634838f919e4 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Thu Jan 07 17:42:01 2016 +0000 +++ b/src/Tools/jEdit/src/document_view.scala Fri Jan 08 15:49:01 2016 +0100 @@ -256,7 +256,7 @@ text_area.getGutter.addExtension(gutter_painter) text_area.addKeyListener(key_listener) text_area.addCaretListener(caret_listener) - text_area.addLeftOfScrollBar(overview) + text_area.addLeftOfScrollBar(overview); text_area.revalidate(); text_area.repaint() Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)). foreach(text_area.addStructureMatcher(_)) session.raw_edits += main @@ -271,7 +271,7 @@ session.commands_changed -= main Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)). foreach(text_area.removeStructureMatcher(_)) - text_area.removeLeftOfScrollBar(overview); overview.revoke() + overview.revoke(); text_area.removeLeftOfScrollBar(overview) text_area.removeCaretListener(caret_listener); delay_caret_update.revoke() text_area.removeKeyListener(key_listener) text_area.getGutter.removeExtension(gutter_painter) diff -r 8463e386eaec -r 634838f919e4 src/Tools/jEdit/src/text_overview.scala --- a/src/Tools/jEdit/src/text_overview.scala Thu Jan 07 17:42:01 2016 +0000 +++ b/src/Tools/jEdit/src/text_overview.scala Fri Jan 08 15:49:01 2016 +0100 @@ -82,7 +82,13 @@ val rendering = doc_view.get_rendering() val overview = get_overview() - if (!rendering.snapshot.is_outdated && overview == current_overview) { + if (rendering.snapshot.is_outdated || overview != current_overview) { + invoke() + + gfx.setColor(rendering.outdated_color) + gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds) + } + else { gfx.setColor(getBackground) gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds) for ((color, h, h1) <- current_colors) { @@ -90,10 +96,6 @@ gfx.fillRect(0, h, getWidth, h1 - h) } } - else { - gfx.setColor(rendering.outdated_color) - gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds) - } } } }