--- a/NEWS Tue Feb 18 17:52:28 2014 +0100
+++ b/NEWS Tue Feb 18 23:08:55 2014 +0100
@@ -358,6 +358,13 @@
pass runtime Proof.context (and ensure that the simplified entity
actually belongs to it).
+* Subtle change of semantics of Thm.eq_thm: theory stamps are not
+compared (according to Thm.thm_ord), but assumed to be covered by the
+current background theory. Thus equivalent data produced in different
+branches of the theory graph usually coincides (e.g. relevant for
+theory merge). Note that the softer Thm.eq_thm_prop is often more
+appropriate than Thm.eq_thm.
+
*** System ***
--- a/etc/symbols Tue Feb 18 17:52:28 2014 +0100
+++ b/etc/symbols Tue Feb 18 23:08:55 2014 +0100
@@ -350,6 +350,7 @@
\<newline> code: 0x0023ce
\<open> code: 0x002039 group: punctuation font: IsabelleText abbrev: <<
\<close> code: 0x00203a group: punctuation font: IsabelleText abbrev: >>
+\<here> code: 0x002302 font: IsabelleText
\<^sub> code: 0x0021e9 group: control font: IsabelleText
\<^sup> code: 0x0021e7 group: control font: IsabelleText
\<^bold> code: 0x002759 group: control font: IsabelleText
--- a/lib/fonts/IsabelleText.sfd Tue Feb 18 17:52:28 2014 +0100
+++ b/lib/fonts/IsabelleText.sfd Tue Feb 18 23:08:55 2014 +0100
@@ -19,7 +19,7 @@
OS2_WeightWidthSlopeOnly: 0
OS2_UseTypoMetrics: 1
CreationTime: 1050361371
-ModificationTime: 1389823475
+ModificationTime: 1392668982
PfmFamily: 17
TTFWeight: 400
TTFWidth: 5
@@ -2240,9 +2240,9 @@
DisplaySize: -48
AntiAlias: 1
FitToEm: 1
-WinInfo: 9104 16 10
+WinInfo: 8912 16 10
TeXData: 1 0 0 631296 315648 210432 572416 -1048576 210432 783286 444596 497025 792723 393216 433062 380633 303038 157286 324010 404750 52429 2506097 1059062 262144
-BeginChars: 1114189 1095
+BeginChars: 1114189 1096
StartChar: u10000
Encoding: 65536 65536 0
@@ -55572,5 +55572,27 @@
893 663 l 1,9,-1
EndSplineSet
EndChar
+
+StartChar: house
+Encoding: 8962 8962 1095
+Width: 1233
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+146.5 0 m 9,0,-1
+ 146.5 647 l 25,1,-1
+ 616 1220 l 25,2,-1
+ 1086.5 647 l 25,3,-1
+ 1086.5 0 l 17,4,-1
+ 146.5 0 l 9,0,-1
+268.5 122 m 17,5,-1
+ 964.5 122 l 9,6,-1
+ 964.5 591 l 25,7,-1
+ 616 1018 l 25,8,-1
+ 268.5 591 l 25,9,-1
+ 268.5 122 l 17,5,-1
+EndSplineSet
+EndChar
EndChars
EndSplineFont
Binary file lib/fonts/IsabelleText.ttf has changed
--- a/lib/fonts/IsabelleTextBold.sfd Tue Feb 18 17:52:28 2014 +0100
+++ b/lib/fonts/IsabelleTextBold.sfd Tue Feb 18 23:08:55 2014 +0100
@@ -19,7 +19,7 @@
OS2_WeightWidthSlopeOnly: 0
OS2_UseTypoMetrics: 1
CreationTime: 1050374980
-ModificationTime: 1389823579
+ModificationTime: 1392669044
PfmFamily: 17
TTFWeight: 700
TTFWidth: 5
@@ -1674,8 +1674,8 @@
DisplaySize: -48
AntiAlias: 1
FitToEm: 1
-WinInfo: 9072 16 10
-BeginChars: 1114112 1084
+WinInfo: 8928 16 10
+BeginChars: 1114112 1085
StartChar: u10000
Encoding: 65536 65536 0
@@ -58502,5 +58502,27 @@
1067 1072 l 1,9,-1
EndSplineSet
EndChar
+
+StartChar: house
+Encoding: 8962 8962 1084
+Width: 1233
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+110 0 m 9,0,-1
+ 110 682 l 25,1,-1
+ 616 1220 l 25,2,-1
+ 1123 682 l 25,3,-1
+ 1123 0 l 17,4,-1
+ 110 0 l 9,0,-1
+298 187 m 17,5,-1
+ 935 187 l 9,6,-1
+ 935 625 l 25,7,-1
+ 616 959 l 25,8,-1
+ 298 625 l 25,9,-1
+ 298 187 l 17,5,-1
+EndSplineSet
+EndChar
EndChars
EndSplineFont
Binary file lib/fonts/IsabelleTextBold.ttf has changed
--- a/src/Doc/IsarImplementation/Tactic.thy Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Doc/IsarImplementation/Tactic.thy Tue Feb 18 23:08:55 2014 +0100
@@ -920,9 +920,8 @@
"thm"} has fewer than @{text "n"} premises.
\item @{ML Thm.eq_thm}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether @{text
- "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal. Both theorems must have
- compatible background theories. Both theorems must have the same
- conclusions, the same set of hypotheses, and the same set of sort
+ "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal. Both theorems must have the
+ same conclusions, the same set of hypotheses, and the same set of sort
hypotheses. Names of bound variables are ignored as usual.
\item @{ML Thm.eq_thm_prop}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether
--- a/src/Doc/IsarRef/HOL_Specific.thy Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Doc/IsarRef/HOL_Specific.thy Tue Feb 18 23:08:55 2014 +0100
@@ -1761,7 +1761,7 @@
"~~/src/HOL/List.thy"} or Lifting_*.thy files in the same directory.
\item @{attribute (HOL) reflexivity_rule} registers a theorem that shows
- that a relator respects reflexivity, left-totality and left_uniqueness. For examples
+ that a relator respects left-totality and left_uniqueness. For examples
see @{file "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"} or Lifting_*.thy files
in the same directory.
The property is used in a reflexivity prover, which is used for discharging respectfulness
--- a/src/HOL/BNF_GFP.thy Tue Feb 18 17:52:28 2014 +0100
+++ b/src/HOL/BNF_GFP.thy Tue Feb 18 23:08:55 2014 +0100
@@ -51,21 +51,6 @@
(* Operators: *)
definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
-lemma Id_onD: "(a, b) \<in> Id_on A \<Longrightarrow> a = b"
-unfolding Id_on_def by simp
-
-lemma Id_onD': "x \<in> Id_on A \<Longrightarrow> fst x = snd x"
-unfolding Id_on_def by auto
-
-lemma Id_on_fst: "x \<in> Id_on A \<Longrightarrow> fst x \<in> A"
-unfolding Id_on_def by auto
-
-lemma Id_on_UNIV: "Id_on UNIV = Id"
-unfolding Id_on_def by auto
-
-lemma Id_on_Comp: "Id_on A = Id_on A O Id_on A"
-unfolding Id_on_def by auto
-
lemma Id_on_Gr: "Id_on A = Gr A id"
unfolding Id_on_def Gr_def by auto
@@ -102,9 +87,6 @@
lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (split (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
by force
-lemma Collect_split_in_relI: "x \<in> X \<Longrightarrow> x \<in> Collect (split (in_rel X))"
-by auto
-
lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
unfolding fun_eq_iff by auto
@@ -114,9 +96,6 @@
lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f"
unfolding Gr_def Grp_def fun_eq_iff by auto
-lemma in_rel_Id_on_UNIV: "in_rel (Id_on UNIV) = op ="
-unfolding fun_eq_iff by auto
-
definition relImage where
"relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
--- a/src/HOL/IMP/Abs_Int2_ivl.thy Tue Feb 18 17:52:28 2014 +0100
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy Tue Feb 18 23:08:55 2014 +0100
@@ -30,8 +30,7 @@
lemma \<gamma>_ivl_nice: "\<gamma>_ivl[l,h] = {i. l \<le> Fin i \<and> Fin i \<le> h}"
by transfer (simp add: \<gamma>_rep_def)
-lift_definition num_ivl :: "int \<Rightarrow> ivl" is "\<lambda>i. (Fin i, Fin i)"
-by(auto simp: eq_ivl_def)
+lift_definition num_ivl :: "int \<Rightarrow> ivl" is "\<lambda>i. (Fin i, Fin i)" .
lift_definition in_ivl :: "int \<Rightarrow> ivl \<Rightarrow> bool"
is "\<lambda>i (l,h). l \<le> Fin i \<and> Fin i \<le> h"
--- a/src/HOL/Library/Countable_Set_Type.thy Tue Feb 18 17:52:28 2014 +0100
+++ b/src/HOL/Library/Countable_Set_Type.thy Tue Feb 18 23:08:55 2014 +0100
@@ -69,7 +69,7 @@
rcset[Transfer.transferred, unfolded mem_Collect_eq, simp]
lift_definition cin :: "'a \<Rightarrow> 'a cset \<Rightarrow> bool" is "op \<in>" parametric member_transfer
- ..
+ .
lift_definition cempty :: "'a cset" is "{}" parametric empty_transfer
by (rule countable_empty)
lift_definition cinsert :: "'a \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is insert parametric Lifting_Set.insert_transfer
--- a/src/HOL/Library/DAList.thy Tue Feb 18 17:52:28 2014 +0100
+++ b/src/HOL/Library/DAList.thy Tue Feb 18 23:08:55 2014 +0100
@@ -39,7 +39,7 @@
subsection {* Primitive operations *}
-lift_definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option" is map_of ..
+lift_definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option" is map_of .
lift_definition empty :: "('key, 'value) alist" is "[]" by simp
--- a/src/HOL/Library/FSet.thy Tue Feb 18 17:52:28 2014 +0100
+++ b/src/HOL/Library/FSet.thy Tue Feb 18 23:08:55 2014 +0100
@@ -34,7 +34,7 @@
lift_definition bot_fset :: "'a fset" is "{}" parametric empty_transfer by simp
lift_definition less_eq_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" is subset_eq parametric subset_transfer
- by simp
+ .
definition less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a fset)"
@@ -164,7 +164,7 @@
"{|x|}" == "CONST finsert x {||}"
lift_definition fmember :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) is Set.member
- parametric member_transfer by simp
+ parametric member_transfer .
abbreviation notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) where "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
@@ -187,12 +187,12 @@
by (subst compose_rel_to_Domainp [OF _ finite_transfer]) (auto intro: transfer_raw finite_subset
simp add: fset.pcr_cr_eq[symmetric] Domainp_set fset.domain_eq)
-lift_definition fcard :: "'a fset \<Rightarrow> nat" is card parametric card_transfer by simp
+lift_definition fcard :: "'a fset \<Rightarrow> nat" is card parametric card_transfer .
lift_definition fimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" (infixr "|`|" 90) is image
parametric image_transfer by simp
-lift_definition fthe_elem :: "'a fset \<Rightarrow> 'a" is the_elem ..
+lift_definition fthe_elem :: "'a fset \<Rightarrow> 'a" is the_elem .
(* FIXME why is not invariant here unfolded ? *)
lift_definition fbind :: "'a fset \<Rightarrow> ('a \<Rightarrow> 'b fset) \<Rightarrow> 'b fset" is Set.bind parametric bind_transfer
@@ -202,10 +202,10 @@
by (subst(asm) compose_rel_to_Domainp [OF _ finite_transfer])
(auto intro: transfer_raw simp add: fset.pcr_cr_eq[symmetric] Domainp_set fset.domain_eq invariant_def)
-lift_definition fBall :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Ball parametric Ball_transfer ..
-lift_definition fBex :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Bex parametric Bex_transfer ..
+lift_definition fBall :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Ball parametric Ball_transfer .
+lift_definition fBex :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Bex parametric Bex_transfer .
-lift_definition ffold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" is Finite_Set.fold ..
+lift_definition ffold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" is Finite_Set.fold .
subsection {* Transferred lemmas from Set.thy *}
@@ -774,7 +774,7 @@
subsubsection {* Relator and predicator properties *}
lift_definition fset_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'b fset \<Rightarrow> bool" is set_rel
-parametric set_rel_transfer ..
+parametric set_rel_transfer .
lemma fset_rel_alt_def: "fset_rel R = (\<lambda>A B. (\<forall>x.\<exists>y. x|\<in>|A \<longrightarrow> y|\<in>|B \<and> R x y)
\<and> (\<forall>y. \<exists>x. y|\<in>|B \<longrightarrow> x|\<in>|A \<and> R x y))"
@@ -837,8 +837,6 @@
by (rename_tac A, rule_tac x="f |`| A" in exI, blast)
qed
-lemmas reflp_fset_rel[reflexivity_rule] = reflp_set_rel[Transfer.transferred]
-
lemma right_total_fset_rel[transfer_rule]: "right_total A \<Longrightarrow> right_total (fset_rel A)"
unfolding right_total_def
apply transfer
--- a/src/HOL/Library/FinFun.thy Tue Feb 18 17:52:28 2014 +0100
+++ b/src/HOL/Library/FinFun.thy Tue Feb 18 23:08:55 2014 +0100
@@ -411,7 +411,7 @@
qed
lift_definition finfun_default :: "'a \<Rightarrow>f 'b \<Rightarrow> 'b"
-is "finfun_default_aux" ..
+is "finfun_default_aux" .
lemma finite_finfun_default: "finite {a. finfun_apply f a \<noteq> finfun_default f}"
by transfer (erule finite_finfun_default_aux)
--- a/src/HOL/Library/Float.thy Tue Feb 18 17:52:28 2014 +0100
+++ b/src/HOL/Library/Float.thy Tue Feb 18 23:08:55 2014 +0100
@@ -161,11 +161,11 @@
lift_definition sgn_float :: "float \<Rightarrow> float" is sgn by simp
declare sgn_float.rep_eq[simp]
-lift_definition equal_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op = :: real \<Rightarrow> real \<Rightarrow> bool" ..
+lift_definition equal_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op = :: real \<Rightarrow> real \<Rightarrow> bool" .
-lift_definition less_eq_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op \<le>" ..
+lift_definition less_eq_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op \<le>" .
declare less_eq_float.rep_eq[simp]
-lift_definition less_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op <" ..
+lift_definition less_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op <" .
declare less_float.rep_eq[simp]
instance
@@ -466,7 +466,7 @@
by transfer (simp add: sgn_times)
hide_fact (open) compute_float_sgn
-lift_definition is_float_pos :: "float \<Rightarrow> bool" is "op < 0 :: real \<Rightarrow> bool" ..
+lift_definition is_float_pos :: "float \<Rightarrow> bool" is "op < 0 :: real \<Rightarrow> bool" .
lemma compute_is_float_pos[code]: "is_float_pos (Float m e) \<longleftrightarrow> 0 < m"
by transfer (auto simp add: zero_less_mult_iff not_le[symmetric, of _ 0])
@@ -476,7 +476,7 @@
by transfer (simp add: field_simps)
hide_fact (open) compute_float_less
-lift_definition is_float_nonneg :: "float \<Rightarrow> bool" is "op \<le> 0 :: real \<Rightarrow> bool" ..
+lift_definition is_float_nonneg :: "float \<Rightarrow> bool" is "op \<le> 0 :: real \<Rightarrow> bool" .
lemma compute_is_float_nonneg[code]: "is_float_nonneg (Float m e) \<longleftrightarrow> 0 \<le> m"
by transfer (auto simp add: zero_le_mult_iff not_less[symmetric, of _ 0])
@@ -486,7 +486,7 @@
by transfer (simp add: field_simps)
hide_fact (open) compute_float_le
-lift_definition is_float_zero :: "float \<Rightarrow> bool" is "op = 0 :: real \<Rightarrow> bool" by simp
+lift_definition is_float_zero :: "float \<Rightarrow> bool" is "op = 0 :: real \<Rightarrow> bool" .
lemma compute_is_float_zero[code]: "is_float_zero (Float m e) \<longleftrightarrow> 0 = m"
by transfer (auto simp add: is_float_zero_def)
@@ -1533,7 +1533,7 @@
lemma real_of_float_nprt[simp]: fixes a::float shows "real (nprt a) = nprt (real a)"
unfolding nprt_def inf_float_def min_def inf_real_def by auto
-lift_definition int_floor_fl :: "float \<Rightarrow> int" is floor by simp
+lift_definition int_floor_fl :: "float \<Rightarrow> int" is floor .
lemma compute_int_floor_fl[code]:
"int_floor_fl (Float m e) = (if 0 \<le> e then m * 2 ^ nat e else m div (2 ^ (nat (-e))))"
--- a/src/HOL/Library/Multiset.thy Tue Feb 18 17:52:28 2014 +0100
+++ b/src/HOL/Library/Multiset.thy Tue Feb 18 23:08:55 2014 +0100
@@ -268,8 +268,8 @@
instantiation multiset :: (type) ordered_ab_semigroup_add_imp_le
begin
-lift_definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" is "\<lambda> A B. (\<forall>a. A a \<le> B a)"
-by simp
+lift_definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" is "\<lambda> A B. (\<forall>a. A a \<le> B a)" .
+
lemmas mset_le_def = less_eq_multiset_def
definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
--- a/src/HOL/Library/Quotient_List.thy Tue Feb 18 17:52:28 2014 +0100
+++ b/src/HOL/Library/Quotient_List.thy Tue Feb 18 23:08:55 2014 +0100
@@ -22,6 +22,16 @@
by (induct xs ys rule: list_induct2') simp_all
qed
+lemma reflp_list_all2:
+ assumes "reflp R"
+ shows "reflp (list_all2 R)"
+proof (rule reflpI)
+ from assms have *: "\<And>xs. R xs xs" by (rule reflpE)
+ fix xs
+ show "list_all2 R xs xs"
+ by (induct xs) (simp_all add: *)
+qed
+
lemma list_symp:
assumes "symp R"
shows "symp (list_all2 R)"
--- a/src/HOL/Library/Quotient_Option.thy Tue Feb 18 17:52:28 2014 +0100
+++ b/src/HOL/Library/Quotient_Option.thy Tue Feb 18 23:08:55 2014 +0100
@@ -22,6 +22,10 @@
map_option.id [id_simps]
rel_option_eq [id_simps]
+lemma reflp_rel_option:
+ "reflp R \<Longrightarrow> reflp (rel_option R)"
+ unfolding reflp_def split_option_all by simp
+
lemma option_symp:
"symp R \<Longrightarrow> symp (rel_option R)"
unfolding symp_def split_option_all
--- a/src/HOL/Library/Quotient_Sum.thy Tue Feb 18 17:52:28 2014 +0100
+++ b/src/HOL/Library/Quotient_Sum.thy Tue Feb 18 23:08:55 2014 +0100
@@ -26,6 +26,10 @@
"sum_rel (op =) (op =) = (op =)"
by (simp add: sum_rel_def fun_eq_iff split: sum.split)
+lemma reflp_sum_rel:
+ "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
+ unfolding reflp_def split_sum_all sum_rel_simps by fast
+
lemma sum_symp:
"symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
unfolding symp_def split_sum_all sum_rel_simps by fast
--- a/src/HOL/Library/RBT.thy Tue Feb 18 17:52:28 2014 +0100
+++ b/src/HOL/Library/RBT.thy Tue Feb 18 23:08:55 2014 +0100
@@ -38,8 +38,7 @@
setup_lifting type_definition_rbt
print_theorems
-lift_definition lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "rbt_lookup"
-by simp
+lift_definition lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "rbt_lookup" .
lift_definition empty :: "('a\<Colon>linorder, 'b) rbt" is RBT_Impl.Empty
by (simp add: empty_def)
@@ -50,29 +49,25 @@
lift_definition delete :: "'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "rbt_delete"
by simp
-lift_definition entries :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" is RBT_Impl.entries
-by simp
+lift_definition entries :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" is RBT_Impl.entries .
+
+lift_definition keys :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list" is RBT_Impl.keys .
-lift_definition keys :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list" is RBT_Impl.keys
-by simp
+lift_definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" is "rbt_bulkload" ..
-lift_definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" is "rbt_bulkload"
-by simp
-
-lift_definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is rbt_map_entry
+lift_definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is rbt_map_entry
by simp
lift_definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'c) rbt" is RBT_Impl.map
by simp
-lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" is RBT_Impl.fold
-by simp
+lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" is RBT_Impl.fold .
lift_definition union :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "rbt_union"
by (simp add: rbt_union_is_rbt)
lift_definition foldi :: "('c \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a :: linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"
- is RBT_Impl.foldi by simp
+ is RBT_Impl.foldi .
subsection {* Derived operations *}
--- a/src/HOL/Library/RBT_Set.thy Tue Feb 18 17:52:28 2014 +0100
+++ b/src/HOL/Library/RBT_Set.thy Tue Feb 18 23:08:55 2014 +0100
@@ -423,7 +423,7 @@
(** abstract **)
lift_definition fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> 'a"
- is rbt_fold1_keys by simp
+ is rbt_fold1_keys .
lemma fold1_keys_def_alt:
"fold1_keys f t = List.fold f (tl(keys t)) (hd(keys t))"
@@ -441,9 +441,9 @@
(* minimum *)
-lift_definition r_min :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min by simp
+lift_definition r_min :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min .
-lift_definition r_min_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min_opt by simp
+lift_definition r_min_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min_opt .
lemma r_min_alt_def: "r_min t = fold1_keys min t"
by transfer (simp add: rbt_min_def)
@@ -479,9 +479,9 @@
(* maximum *)
-lift_definition r_max :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max by simp
+lift_definition r_max :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max .
-lift_definition r_max_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max_opt by simp
+lift_definition r_max_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max_opt .
lemma r_max_alt_def: "r_max t = fold1_keys max t"
by transfer (simp add: rbt_max_def)
--- a/src/HOL/Lifting.thy Tue Feb 18 17:52:28 2014 +0100
+++ b/src/HOL/Lifting.thy Tue Feb 18 23:08:55 2014 +0100
@@ -439,39 +439,23 @@
text {* Proving reflexivity *}
-definition reflp' :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where "reflp' R \<equiv> reflp R"
-
lemma Quotient_to_left_total:
assumes q: "Quotient R Abs Rep T"
and r_R: "reflp R"
shows "left_total T"
using r_R Quotient_cr_rel[OF q] unfolding left_total_def by (auto elim: reflpE)
-lemma reflp_Quotient_composition:
- assumes "left_total R"
- assumes "reflp T"
- shows "reflp (R OO T OO R\<inverse>\<inverse>)"
-using assms unfolding reflp_def left_total_def by fast
-
-lemma reflp_fun1:
- assumes "is_equality R"
- assumes "reflp' S"
- shows "reflp (R ===> S)"
-using assms unfolding is_equality_def reflp'_def reflp_def fun_rel_def by blast
+lemma Quotient_composition_ge_eq:
+ assumes "left_total T"
+ assumes "R \<ge> op="
+ shows "(T OO R OO T\<inverse>\<inverse>) \<ge> op="
+using assms unfolding left_total_def by fast
-lemma reflp_fun2:
- assumes "is_equality R"
- assumes "is_equality S"
- shows "reflp (R ===> S)"
-using assms unfolding is_equality_def reflp_def fun_rel_def by blast
-
-lemma is_equality_Quotient_composition:
- assumes "is_equality T"
- assumes "left_total R"
- assumes "left_unique R"
- shows "is_equality (R OO T OO R\<inverse>\<inverse>)"
-using assms unfolding is_equality_def left_total_def left_unique_def OO_def conversep_iff
-by fastforce
+lemma Quotient_composition_le_eq:
+ assumes "left_unique T"
+ assumes "R \<le> op="
+ shows "(T OO R OO T\<inverse>\<inverse>) \<le> op="
+using assms unfolding left_unique_def by fast
lemma left_total_composition: "left_total R \<Longrightarrow> left_total S \<Longrightarrow> left_total (R OO S)"
unfolding left_total_def OO_def by fast
@@ -479,8 +463,14 @@
lemma left_unique_composition: "left_unique R \<Longrightarrow> left_unique S \<Longrightarrow> left_unique (R OO S)"
unfolding left_unique_def OO_def by fast
-lemma reflp_equality: "reflp (op =)"
-by (auto intro: reflpI)
+lemma invariant_le_eq:
+ "invariant P \<le> op=" unfolding invariant_def by blast
+
+lemma reflp_ge_eq:
+ "reflp R \<Longrightarrow> R \<ge> op=" unfolding reflp_def by blast
+
+lemma ge_eq_refl:
+ "R \<ge> op= \<Longrightarrow> R x x" by blast
text {* Proving a parametrized correspondence relation *}
@@ -649,19 +639,10 @@
setup Lifting_Info.setup
lemmas [reflexivity_rule] =
- reflp_equality reflp_Quotient_composition is_equality_Quotient_composition
- left_total_fun left_unique_fun left_total_eq left_unique_eq left_total_composition
- left_unique_composition
-
-text {* add @{thm reflp_fun1} and @{thm reflp_fun2} manually through ML
- because we don't want to get reflp' variant of these theorems *}
-
-setup{*
-Context.theory_map
- (fold
- (snd oo (Thm.apply_attribute Lifting_Info.add_reflexivity_rule_raw_attribute))
- [@{thm reflp_fun1}, @{thm reflp_fun2}])
-*}
+ order_refl[of "op="] invariant_le_eq Quotient_composition_le_eq
+ Quotient_composition_ge_eq
+ left_total_eq left_unique_eq left_total_composition left_unique_composition
+ left_total_fun left_unique_fun
(* setup for the function type *)
declare fun_quotient[quot_map]
@@ -674,6 +655,6 @@
ML_file "Tools/Lifting/lifting_setup.ML"
-hide_const (open) invariant POS NEG reflp'
+hide_const (open) invariant POS NEG
end
--- a/src/HOL/Lifting_Option.thy Tue Feb 18 17:52:28 2014 +0100
+++ b/src/HOL/Lifting_Option.thy Tue Feb 18 23:08:55 2014 +0100
@@ -39,10 +39,6 @@
using assms unfolding Domainp_iff[abs_def] rel_option_iff[abs_def]
by (auto iff: fun_eq_iff split: option.split)
-lemma reflp_rel_option[reflexivity_rule]:
- "reflp R \<Longrightarrow> reflp (rel_option R)"
- unfolding reflp_def split_option_all by simp
-
lemma left_total_rel_option[reflexivity_rule]:
"left_total R \<Longrightarrow> left_total (rel_option R)"
unfolding left_total_def split_option_all split_option_ex by simp
--- a/src/HOL/Lifting_Product.thy Tue Feb 18 17:52:28 2014 +0100
+++ b/src/HOL/Lifting_Product.thy Tue Feb 18 23:08:55 2014 +0100
@@ -30,12 +30,6 @@
shows "Domainp (prod_rel T1 T2) = (prod_pred P1 P2)"
using assms unfolding prod_rel_def prod_pred_def by blast
-lemma reflp_prod_rel [reflexivity_rule]:
- assumes "reflp R1"
- assumes "reflp R2"
- shows "reflp (prod_rel R1 R2)"
-using assms by (auto intro!: reflpI elim: reflpE)
-
lemma left_total_prod_rel [reflexivity_rule]:
assumes "left_total R1"
assumes "left_total R2"
--- a/src/HOL/Lifting_Set.thy Tue Feb 18 17:52:28 2014 +0100
+++ b/src/HOL/Lifting_Set.thy Tue Feb 18 23:08:55 2014 +0100
@@ -54,9 +54,6 @@
apply (rename_tac A, rule_tac x="{y. \<exists>x\<in>A. T x y}" in exI, fast)
done
-lemma reflp_set_rel[reflexivity_rule]: "reflp R \<Longrightarrow> reflp (set_rel R)"
- unfolding reflp_def set_rel_def by fast
-
lemma left_total_set_rel[reflexivity_rule]:
"left_total A \<Longrightarrow> left_total (set_rel A)"
unfolding left_total_def set_rel_def
--- a/src/HOL/Lifting_Sum.thy Tue Feb 18 17:52:28 2014 +0100
+++ b/src/HOL/Lifting_Sum.thy Tue Feb 18 23:08:55 2014 +0100
@@ -26,10 +26,6 @@
using assms
by (auto simp add: Domainp_iff split_sum_ex iff: fun_eq_iff split: sum.split)
-lemma reflp_sum_rel[reflexivity_rule]:
- "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
- unfolding reflp_def split_sum_all sum_rel_simps by fast
-
lemma left_total_sum_rel[reflexivity_rule]:
"left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (sum_rel R1 R2)"
using assms unfolding left_total_def split_sum_all split_sum_ex by simp
--- a/src/HOL/List.thy Tue Feb 18 17:52:28 2014 +0100
+++ b/src/HOL/List.thy Tue Feb 18 23:08:55 2014 +0100
@@ -6582,16 +6582,6 @@
by (auto iff: fun_eq_iff)
qed
-lemma reflp_list_all2[reflexivity_rule]:
- assumes "reflp R"
- shows "reflp (list_all2 R)"
-proof (rule reflpI)
- from assms have *: "\<And>xs. R xs xs" by (rule reflpE)
- fix xs
- show "list_all2 R xs xs"
- by (induct xs) (simp_all add: *)
-qed
-
lemma left_total_list_all2[reflexivity_rule]:
"left_total R \<Longrightarrow> left_total (list_all2 R)"
unfolding left_total_def
--- a/src/HOL/Predicate_Compile.thy Tue Feb 18 17:52:28 2014 +0100
+++ b/src/HOL/Predicate_Compile.thy Tue Feb 18 23:08:55 2014 +0100
@@ -81,6 +81,7 @@
Core_Data.PredData.map (Graph.new_node
(@{const_name contains},
Core_Data.PredData {
+ pos = Position.thread_data (),
intros = [(NONE, @{thm containsI})],
elim = SOME @{thm containsE},
preprocessed = true,
--- a/src/HOL/Quotient_Examples/Lift_DList.thy Tue Feb 18 17:52:28 2014 +0100
+++ b/src/HOL/Quotient_Examples/Lift_DList.thy Tue Feb 18 23:08:55 2014 +0100
@@ -35,20 +35,15 @@
text {* Derived operations: *}
-lift_definition null :: "'a dlist \<Rightarrow> bool" is List.null
-by simp
+lift_definition null :: "'a dlist \<Rightarrow> bool" is List.null .
-lift_definition member :: "'a dlist \<Rightarrow> 'a \<Rightarrow> bool" is List.member
-by simp
+lift_definition member :: "'a dlist \<Rightarrow> 'a \<Rightarrow> bool" is List.member .
-lift_definition length :: "'a dlist \<Rightarrow> nat" is List.length
-by simp
+lift_definition length :: "'a dlist \<Rightarrow> nat" is List.length .
-lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" is List.fold
-by simp
+lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" is List.fold .
-lift_definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" is List.foldr
-by simp
+lift_definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" is List.foldr .
lift_definition concat :: "'a dlist dlist \<Rightarrow> 'a dlist" is "remdups o List.concat"
proof -
--- a/src/HOL/Tools/Lifting/lifting_def.ML Tue Feb 18 17:52:28 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Tue Feb 18 23:08:55 2014 +0100
@@ -31,7 +31,7 @@
let
fun intro_reflp_tac (ct, i) =
let
- val rule = Thm.incr_indexes (#maxidx (rep_cterm ct) + 1) @{thm reflpD}
+ val rule = Thm.incr_indexes (#maxidx (rep_cterm ct) + 1) @{thm ge_eq_refl}
val concl_pat = Drule.strip_imp_concl (cprop_of rule)
val insts = Thm.first_order_match (concl_pat, ct)
in
--- a/src/HOL/Tools/Lifting/lifting_info.ML Tue Feb 18 17:52:28 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Tue Feb 18 23:08:55 2014 +0100
@@ -28,7 +28,6 @@
val get_invariant_commute_rules: Proof.context -> thm list
val get_reflexivity_rules: Proof.context -> thm list
- val add_reflexivity_rule_raw_attribute: attribute
val add_reflexivity_rule_attribute: attribute
type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm,
@@ -276,33 +275,14 @@
(* info about reflexivity rules *)
fun get_reflexivity_rules ctxt = Item_Net.content (get_reflexivity_rules' (Context.Proof ctxt))
-
-(* Conversion to create a reflp' variant of a reflexivity rule *)
-fun safe_reflp_conv ct =
- Conv.try_conv (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm reflp'_def}))) ct
-
-fun prep_reflp_conv ct = (
- Conv.implies_conv safe_reflp_conv prep_reflp_conv
- else_conv
- safe_reflp_conv
- else_conv
- Conv.all_conv) ct
-
-fun add_reflexivity_rule_raw thm = Data.map (map_reflexivity_rules (Item_Net.update thm))
-val add_reflexivity_rule_raw_attribute = Thm.declaration_attribute add_reflexivity_rule_raw
-
-fun add_reflexivity_rule thm = add_reflexivity_rule_raw thm #>
- add_reflexivity_rule_raw (Conv.fconv_rule prep_reflp_conv thm)
+fun add_reflexivity_rule thm = Data.map (map_reflexivity_rules (Item_Net.update thm))
val add_reflexivity_rule_attribute = Thm.declaration_attribute add_reflexivity_rule
-
val relfexivity_rule_setup =
let
val name = @{binding reflexivity_rule}
- fun del_thm_raw thm = Data.map (map_reflexivity_rules (Item_Net.remove thm))
- fun del_thm thm = del_thm_raw thm #>
- del_thm_raw (Conv.fconv_rule prep_reflp_conv thm)
+ fun del_thm thm = Data.map (map_reflexivity_rules (Item_Net.remove thm))
val del = Thm.declaration_attribute del_thm
val text = "rules that are used to prove that a relation is reflexive"
val content = Item_Net.content o get_reflexivity_rules'
@@ -370,19 +350,42 @@
Conv.fconv_rule (Conv.prems_conv ~1 rewr_conv then_conv Conv.concl_conv ~1 rewr_conv) mono_rule
end;
+fun add_reflexivity_rules mono_rule ctxt =
+ let
+ fun find_eq_rule thm ctxt =
+ let
+ val concl_rhs = (hd o get_args 1 o HOLogic.dest_Trueprop o concl_of) thm;
+ val rules = Item_Net.retrieve (Transfer.get_relator_eq_item_net ctxt) concl_rhs;
+ in
+ find_first (fn thm => Pattern.matches (Proof_Context.theory_of ctxt) (concl_rhs,
+ (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.concl_of) thm)) rules
+ end
+
+ val eq_rule = find_eq_rule mono_rule (Context.proof_of ctxt);
+ val eq_rule = if is_some eq_rule then the eq_rule else error
+ "No corresponding rule that the relator preserves equality was found."
+ in
+ ctxt
+ |> add_reflexivity_rule (Drule.zero_var_indexes (@{thm ord_le_eq_trans} OF [mono_rule, eq_rule]))
+ |> add_reflexivity_rule
+ (Drule.zero_var_indexes (@{thm ord_eq_le_trans} OF [sym OF [eq_rule], mono_rule]))
+ end
+
fun add_mono_rule mono_rule ctxt =
let
- val mono_rule = introduce_polarities mono_rule
+ val pol_mono_rule = introduce_polarities mono_rule
val mono_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o
- dest_Const o head_of o HOLogic.dest_Trueprop o concl_of) mono_rule
+ dest_Const o head_of o HOLogic.dest_Trueprop o concl_of) pol_mono_rule
val _ = if Symtab.defined (get_relator_distr_data' ctxt) mono_ruleT_name
then error ("Monotocity rule for type " ^ quote mono_ruleT_name ^ " is already_defined.")
else ()
- val neg_mono_rule = negate_mono_rule mono_rule
- val relator_distr_data = {pos_mono_rule = mono_rule, neg_mono_rule = neg_mono_rule,
+ val neg_mono_rule = negate_mono_rule pol_mono_rule
+ val relator_distr_data = {pos_mono_rule = pol_mono_rule, neg_mono_rule = neg_mono_rule,
pos_distr_rules = [], neg_distr_rules = []}
in
- Data.map (map_relator_distr_data (Symtab.update (mono_ruleT_name, relator_distr_data))) ctxt
+ ctxt
+ |> Data.map (map_relator_distr_data (Symtab.update (mono_ruleT_name, relator_distr_data)))
+ |> add_reflexivity_rules mono_rule
end;
local
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Tue Feb 18 17:52:28 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Tue Feb 18 23:08:55 2014 +0100
@@ -252,7 +252,7 @@
val lthy = case opt_reflp_thm of
SOME reflp_thm => lthy
|> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]),
- [reflp_thm])
+ [reflp_thm RS @{thm reflp_ge_eq}])
|> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]),
[[quot_thm, reflp_thm] MRSL @{thm Quotient_to_left_total}])
|> define_code_constr gen_code quot_thm
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML Tue Feb 18 17:52:28 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Tue Feb 18 23:08:55 2014 +0100
@@ -18,6 +18,7 @@
};
datatype pred_data = PredData of {
+ pos : Position.T,
intros : (string option * thm) list,
elim : thm option,
preprocessed : bool,
@@ -100,6 +101,7 @@
PredfunData {definition = definition, intro = intro, elim = elim, neg_intro = neg_intro}
datatype pred_data = PredData of {
+ pos: Position.T,
intros : (string option * thm) list,
elim : thm option,
preprocessed : bool,
@@ -109,13 +111,17 @@
};
fun rep_pred_data (PredData data) = data;
+val pos_of = #pos o rep_pred_data;
-fun mk_pred_data (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random))) =
- PredData {intros = intros, elim = elim, preprocessed = preprocessed,
+fun mk_pred_data
+ (pos, (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random)))) =
+ PredData {pos = pos, intros = intros, elim = elim, preprocessed = preprocessed,
function_names = function_names, predfun_data = predfun_data, needs_random = needs_random}
-fun map_pred_data f (PredData {intros, elim, preprocessed, function_names, predfun_data, needs_random}) =
- mk_pred_data (f (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random))))
+fun map_pred_data f
+ (PredData {pos, intros, elim, preprocessed, function_names, predfun_data, needs_random}) =
+ mk_pred_data
+ (f (pos, (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random)))))
fun eq_option eq (NONE, NONE) = true
| eq_option eq (SOME x, SOME y) = eq (x, y)
@@ -130,7 +136,13 @@
type T = pred_data Graph.T;
val empty = Graph.empty;
val extend = I;
- val merge = Graph.merge eq_pred_data;
+ val merge =
+ Graph.join (fn key => fn (x, y) =>
+ if eq_pred_data (x, y)
+ then raise Graph.SAME
+ else
+ error ("Duplicate predicate declarations for " ^ quote key ^
+ Position.here (pos_of x) ^ Position.here (pos_of y)));
);
@@ -260,11 +272,13 @@
(case try (Inductive.the_inductive ctxt) name of
SOME (info as (_, result)) =>
let
+ val thy = Proof_Context.theory_of ctxt
+
+ val pos = Position.thread_data ()
fun is_intro_of intro =
let
val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro))
in (fst (dest_Const const) = name) end;
- val thy = Proof_Context.theory_of ctxt
val intros = map (preprocess_intro thy) (filter is_intro_of (#intrs result))
val index = find_index (fn s => s = name) (#names (fst info))
val pre_elim = nth (#elims result) index
@@ -273,13 +287,13 @@
val nparams = length (Inductive.params_of (#raw_induct result))
val elim = prove_casesrule ctxt (pred, (pre_elim, nparams)) elim_t
in
- mk_pred_data (((map (pair NONE) intros, SOME elim), true), no_compilation)
+ mk_pred_data (pos, (((map (pair NONE) intros, SOME elim), true), no_compilation))
end
| NONE => error ("No such predicate: " ^ quote name))
fun add_predfun_data name mode data =
let
- val add = (apsnd o apsnd o apfst) (cons (mode, mk_predfun_data data))
+ val add = (apsnd o apsnd o apsnd o apfst) (cons (mode, mk_predfun_data data))
in PredData.map (Graph.map_node name (map_pred_data add)) end
fun is_inductive_predicate ctxt name =
@@ -305,17 +319,21 @@
(case try (Graph.get_node gr) name of
SOME _ =>
Graph.map_node name (map_pred_data
- (apfst (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)]))))) gr
+ (apsnd (apfst (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)])))))) gr
| NONE =>
Graph.new_node
- (name, mk_pred_data ((([(opt_case_name, thm)], NONE), false), no_compilation)) gr)
+ (name,
+ mk_pred_data (Position.thread_data (),
+ (((([(opt_case_name, thm)], NONE), false), no_compilation)))) gr)
in PredData.map cons_intro thy end
fun set_elim thm =
let
val (name, _) =
dest_Const (fst (strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm)))))
- in PredData.map (Graph.map_node name (map_pred_data (apfst (apfst (apsnd (K (SOME thm))))))) end
+ in
+ PredData.map (Graph.map_node name (map_pred_data (apsnd (apfst (apfst (apsnd (K (SOME thm))))))))
+ end
fun register_predicate (constname, intros, elim) thy =
let
@@ -324,7 +342,8 @@
if not (member (op =) (Graph.keys (PredData.get thy)) constname) then
PredData.map
(Graph.new_node (constname,
- mk_pred_data (((named_intros, SOME elim), false), no_compilation))) thy
+ mk_pred_data (Position.thread_data (),
+ (((named_intros, SOME elim), false), no_compilation)))) thy
else thy
end
@@ -345,14 +364,14 @@
fun defined_function_of compilation pred =
let
- val set = (apsnd o apfst) (cons (compilation, []))
+ val set = (apsnd o apsnd o apfst) (cons (compilation, []))
in
PredData.map (Graph.map_node pred (map_pred_data set))
end
fun set_function_name compilation pred mode name =
let
- val set = (apsnd o apfst)
+ val set = (apsnd o apsnd o apfst)
(AList.map_default (op =) (compilation, [(mode, name)]) (cons (mode, name)))
in
PredData.map (Graph.map_node pred (map_pred_data set))
@@ -360,7 +379,7 @@
fun set_needs_random name modes =
let
- val set = (apsnd o apsnd o apsnd) (K modes)
+ val set = (apsnd o apsnd o apsnd o apsnd) (K modes)
in
PredData.map (Graph.map_node name (map_pred_data set))
end
@@ -389,7 +408,7 @@
end
fun preprocess_intros name thy =
- PredData.map (Graph.map_node name (map_pred_data (apfst (fn (rules, preprocessed) =>
+ PredData.map (Graph.map_node name (map_pred_data (apsnd (apfst (fn (rules, preprocessed) =>
if preprocessed then (rules, preprocessed)
else
let
@@ -401,7 +420,7 @@
val elim' = prove_casesrule ctxt (pred, (elim, 0)) elim_t
in
((named_intros', SOME elim'), true)
- end))))
+ end)))))
thy
@@ -422,7 +441,7 @@
AList.lookup eq_mode
(Symtab.lookup_list (Alt_Compilations_Data.get (Proof_Context.theory_of ctxt)) pred_name) mode
-fun force_modes_and_compilations pred_name compilations =
+fun force_modes_and_compilations pred_name compilations thy =
let
(* thm refl is a dummy thm *)
val modes = map fst compilations
@@ -435,11 +454,14 @@
map (rpair non_random_dummys) Predicate_Compile_Aux.non_random_compilations
val alt_compilations = map (apsnd fst) compilations
in
+ thy |>
PredData.map
(Graph.new_node
(pred_name,
- mk_pred_data ((([], SOME @{thm refl}), true), (dummy_function_names, ([], needs_random)))))
- #> Alt_Compilations_Data.map (Symtab.insert (K false) (pred_name, alt_compilations))
+ mk_pred_data
+ (Position.thread_data (),
+ ((([], SOME @{thm refl}), true), (dummy_function_names, ([], needs_random))))))
+ |> Alt_Compilations_Data.map (Symtab.insert (K false) (pred_name, alt_compilations))
end
fun functional_compilation fun_name mode compfuns T =
--- a/src/HOL/Tools/transfer.ML Tue Feb 18 17:52:28 2014 +0100
+++ b/src/HOL/Tools/transfer.ML Tue Feb 18 23:08:55 2014 +0100
@@ -12,6 +12,7 @@
val prep_conv: conv
val get_transfer_raw: Proof.context -> thm list
+ val get_relator_eq_item_net: Proof.context -> thm Item_Net.T
val get_relator_eq: Proof.context -> thm list
val get_sym_relator_eq: Proof.context -> thm list
val get_relator_eq_raw: Proof.context -> thm list
@@ -40,6 +41,8 @@
(** Theory Data **)
val compound_xhs_empty_net = Item_Net.init (Thm.eq_thm_prop o pairself snd) (single o fst);
+val rewr_rules = Item_Net.init Thm.eq_thm_prop (single o fst o HOLogic.dest_eq
+ o HOLogic.dest_Trueprop o Thm.concl_of);
structure Data = Generic_Data
(
@@ -56,7 +59,7 @@
known_frees = [],
compound_lhs = compound_xhs_empty_net,
compound_rhs = compound_xhs_empty_net,
- relator_eq = Thm.full_rules,
+ relator_eq = rewr_rules,
relator_eq_raw = Thm.full_rules,
relator_domain = Thm.full_rules }
val extend = I
@@ -90,6 +93,8 @@
fun get_compound_rhs ctxt = ctxt
|> (#compound_rhs o Data.get o Context.Proof)
+fun get_relator_eq_item_net ctxt = (#relator_eq o Data.get o Context.Proof) ctxt
+
fun get_relator_eq ctxt = ctxt
|> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
|> map safe_mk_meta_eq
--- a/src/HOL/Topological_Spaces.thy Tue Feb 18 17:52:28 2014 +0100
+++ b/src/HOL/Topological_Spaces.thy Tue Feb 18 23:08:55 2014 +0100
@@ -2375,10 +2375,6 @@
unfolding filter_rel_eventually[abs_def]
by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl)
-lemma reflp_filter_rel [reflexivity_rule]: "reflp R \<Longrightarrow> reflp (filter_rel R)"
-unfolding filter_rel_eventually[abs_def]
-by(blast intro!: reflpI eventually_subst always_eventually dest: fun_relD reflpD)
-
lemma filter_rel_conversep [simp]: "filter_rel A\<inverse>\<inverse> = (filter_rel A)\<inverse>\<inverse>"
by(auto simp add: filter_rel_eventually fun_eq_iff fun_rel_def)
--- a/src/Pure/General/path.scala Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Pure/General/path.scala Tue Feb 18 23:08:55 2014 +0100
@@ -94,7 +94,7 @@
else (List(root_elem(es.head)), es.tail)
val elems = raw_elems.filterNot(s => s.isEmpty || s == ".").map(explode_elem)
- new Path(norm_elems(elems.reverse ++ roots))
+ new Path(norm_elems(elems.reverse ::: roots))
}
def is_ok(str: String): Boolean =
--- a/src/Pure/General/position.ML Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Pure/General/position.ML Tue Feb 18 23:08:55 2014 +0100
@@ -192,7 +192,7 @@
(SOME i, NONE) => "(line " ^ Markup.print_int i ^ ")"
| (SOME i, SOME name) => "(line " ^ Markup.print_int i ^ " of " ^ quote name ^ ")"
| (NONE, SOME name) => "(file " ^ quote name ^ ")"
- | _ => "");
+ | _ => if is_reported pos then "\\<here>" else "");
in
if null props then ""
else (if s = "" then "" else " ") ^ Markup.markup (Markup.properties props Markup.position) s
--- a/src/Pure/General/position.scala Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Pure/General/position.scala Tue Feb 18 23:08:55 2014 +0100
@@ -50,7 +50,7 @@
object Range
{
- def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop)
+ def apply(range: Text.Range): T = Offset(range.start) ::: Offset(range.stop)
def unapply(pos: T): Option[Text.Range] =
(pos, pos) match {
case (Offset(start), End_Offset(stop)) if start <= stop => Some(Text.Range(start, stop))
--- a/src/Pure/General/pretty.scala Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Pure/General/pretty.scala Tue Feb 18 23:08:55 2014 +0100
@@ -45,12 +45,11 @@
object Block
{
def apply(i: Int, body: XML.Body): XML.Tree =
- XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body)
+ XML.Elem(Markup.Block(i), body)
def unapply(tree: XML.Tree): Option[(Int, XML.Body)] =
tree match {
- case XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body) =>
- Some((i, body))
+ case XML.Elem(Markup.Block(i), body) => Some((i, body))
case _ => None
}
}
@@ -58,12 +57,11 @@
object Break
{
def apply(w: Int): XML.Tree =
- XML.Elem(Markup(Markup.BREAK, Markup.Width(w)),
- List(XML.Text(spaces(w))))
+ XML.Elem(Markup.Break(w), List(XML.Text(spaces(w))))
def unapply(tree: XML.Tree): Option[Int] =
tree match {
- case XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), _) => Some(w)
+ case XML.Elem(Markup.Break(w), _) => Some(w)
case _ => None
}
}
--- a/src/Pure/ML/ml_lex.ML Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML Tue Feb 18 23:08:55 2014 +0100
@@ -300,7 +300,7 @@
fun read pos txt =
let
- val _ = Position.report pos Markup.ML_source;
+ val _ = Position.report pos Markup.language_ML;
val syms = Symbol_Pos.explode (txt, pos);
val termination =
if null syms then []
--- a/src/Pure/PIDE/command.scala Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Pure/PIDE/command.scala Tue Feb 18 23:08:55 2014 +0100
@@ -108,19 +108,17 @@
if id == command.id || id == alt_id =>
command.chunks.get(file_name) match {
case Some(chunk) =>
- val range = chunk.decode(raw_range)
- if (chunk.range.contains(range)) {
- val props = Position.purge(atts)
- val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
- state.add_markup(file_name, info)
+ chunk.decode(raw_range).try_restrict(chunk.range) match {
+ case Some(range) =>
+ if (!range.is_singularity) {
+ val props = Position.purge(atts)
+ state.add_markup(file_name,
+ Text.Info(range, XML.Elem(Markup(name, props), args)))
+ }
+ else state
+ case None => bad(); state
}
- else {
- bad()
- state
- }
- case None =>
- bad()
- state
+ case None => bad(); state
}
case XML.Elem(Markup(name, atts), args)
@@ -130,9 +128,7 @@
val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
state.add_markup("", info)
- case _ =>
- // FIXME bad()
- state
+ case _ => /* FIXME bad(); */ state
}
})
case XML.Elem(Markup(name, props), body) =>
--- a/src/Pure/PIDE/markup.ML Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Pure/PIDE/markup.ML Tue Feb 18 23:08:55 2014 +0100
@@ -20,6 +20,14 @@
val name: string -> T -> T
val kindN: string
val instanceN: string
+ val languageN: string val language: string -> T
+ val language_sort: T
+ val language_type: T
+ val language_term: T
+ val language_prop: T
+ val language_ML: T
+ val language_document: T
+ val language_text: T
val bindingN: string val binding: T
val entityN: string val entity: string -> string -> T
val get_entity_kind: T -> string option
@@ -62,10 +70,6 @@
val inner_cartoucheN: string val inner_cartouche: T
val inner_commentN: string val inner_comment: T
val token_rangeN: string val token_range: T
- val sortN: string val sort: T
- val typN: string val typ: T
- val termN: string val term: T
- val propN: string val prop: T
val sortingN: string val sorting: T
val typingN: string val typing: T
val ML_keyword1N: string val ML_keyword1: T
@@ -81,8 +85,6 @@
val ML_openN: string
val ML_structN: string
val ML_typingN: string val ML_typing: T
- val ML_sourceN: string val ML_source: T
- val document_sourceN: string val document_source: T
val antiquotedN: string val antiquoted: T
val antiquoteN: string val antiquote: T
val ML_antiquotationN: string
@@ -163,6 +165,12 @@
val command_timing: Properties.entry
val loading_theory: string -> Properties.T
val dest_loading_theory: Properties.T -> string option
+ val simp_trace_logN: string
+ val simp_trace_stepN: string
+ val simp_trace_recurseN: string
+ val simp_trace_hintN: string
+ val simp_trace_ignoreN: string
+ val simp_trace_cancel: serial -> Properties.T
val no_output: Output.output * Output.output
val default_output: T -> Output.output * Output.output
val add_mode: string -> (T -> Output.output * Output.output) -> unit
@@ -220,9 +228,9 @@
fun properties more_props ((elem, props): T) =
(elem, fold_rev Properties.put more_props props);
-fun markup_elem elem = (elem, (elem, []): T);
-fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T);
-fun markup_int elem prop = (elem, fn i => (elem, [(prop, print_int i)]): T);
+fun markup_elem name = (name, (name, []): T);
+fun markup_string name prop = (name, fn s => (name, [(prop, s)]): T);
+fun markup_int name prop = (name, fn i => (name, [(prop, print_int i)]): T);
(* misc properties *)
@@ -235,6 +243,20 @@
val instanceN = "instance";
+(* embedded languages *)
+
+val (languageN, language) = markup_string "language" nameN;
+
+val language_sort = language "sort";
+val language_type = language "type";
+val language_term = language "term";
+val language_prop = language "prop";
+
+val language_ML = language "ML";
+val language_document = language "document";
+val language_text = language "text";
+
+
(* formal entities *)
val (bindingN, binding) = markup_elem "binding";
@@ -317,11 +339,6 @@
val (token_rangeN, token_range) = markup_elem "token_range";
-val (sortN, sort) = markup_elem "sort";
-val (typN, typ) = markup_elem "typ";
-val (termN, term) = markup_elem "term";
-val (propN, prop) = markup_elem "prop";
-
val (sortingN, sorting) = markup_elem "sorting";
val (typingN, typing) = markup_elem "typing";
@@ -344,10 +361,7 @@
val (ML_typingN, ML_typing) = markup_elem "ML_typing";
-(* embedded source text *)
-
-val (ML_sourceN, ML_source) = markup_elem "ML_source";
-val (document_sourceN, document_source) = markup_elem "document_source";
+(* antiquotations *)
val (antiquotedN, antiquoted) = markup_elem "antiquoted";
val (antiquoteN, antiquote) = markup_elem "antiquote";
@@ -510,6 +524,16 @@
| dest_loading_theory _ = NONE;
+(* simplifier trace *)
+
+val simp_trace_logN = "simp_trace_log";
+val simp_trace_stepN = "simp_trace_step";
+val simp_trace_recurseN = "simp_trace_recurse";
+val simp_trace_hintN = "simp_trace_hint";
+val simp_trace_ignoreN = "simp_trace_ignore";
+
+fun simp_trace_cancel i = [(functionN, "simp_trace_cancel"), (serialN, print_int i)];
+
(** print mode operations **)
--- a/src/Pure/PIDE/markup.scala Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Pure/PIDE/markup.scala Tue Feb 18 23:08:55 2014 +0100
@@ -27,6 +27,24 @@
val Empty = Markup("", Nil)
val Broken = Markup("broken", Nil)
+ class Markup_String(val name: String, prop: String)
+ {
+ private val Prop = new Properties.String(prop)
+
+ def apply(s: String): Markup = Markup(name, Prop(s))
+ def unapply(markup: Markup): Option[String] =
+ if (markup.name == name) Prop.unapply(markup.properties) else None
+ }
+
+ class Markup_Int(val name: String, prop: String)
+ {
+ private val Prop = new Properties.Int(prop)
+
+ def apply(i: Int): Markup = Markup(name, Prop(i))
+ def unapply(markup: Markup): Option[Int] =
+ if (markup.name == name) Prop.unapply(markup.properties) else None
+ }
+
/* formal entities */
@@ -39,9 +57,9 @@
{
def unapply(markup: Markup): Option[(String, String)] =
markup match {
- case Markup(ENTITY, props @ Kind(kind)) =>
- props match {
- case Name(name) => Some(kind, name)
+ case Markup(ENTITY, props) =>
+ (props, props) match {
+ case (Kind(kind), Name(name)) => Some(kind, name)
case _ => None
}
case _ => None
@@ -67,38 +85,25 @@
val POSITION = "position"
+ /* embedded languages */
+
+ val LANGUAGE = "language"
+ val Language = new Markup_String(LANGUAGE, NAME)
+
+
/* external resources */
val PATH = "path"
-
- object Path
- {
- def unapply(markup: Markup): Option[String] =
- markup match {
- case Markup(PATH, Name(name)) => Some(name)
- case _ => None
- }
- }
+ val Path = new Markup_String(PATH, NAME)
val URL = "url"
-
- object Url
- {
- def unapply(markup: Markup): Option[String] =
- markup match {
- case Markup(URL, Name(name)) => Some(name)
- case _ => None
- }
- }
+ val Url = new Markup_String(URL, NAME)
/* pretty printing */
- val Indent = new Properties.Int("indent")
- val BLOCK = "block"
-
- val Width = new Properties.Int("width")
- val BREAK = "break"
+ val Block = new Markup_Int("block", "indent")
+ val Break = new Markup_Int("break", "width")
val ITEM = "item"
val BULLET = "bullet"
@@ -138,11 +143,6 @@
val TOKEN_RANGE = "token_range"
- val SORT = "sort"
- val TYP = "typ"
- val TERM = "term"
- val PROP = "prop"
-
val SORTING = "sorting"
val TYPING = "typing"
@@ -150,10 +150,7 @@
val METHOD = "method"
- /* embedded source text */
-
- val ML_SOURCE = "ML_source"
- val DOCUMENT_SOURCE = "document_source"
+ /* antiquotations */
val ANTIQUOTED = "antiquoted"
val ANTIQUOTE = "antiquote"
@@ -392,82 +389,26 @@
}
}
+
/* simplifier trace */
- val TEXT = "text"
- val Text = new Properties.String(TEXT)
-
- val PARENT = "parent"
- val Parent = new Properties.Long(PARENT)
+ val SIMP_TRACE = "simp_trace"
- val SUCCESS = "success"
- val Success = new Properties.Boolean(SUCCESS)
+ val SIMP_TRACE_LOG = "simp_trace_log"
+ val SIMP_TRACE_STEP = "simp_trace_step"
+ val SIMP_TRACE_RECURSE = "simp_trace_recurse"
+ val SIMP_TRACE_HINT = "simp_trace_hint"
+ val SIMP_TRACE_IGNORE = "simp_trace_ignore"
- val MEMORY = "memory"
- val Memory = new Properties.Boolean(MEMORY)
-
- val CANCEL_SIMP_TRACE = "simp_trace_cancel"
- object Cancel_Simp_Trace
+ val SIMP_TRACE_CANCEL = "simp_trace_cancel"
+ object Simp_Trace_Cancel
{
def unapply(props: Properties.T): Option[Long] =
props match {
- case (FUNCTION, CANCEL_SIMP_TRACE) :: Serial(id) => Some(id)
+ case (FUNCTION, SIMP_TRACE_CANCEL) :: Serial(i) => Some(i)
case _ => None
}
}
-
- val SIMP_TRACE = "simp_trace"
- object Simp_Trace
- {
- def unapply(tree: XML.Tree): Option[(Long, Simplifier_Trace.Answer)] =
- tree match {
- case XML.Elem(Markup(SIMP_TRACE, props), _) =>
- (props, props) match {
- case (Serial(serial), Name(name)) =>
- Simplifier_Trace.all_answers.find(_.name == name).map((serial, _))
- case _ =>
- None
- }
- case _ =>
- None
- }
- }
-
- /* trace items from the prover */
-
- object Simp_Trace_Item
- {
-
- def unapply(tree: XML.Tree): Option[(String, Data)] =
- tree match {
- case XML.Elem(Markup(RESULT, Serial(serial)), List(
- XML.Elem(Markup(markup, props), content)
- )) if markup.startsWith("simp_trace_") =>
- (props, props) match {
- case (Text(text), Parent(parent)) =>
- Some((markup, Data(serial, markup, text, parent, props, content)))
- case _ =>
- None
- }
- case _ =>
- None
- }
-
- val LOG = "simp_trace_log"
- val STEP = "simp_trace_step"
- val RECURSE = "simp_trace_recurse"
- val HINT = "simp_trace_hint"
- val IGNORE = "simp_trace_ignore"
-
- case class Data(serial: Long, markup: String, text: String,
- parent: Long, props: Properties.T, content: XML.Body)
- {
- def memory: Boolean =
- Memory.unapply(props) getOrElse true
- }
-
- }
-
}
--- a/src/Pure/PIDE/protocol.scala Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Pure/PIDE/protocol.scala Tue Feb 18 23:08:55 2014 +0100
@@ -282,10 +282,12 @@
{
def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
props match {
- case Position.Reported(id, file_name, range)
+ case Position.Reported(id, file_name, raw_range)
if (id == command_id || id == alt_id) && file_name == chunk.file_name =>
- val range1 = chunk.decode(range).restrict(chunk.range)
- if (range1.is_singularity) set else set + range1
+ chunk.decode(raw_range).try_restrict(chunk.range) match {
+ case Some(range) if !range.is_singularity => set + range
+ case _ => set
+ }
case _ => set
}
--- a/src/Pure/PIDE/yxml.scala Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Pure/PIDE/yxml.scala Tue Feb 18 23:08:55 2014 +0100
@@ -33,7 +33,7 @@
def tree(t: XML.Tree): Unit =
t match {
case XML.Elem(Markup(name, atts), ts) =>
- s += X; s += Y; s++= name; atts.foreach(attrib); s += X
+ s += X; s += Y; s ++= name; atts.foreach(attrib); s += X
ts.foreach(tree)
s += X; s += Y; s += X
case XML.Text(text) => s ++= text
@@ -120,7 +120,7 @@
/* failsafe parsing */
private def markup_broken(source: CharSequence) =
- XML.elem(Markup.Broken.name, List(XML.Text(source.toString)))
+ XML.Elem(Markup.Broken, List(XML.Text(source.toString)))
def parse_body_failsafe(source: CharSequence): XML.Body =
{
--- a/src/Pure/Syntax/syntax_phases.ML Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Tue Feb 18 23:08:55 2014 +0100
@@ -342,7 +342,7 @@
Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
fun parse_sort ctxt =
- Syntax.parse_token ctxt Term_XML.Decode.sort Markup.sort
+ Syntax.parse_token ctxt Term_XML.Decode.sort Markup.language_sort
(fn (syms, pos) =>
parse_tree ctxt "sort" (syms, pos)
|> uncurry (report_result ctxt pos)
@@ -351,7 +351,7 @@
handle ERROR msg => parse_failed ctxt pos msg "sort");
fun parse_typ ctxt =
- Syntax.parse_token ctxt Term_XML.Decode.typ Markup.typ
+ Syntax.parse_token ctxt Term_XML.Decode.typ Markup.language_type
(fn (syms, pos) =>
parse_tree ctxt "type" (syms, pos)
|> uncurry (report_result ctxt pos)
@@ -362,8 +362,8 @@
let
val (markup, kind, root, constrain) =
if is_prop
- then (Markup.prop, "proposition", "prop", Type.constraint propT)
- else (Markup.term, "term", Config.get ctxt Syntax.root, I);
+ then (Markup.language_prop, "prop", "prop", Type.constraint propT)
+ else (Markup.language_term, "term", Config.get ctxt Syntax.root, I);
val decode = constrain o Term_XML.Decode.term;
in
Syntax.parse_token ctxt decode markup
@@ -749,8 +749,8 @@
in
-val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Markup.sort;
-val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Markup.typ;
+val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Markup.language_sort;
+val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Markup.language_type;
fun unparse_term ctxt =
let
@@ -760,7 +760,7 @@
in
unparse_t (term_to_ast idents (is_some o Syntax.lookup_const syn))
(Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy)))
- Markup.term ctxt
+ Markup.language_term ctxt
end;
end;
--- a/src/Pure/System/isabelle_system.scala Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Pure/System/isabelle_system.scala Tue Feb 18 23:08:55 2014 +0100
@@ -267,7 +267,7 @@
def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
{
val cmdline =
- if (Platform.is_windows) List(get_cygwin_root() + "\\bin\\env.exe") ++ args
+ if (Platform.is_windows) List(get_cygwin_root() + "\\bin\\env.exe") ::: args.toList
else args
val env1 = if (env == null) settings else settings ++ env
raw_execute(cwd, env1, redirect, cmdline: _*)
@@ -283,7 +283,7 @@
{
private val params =
List(standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
- private val proc = execute_env(cwd, env, redirect, (params ++ args):_*)
+ private val proc = execute_env(cwd, env, redirect, (params ::: args.toList):_*)
// channels
@@ -414,7 +414,7 @@
} match {
case Some(dir) =>
val file = standard_path(dir + Path.basic(name))
- process_output(execute(true, (List(file) ++ args): _*))
+ process_output(execute(true, (List(file) ::: args.toList): _*))
case None => ("Unknown Isabelle tool: " + name, 2)
}
}
--- a/src/Pure/Thy/thy_output.ML Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML Tue Feb 18 23:08:55 2014 +0100
@@ -188,7 +188,7 @@
fun check_text (txt, pos) state =
- (Position.report pos Markup.document_source;
+ (Position.report pos Markup.language_document;
if Toplevel.is_skipped_proof state then ()
else ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
@@ -470,6 +470,9 @@
fun pretty_text ctxt =
Pretty.chunks o map Pretty.str o map (tweak_line ctxt) o split_lines;
+fun pretty_text_report ctxt (s, pos) =
+ (Context_Position.report ctxt pos Markup.language_text; pretty_text ctxt s);
+
fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
@@ -574,7 +577,7 @@
basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
basic_entity (Binding.name "class") (Scan.lift Args.name_inner_syntax) pretty_class #>
basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
- basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #>
+ basic_entity (Binding.name "text") (Scan.lift (Parse.position Args.name)) pretty_text_report #>
basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
basic_entities (Binding.name "full_prf") Attrib.thms (pretty_prf true) #>
basic_entity (Binding.name "theory") (Scan.lift (Parse.position Args.name)) pretty_theory);
--- a/src/Pure/Tools/simplifier_trace.ML Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Pure/Tools/simplifier_trace.ML Tue Feb 18 23:08:55 2014 +0100
@@ -13,7 +13,7 @@
structure Simplifier_Trace: SIMPLIFIER_TRACE =
struct
-(** background data **)
+(** context data **)
datatype mode = Disabled | Normal | Full
@@ -23,7 +23,7 @@
| merge_modes Full _ = Full
val empty_breakpoints =
- (Item_Net.init (op =) single (* FIXME equality on terms? *),
+ (Item_Net.init (op aconv) single,
Item_Net.init eq_rrule (single o Thm.full_prop_of o #thm))
fun merge_breakpoints ((term_bs1, thm_bs1), (term_bs2, thm_bs2)) =
@@ -49,10 +49,11 @@
parent = 0,
breakpoints = empty_breakpoints}
val extend = I
- fun merge ({max_depth = max_depth1, mode = mode1, interactive = interactive1,
- memory = memory1, breakpoints = breakpoints1, ...}: T,
- {max_depth = max_depth2, mode = mode2, interactive = interactive2,
- memory = memory2, breakpoints = breakpoints2, ...}: T) =
+ fun merge
+ ({max_depth = max_depth1, mode = mode1, interactive = interactive1,
+ memory = memory1, breakpoints = breakpoints1, ...}: T,
+ {max_depth = max_depth2, mode = mode2, interactive = interactive2,
+ memory = memory2, breakpoints = breakpoints2, ...}: T) =
{max_depth = Int.max (max_depth1, max_depth2),
depth = 0,
mode = merge_modes mode1 mode2,
@@ -97,14 +98,17 @@
(term_matches, thm_matches)
end
+
+
(** config and attributes **)
fun config raw_mode interactive max_depth memory =
let
- val mode = case raw_mode of
- "normal" => Normal
- | "full" => Full
- | _ => error ("Simplifier_Trace.config: unknown mode " ^ raw_mode)
+ val mode =
+ (case raw_mode of
+ "normal" => Normal
+ | "full" => Full
+ | _ => error ("Simplifier_Trace.config: unknown mode " ^ raw_mode))
val update = Data.map (fn {depth, parent, breakpoints, ...} =>
{max_depth = max_depth,
@@ -122,11 +126,15 @@
val thm_breakpoint =
Thm.declaration_attribute add_thm_breakpoint
+
+
(** tracing state **)
val futures =
Synchronized.var "Simplifier_Trace.futures" (Inttab.empty: string future Inttab.table)
+
+
(** markup **)
fun output_result (id, data) =
@@ -138,14 +146,6 @@
val memoryN = "memory"
val successN = "success"
-val logN = "simp_trace_log"
-val stepN = "simp_trace_step"
-val recurseN = "simp_trace_recurse"
-val hintN = "simp_trace_hint"
-val ignoreN = "simp_trace_ignore"
-
-val cancelN = "simp_trace_cancel"
-
type payload =
{props: Properties.T,
pretty: Pretty.T}
@@ -158,15 +158,17 @@
val {max_depth, depth, mode, interactive, memory, parent, ...} = Data.get (Context.Proof ctxt)
val eligible =
- case mode of
+ (case mode of
Disabled => false
| Normal => triggered
- | Full => true
+ | Full => true)
- val markup' = if markup = stepN andalso not interactive then logN else markup
+ val markup' =
+ if markup = Markup.simp_trace_stepN andalso not interactive
+ then Markup.simp_trace_logN
+ else markup
in
- if not eligible orelse depth > max_depth then
- NONE
+ if not eligible orelse depth > max_depth then NONE
else
let
val {props = more_props, pretty} = payload ()
@@ -181,15 +183,14 @@
end
end
+
+
(** tracing output **)
fun send_request (result_id, content) =
let
fun break () =
- (Output.protocol_message
- [(Markup.functionN, cancelN),
- (serialN, Markup.print_int result_id)]
- "";
+ (Output.protocol_message (Markup.simp_trace_cancel result_id) "";
Synchronized.change futures (Inttab.delete_safe result_id))
val promise = Future.promise break : string future
in
@@ -209,10 +210,8 @@
val term_triggered = not (null matching_terms)
val text =
- if unconditional then
- "Apply rewrite rule?"
- else
- "Apply conditional rewrite rule?"
+ if unconditional then "Apply rewrite rule?"
+ else "Apply conditional rewrite rule?"
fun payload () =
let
@@ -233,8 +232,7 @@
in
if not (null matching_terms) then
[Pretty.block (Pretty.fbreaks (Pretty.str "Matching terms:" :: items))]
- else
- []
+ else []
end
val pretty =
@@ -269,14 +267,14 @@
in
if not interactive then
(output_result result; Future.value (SOME (put mode false)))
- else
- Future.map to_response (send_request result)
+ else Future.map to_response (send_request result)
end
in
- case mk_generic_result stepN text (thm_triggered orelse term_triggered) payload ctxt of
+ (case mk_generic_result Markup.simp_trace_stepN text
+ (thm_triggered orelse term_triggered) payload ctxt of
NONE => Future.value (SOME ctxt)
- | SOME res => mk_promise res
+ | SOME res => mk_promise res)
end
fun recurse text term ctxt =
@@ -298,11 +296,9 @@
breakpoints = breakpoints} (Context.Proof ctxt)
val context' =
- case mk_generic_result recurseN text true payload ctxt of
- NONE =>
- put 0
- | SOME res =>
- (output_result res; put (#1 res))
+ (case mk_generic_result Markup.simp_trace_recurseN text true payload ctxt of
+ NONE => put 0
+ | SOME res => (output_result res; put (#1 res)))
in Context.the_proof context' end
fun indicate_failure ({term, ctxt, thm, rrule, ...}: data) ctxt' =
@@ -336,24 +332,21 @@
let
val result_id = #1 result
- fun to_response "exit" =
- false
+ fun to_response "exit" = false
| to_response "redo" =
(Option.app output_result
- (mk_generic_result ignoreN "Ignore" true empty_payload ctxt');
+ (mk_generic_result Markup.simp_trace_ignoreN "Ignore" true empty_payload ctxt');
true)
- | to_response _ =
- raise Fail "Simplifier_Trace.indicate_failure: invalid message"
+ | to_response _ = raise Fail "Simplifier_Trace.indicate_failure: invalid message"
in
if not interactive then
(output_result result; Future.value false)
- else
- Future.map to_response (send_request result)
+ else Future.map to_response (send_request result)
end
in
- case mk_generic_result hintN "Step failed" true payload ctxt' of
+ (case mk_generic_result Markup.simp_trace_hintN "Step failed" true payload ctxt' of
NONE => Future.value false
- | SOME res => mk_promise res
+ | SOME res => mk_promise res)
end
fun indicate_success thm ctxt =
@@ -362,9 +355,12 @@
{props = [(successN, "true")],
pretty = Syntax.pretty_term ctxt (Thm.prop_of thm)}
in
- Option.app output_result (mk_generic_result hintN "Successfully rewrote" true payload ctxt)
+ Option.app output_result
+ (mk_generic_result Markup.simp_trace_hintN "Successfully rewrote" true payload ctxt)
end
+
+
(** setup **)
fun simp_apply args ctxt cont =
@@ -377,21 +373,17 @@
thm = thm,
rrule = rrule}
in
- case Future.join (step data) of
- NONE =>
- NONE
+ (case Future.join (step data) of
+ NONE => NONE
| SOME ctxt' =>
let val res = cont ctxt' in
- case res of
+ (case res of
NONE =>
if Future.join (indicate_failure data ctxt') then
simp_apply args ctxt cont
- else
- NONE
- | SOME (thm, _) =>
- (indicate_success thm ctxt';
- res)
- end
+ else NONE
+ | SOME (thm, _) => (indicate_success thm ctxt'; res))
+ end)
end
val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler"
@@ -402,7 +394,7 @@
trace_apply = simp_apply})
val _ =
- Isabelle_Process.protocol_command "Document.simp_trace_reply"
+ Isabelle_Process.protocol_command "Simplifier_Trace.reply"
(fn [s, r] =>
let
val serial = Markup.parse_int s
@@ -415,20 +407,19 @@
handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn
end)
+
+
(** attributes **)
-val pat_parser =
- Args.context -- Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_schematic
-
-val mode_parser: string parser =
+val mode_parser =
Scan.optional
(Args.$$$ "mode" |-- Args.$$$ "=" |-- (Args.$$$ "normal" || Args.$$$ "full"))
"normal"
-val interactive_parser: bool parser =
+val interactive_parser =
Scan.optional (Args.$$$ "interactive" >> K true) false
-val memory_parser: bool parser =
+val memory_parser =
Scan.optional (Args.$$$ "no_memory" >> K false) true
val depth_parser =
@@ -440,7 +431,7 @@
val _ = Theory.setup
(Attrib.setup @{binding break_term}
- ((Scan.repeat1 pat_parser) >> term_breakpoint)
+ (Scan.repeat1 Args.term_pattern >> term_breakpoint)
"declaration of a term breakpoint" #>
Attrib.setup @{binding break_thm}
(Scan.succeed thm_breakpoint)
--- a/src/Pure/Tools/simplifier_trace.scala Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Pure/Tools/simplifier_trace.scala Tue Feb 18 23:08:55 2014 +0100
@@ -6,6 +6,7 @@
package isabelle
+
import scala.actors.Actor._
import scala.annotation.tailrec
import scala.collection.immutable.SortedMap
@@ -13,8 +14,42 @@
object Simplifier_Trace
{
+ /* trace items from the prover */
- import Markup.Simp_Trace_Item
+ val TEXT = "text"
+ val Text = new Properties.String(TEXT)
+
+ val PARENT = "parent"
+ val Parent = new Properties.Long(PARENT)
+
+ val SUCCESS = "success"
+ val Success = new Properties.Boolean(SUCCESS)
+
+ val MEMORY = "memory"
+ val Memory = new Properties.Boolean(MEMORY)
+
+ object Item
+ {
+ case class Data(
+ serial: Long, markup: String, text: String,
+ parent: Long, props: Properties.T, content: XML.Body)
+ {
+ def memory: Boolean = Memory.unapply(props) getOrElse true
+ }
+
+ def unapply(tree: XML.Tree): Option[(String, Data)] =
+ tree match {
+ case XML.Elem(Markup(Markup.RESULT, Markup.Serial(serial)),
+ List(XML.Elem(Markup(markup, props), content)))
+ if markup.startsWith("simp_trace_") => // FIXME proper comparison of string constants
+ (props, props) match {
+ case (Text(text), Parent(parent)) =>
+ Some((markup, Data(serial, markup, text, parent, props, content)))
+ case _ => None
+ }
+ case _ => None
+ }
+ }
/* replies to the prover */
@@ -23,7 +58,6 @@
object Answer
{
-
object step
{
val skip = Answer("skip", "Skip")
@@ -44,10 +78,23 @@
val default = exit
val all = List(redo, exit)
}
-
}
- val all_answers = Answer.step.all ++ Answer.hint_fail.all
+ val all_answers: List[Answer] = Answer.step.all ::: Answer.hint_fail.all
+
+ object Active
+ {
+ def unapply(tree: XML.Tree): Option[(Long, Answer)] =
+ tree match {
+ case XML.Elem(Markup(Markup.SIMP_TRACE, props), _) =>
+ (props, props) match {
+ case (Markup.Serial(serial), Markup.Name(name)) =>
+ all_answers.find(_.name == name).map((serial, _))
+ case _ => None
+ }
+ case _ => None
+ }
+ }
/* GUI interaction */
@@ -64,7 +111,7 @@
private object Stop
case class Reply(session: Session, serial: Long, answer: Answer)
- case class Question(data: Simp_Trace_Item.Data, answers: List[Answer], default_answer: Answer)
+ case class Question(data: Item.Data, answers: List[Answer], default_answer: Answer)
case class Context(
last_serial: Long = 0L,
@@ -83,13 +130,13 @@
}
- case class Trace(entries: List[Simp_Trace_Item.Data])
+ case class Trace(entries: List[Item.Data])
case class Index(text: String, content: XML.Body)
object Index
{
- def of_data(data: Simp_Trace_Item.Data): Index =
+ def of_data(data: Item.Data): Index =
Index(data.text, data.content)
}
@@ -128,7 +175,7 @@
def do_reply(session: Session, serial: Long, answer: Answer)
{
- session.protocol_command("Document.simp_trace_reply", Properties.Value.Long(serial), answer.name)
+ session.protocol_command("Simplifier_Trace.reply", Properties.Value.Long(serial), answer.name)
}
loop {
@@ -140,14 +187,12 @@
for ((serial, result) <- results.entries if serial > new_context.last_serial)
{
result match {
- case Simp_Trace_Item(markup, data) =>
- import Simp_Trace_Item._
-
+ case Item(markup, data) =>
memory_children += (data.parent -> (memory_children.getOrElse(data.parent, Set.empty) + serial))
markup match {
- case STEP =>
+ case Markup.SIMP_TRACE_STEP =>
val index = Index.of_data(data)
memory.get(index) match {
case Some(answer) if data.memory =>
@@ -156,11 +201,11 @@
new_context += Question(data, Answer.step.all, Answer.step.default)
}
- case HINT =>
+ case Markup.SIMP_TRACE_HINT =>
data.props match {
- case Markup.Success(false) =>
+ case Success(false) =>
results.get(data.parent) match {
- case Some(Simp_Trace_Item(STEP, _)) =>
+ case Some(Item(Markup.SIMP_TRACE_STEP, _)) =>
new_context += Question(data, Answer.hint_fail.all, Answer.hint_fail.default)
case _ =>
// unknown, better send a default reply
@@ -169,7 +214,7 @@
case _ =>
}
- case IGNORE =>
+ case Markup.SIMP_TRACE_IGNORE =>
// At this point, we know that the parent of this 'IGNORE' entry is a 'STEP'
// entry, and that that 'STEP' entry is about to be replayed. Hence, we need
// to selectively purge the replies which have been memorized, going down from
@@ -179,7 +224,7 @@
def purge(queue: Vector[Long]): Unit =
queue match {
case s +: rest =>
- for (Simp_Trace_Item(STEP, data) <- results.get(s))
+ for (Item(Markup.SIMP_TRACE_STEP, data) <- results.get(s))
memory -= Index.of_data(data)
val children = memory_children.getOrElse(s, Set.empty)
memory_children -= s
@@ -208,7 +253,7 @@
// current results.
val items =
- for { (_, Simp_Trace_Item(_, data)) <- results.entries }
+ for { (_, Item(_, data)) <- results.entries }
yield data
reply(Trace(items.toList))
@@ -232,7 +277,7 @@
case Reply(session, serial, answer) =>
find_question(serial) match {
case Some((id, Question(data, _, _))) =>
- if (data.markup == Markup.Simp_Trace_Item.STEP && data.memory)
+ if (data.markup == Markup.SIMP_TRACE_STEP && data.memory)
{
val index = Index.of_data(data)
memory += (index -> answer)
@@ -256,10 +301,9 @@
class Handler extends Session.Protocol_Handler
{
- private def cancel(
- prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean =
+ private def cancel(prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean =
msg.properties match {
- case Markup.Cancel_Simp_Trace(serial) =>
+ case Markup.Simp_Trace_Cancel(serial) =>
manager ! Cancel(serial)
true
case _ =>
@@ -272,8 +316,6 @@
manager ! Stop
}
- val functions = Map(
- Markup.CANCEL_SIMP_TRACE -> cancel _)
+ val functions = Map(Markup.SIMP_TRACE_CANCEL -> cancel _)
}
-
}
--- a/src/Pure/context.ML Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Pure/context.ML Tue Feb 18 23:08:55 2014 +0100
@@ -43,7 +43,6 @@
val this_theory: theory -> string -> theory
val eq_thy: theory * theory -> bool
val subthy: theory * theory -> bool
- val joinable: theory * theory -> bool
val merge: theory * theory -> theory
val finish_thy: theory -> theory
val begin_thy: (theory -> pretty) -> string -> theory list -> theory
@@ -246,8 +245,6 @@
fun subthy thys = eq_thy thys orelse proper_subthy thys;
-fun joinable (thy1, thy2) = subthy (thy1, thy2) orelse subthy (thy2, thy1);
-
(* consistent ancestors *)
--- a/src/Pure/defs.ML Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Pure/defs.ML Tue Feb 18 23:08:55 2014 +0100
@@ -11,7 +11,11 @@
val plain_args: typ list -> bool
type T
type spec =
- {def: string option, description: string, lhs: typ list, rhs: (string * typ list) list}
+ {def: string option,
+ description: string,
+ pos: Position.T,
+ lhs: typ list,
+ rhs: (string * typ list) list}
val all_specifications_of: T -> (string * spec list) list
val specifications_of: T -> string -> spec list
val dest: T ->
@@ -53,11 +57,15 @@
(* datatype defs *)
type spec =
- {def: string option, description: string, lhs: args, rhs: (string * args) list};
+ {def: string option,
+ description: string,
+ pos: Position.T,
+ lhs: args,
+ rhs: (string * args) list};
type def =
- {specs: spec Inttab.table, (*source specifications*)
- restricts: (args * string) list, (*global restrictions imposed by incomplete patterns*)
+ {specs: spec Inttab.table, (*source specifications*)
+ restricts: (args * string) list, (*global restrictions imposed by incomplete patterns*)
reducts: (args * (string * args) list) list}; (*specifications as reduction system*)
fun make_def (specs, restricts, reducts) =
@@ -97,11 +105,12 @@
(* specifications *)
-fun disjoint_specs c (i, {lhs = Ts, description = a, ...}: spec) =
- Inttab.forall (fn (j, {lhs = Us, description = b, ...}: spec) =>
+fun disjoint_specs c (i, {description = a, pos = pos_a, lhs = Ts, ...}: spec) =
+ Inttab.forall (fn (j, {description = b, pos = pos_b, lhs = Us, ...}: spec) =>
i = j orelse disjoint_args (Ts, Us) orelse
- error ("Clash of specifications " ^ quote a ^ " and " ^ quote b ^
- " for constant " ^ quote c));
+ error ("Clash of specifications for constant " ^ quote c ^ ":\n" ^
+ " " ^ quote a ^ Position.here pos_a ^ "\n" ^
+ " " ^ quote b ^ Position.here pos_b));
fun join_specs c ({specs = specs1, restricts, reducts}, {specs = specs2, ...}: def) =
let
@@ -204,12 +213,13 @@
fun define ctxt unchecked def description (c, args) deps (Defs defs) =
let
+ val pos = Position.thread_data ();
val restr =
if plain_args args orelse
(case args of [Type (_, rec_args)] => plain_args rec_args | _ => false)
then [] else [(args, description)];
val spec =
- (serial (), {def = def, description = description, lhs = args, rhs = deps});
+ (serial (), {def = def, description = description, pos = pos, lhs = args, rhs = deps});
val defs' = defs |> update_specs c spec;
in Defs (defs' |> (if unchecked then I else dependencies ctxt (c, args) restr deps)) end;
--- a/src/Pure/goal.ML Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Pure/goal.ML Tue Feb 18 23:08:55 2014 +0100
@@ -187,10 +187,10 @@
val skip = not immediate andalso not schematic andalso future andalso skip_proofs_enabled ();
val pos = Position.thread_data ();
- fun err msg = cat_error msg
- ("The error(s) above occurred for the goal statement:\n" ^
- Syntax.string_of_term ctxt (Logic.list_implies (asms, Logic.mk_conjunction_list props)) ^
- (case Position.here pos of "" => "" | s => "\n" ^ s));
+ fun err msg =
+ cat_error msg
+ ("The error(s) above occurred for the goal statement" ^ Position.here pos ^ ":\n" ^
+ Syntax.string_of_term ctxt (Logic.list_implies (asms, Logic.mk_conjunction_list props)));
fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm (Term.no_dummy_patterns t))
handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
--- a/src/Pure/more_thm.ML Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Pure/more_thm.ML Tue Feb 18 23:08:55 2014 +0100
@@ -37,7 +37,6 @@
val thm_cache: (thm -> 'a) -> thm -> 'a
val is_reflexive: thm -> bool
val eq_thm: thm * thm -> bool
- val eq_thm_thy: thm * thm -> bool
val eq_thm_prop: thm * thm -> bool
val eq_thm_strict: thm * thm -> bool
val equiv_thm: thm * thm -> bool
@@ -191,17 +190,17 @@
fun is_reflexive th = op aconv (Logic.dest_equals (Thm.prop_of th))
handle TERM _ => false;
-fun eq_thm ths =
- Context.joinable (pairself Thm.theory_of_thm ths) andalso
- is_equal (thm_ord ths);
+val eq_thm = is_equal o thm_ord;
-val eq_thm_thy = Theory.eq_thy o pairself Thm.theory_of_thm;
val eq_thm_prop = op aconv o pairself Thm.full_prop_of;
fun eq_thm_strict ths =
- eq_thm_thy ths andalso eq_thm ths andalso
- let val (rep1, rep2) = pairself Thm.rep_thm ths
- in #maxidx rep1 = #maxidx rep2 andalso #tags rep1 = #tags rep2 end;
+ eq_thm ths andalso
+ let val (rep1, rep2) = pairself Thm.rep_thm ths in
+ Theory.eq_thy (#thy rep1, #thy rep2) andalso
+ #maxidx rep1 = #maxidx rep2 andalso
+ #tags rep1 = #tags rep2
+ end;
(* pattern equivalence *)
--- a/src/Tools/jEdit/src/Isabelle.props Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Tools/jEdit/src/Isabelle.props Tue Feb 18 23:08:55 2014 +0100
@@ -27,48 +27,48 @@
options.isabelle-rendering.label=Rendering
options.isabelle-rendering.code=new isabelle.jedit.Isabelle_Options2();
-#menu actions
+#menu actions and dockables
plugin.isabelle.jedit.Plugin.menu.label=Isabelle
plugin.isabelle.jedit.Plugin.menu= \
- isabelle.documentation-panel \
- isabelle.find-panel \
- isabelle.monitor-panel \
- isabelle.output-panel \
- isabelle.protocol-panel \
- isabelle.raw-output-panel \
- isabelle.sledgehammer-panel \
- isabelle.simp-trace-panel \
- isabelle.symbols-panel \
- isabelle.syslog-panel \
- isabelle.theories-panel \
- isabelle.timing-panel
-isabelle.documentation-panel.label=Documentation panel
-isabelle.find-panel.label=Find panel
-isabelle.monitor-panel.label=Monitor panel
-isabelle.output-panel.label=Output panel
-isabelle.protocol-panel.label=Protocol panel
-isabelle.raw-output-panel.label=Raw Output panel
-isabelle.simp-trace-panel.label=Simplifier trace panel
-isabelle.sledgehammer-panel.label=Sledgehammer panel
-isabelle.symbols-panel.label=Symbols panel
-isabelle.syslog-panel.label=Syslog panel
-isabelle.theories-panel.label=Theories panel
-isabelle.timing-panel.label=Timing panel
-
-#dockables
+ isabelle-documentation \
+ isabelle-find \
+ isabelle-monitor \
+ isabelle-output \
+ isabelle-protocol \
+ isabelle-raw-output \
+ isabelle-simplifier-trace \
+ isabelle-sledgehammer \
+ isabelle-symbols \
+ isabelle-syslog \
+ isabelle-theories \
+ isabelle-timing
+isabelle-documentation.label=Documentation panel
+isabelle-documentation.title=Documentation
+isabelle-find.label=Find panel
isabelle-find.title=Find
+isabelle-graphview.label=Graphview panel
isabelle-graphview.title=Graphview
+isabelle-info.label=Info panel
isabelle-info.title=Info
+isabelle-monitor.label=Monitor panel
isabelle-monitor.title=Monitor
+isabelle-output.label=Output panel
isabelle-output.title=Output
-isabelle-simp-trace.title=Simplifier trace
+isabelle-protocol.label=Protocol panel
isabelle-protocol.title=Protocol
+isabelle-raw-output.label=Raw Output panel
isabelle-raw-output.title=Raw Output
-isabelle-documentation.title=Documentation
+isabelle-simplifier-trace.label=Simplifier Trace panel
+isabelle-simplifier-trace.title=Simplifier Trace
+isabelle-sledgehammer.label=Sledgehammer panel
isabelle-sledgehammer.title=Sledgehammer
+isabelle-symbols.label=Symbols panel
isabelle-symbols.title=Symbols
+isabelle-syslog.label=Syslog panel
isabelle-syslog.title=Syslog
+isabelle-theories.label=Theories panel
isabelle-theories.title=Theories
+isabelle-timing.label=Timing panel
isabelle-timing.title=Timing
#SideKick
--- a/src/Tools/jEdit/src/actions.xml Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Tools/jEdit/src/actions.xml Tue Feb 18 23:08:55 2014 +0100
@@ -2,66 +2,6 @@
<!DOCTYPE ACTIONS SYSTEM "actions.dtd">
<ACTIONS>
- <ACTION NAME="isabelle.theories-panel">
- <CODE>
- wm.addDockableWindow("isabelle-theories");
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.timing-panel">
- <CODE>
- wm.addDockableWindow("isabelle-timing");
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.syslog-panel">
- <CODE>
- wm.addDockableWindow("isabelle-syslog");
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.documentation-panel">
- <CODE>
- wm.addDockableWindow("isabelle-documentation");
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.find-panel">
- <CODE>
- wm.addDockableWindow("isabelle-find");
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.sledgehammer-panel">
- <CODE>
- wm.addDockableWindow("isabelle-sledgehammer");
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.output-panel">
- <CODE>
- wm.addDockableWindow("isabelle-output");
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.raw-output-panel">
- <CODE>
- wm.addDockableWindow("isabelle-raw-output");
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.simp-trace-panel">
- <CODE>
- wm.addDockableWindow("isabelle-simp-trace");
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.protocol-panel">
- <CODE>
- wm.addDockableWindow("isabelle-protocol");
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.monitor-panel">
- <CODE>
- wm.addDockableWindow("isabelle-monitor");
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.symbols-panel">
- <CODE>
- wm.addDockableWindow("isabelle-symbols");
- </CODE>
- </ACTION>
<ACTION NAME="isabelle.set-continuous-checking">
<CODE>
isabelle.jedit.Isabelle.set_continuous_checking();
--- a/src/Tools/jEdit/src/active.scala Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Tools/jEdit/src/active.scala Tue Feb 18 23:08:55 2014 +0100
@@ -61,7 +61,7 @@
else text_area.setSelectedText(text)
}
- case Markup.Simp_Trace(serial, answer) =>
+ case Simplifier_Trace.Active(serial, answer) =>
Simplifier_Trace.send_reply(PIDE.session, serial, answer)
case Protocol.Dialog(id, serial, result) =>
--- a/src/Tools/jEdit/src/dockables.xml Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Tools/jEdit/src/dockables.xml Tue Feb 18 23:08:55 2014 +0100
@@ -2,46 +2,46 @@
<!DOCTYPE DOCKABLES SYSTEM "dockables.dtd">
<DOCKABLES>
- <DOCKABLE NAME="isabelle-theories" MOVABLE="TRUE">
- new isabelle.jedit.Theories_Dockable(view, position);
- </DOCKABLE>
- <DOCKABLE NAME="isabelle-timing" MOVABLE="TRUE">
- new isabelle.jedit.Timing_Dockable(view, position);
- </DOCKABLE>
- <DOCKABLE NAME="isabelle-syslog" MOVABLE="TRUE">
- new isabelle.jedit.Syslog_Dockable(view, position);
- </DOCKABLE>
<DOCKABLE NAME="isabelle-documentation" MOVABLE="TRUE">
new isabelle.jedit.Documentation_Dockable(view, position);
</DOCKABLE>
- <DOCKABLE NAME="isabelle-output" MOVABLE="TRUE">
- new isabelle.jedit.Output_Dockable(view, position);
- </DOCKABLE>
<DOCKABLE NAME="isabelle-find" MOVABLE="TRUE">
new isabelle.jedit.Find_Dockable(view, position);
</DOCKABLE>
- <DOCKABLE NAME="isabelle-sledgehammer" MOVABLE="TRUE">
- new isabelle.jedit.Sledgehammer_Dockable(view, position);
- </DOCKABLE>
<DOCKABLE NAME="isabelle-info" MOVABLE="TRUE">
new isabelle.jedit.Info_Dockable(view, position);
</DOCKABLE>
<DOCKABLE NAME="isabelle-graphview" MOVABLE="TRUE">
new isabelle.jedit.Graphview_Dockable(view, position);
</DOCKABLE>
- <DOCKABLE NAME="isabelle-raw-output" MOVABLE="TRUE">
- new isabelle.jedit.Raw_Output_Dockable(view, position);
+ <DOCKABLE NAME="isabelle-monitor" MOVABLE="TRUE">
+ new isabelle.jedit.Monitor_Dockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="isabelle-output" MOVABLE="TRUE">
+ new isabelle.jedit.Output_Dockable(view, position);
</DOCKABLE>
<DOCKABLE NAME="isabelle-protocol" MOVABLE="TRUE">
new isabelle.jedit.Protocol_Dockable(view, position);
</DOCKABLE>
- <DOCKABLE NAME="isabelle-monitor" MOVABLE="TRUE">
- new isabelle.jedit.Monitor_Dockable(view, position);
+ <DOCKABLE NAME="isabelle-raw-output" MOVABLE="TRUE">
+ new isabelle.jedit.Raw_Output_Dockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="isabelle-simplifier-trace" MOVABLE="TRUE">
+ new isabelle.jedit.Simplifier_Trace_Dockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="isabelle-sledgehammer" MOVABLE="TRUE">
+ new isabelle.jedit.Sledgehammer_Dockable(view, position);
</DOCKABLE>
<DOCKABLE NAME="isabelle-symbols" MOVABLE="TRUE">
new isabelle.jedit.Symbols_Dockable(view, position);
</DOCKABLE>
- <DOCKABLE NAME="isabelle-simp-trace" MOVABLE="TRUE">
- new isabelle.jedit.Simplifier_Trace_Dockable(view, position);
+ <DOCKABLE NAME="isabelle-syslog" MOVABLE="TRUE">
+ new isabelle.jedit.Syslog_Dockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="isabelle-theories" MOVABLE="TRUE">
+ new isabelle.jedit.Theories_Dockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="isabelle-timing" MOVABLE="TRUE">
+ new isabelle.jedit.Timing_Dockable(view, position);
</DOCKABLE>
</DOCKABLES>
--- a/src/Tools/jEdit/src/isabelle.scala Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Tue Feb 18 23:08:55 2014 +0100
@@ -58,45 +58,75 @@
private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
- def docked_theories(view: View): Option[Theories_Dockable] =
- wm(view).getDockableWindow("isabelle-theories") match {
- case dockable: Theories_Dockable => Some(dockable)
+ def documentation_dockable(view: View): Option[Documentation_Dockable] =
+ wm(view).getDockableWindow("isabelle-documentation") match {
+ case dockable: Documentation_Dockable => Some(dockable)
case _ => None
}
- def docked_timing(view: View): Option[Timing_Dockable] =
- wm(view).getDockableWindow("isabelle-timing") match {
- case dockable: Timing_Dockable => Some(dockable)
+ def find_dockable(view: View): Option[Find_Dockable] =
+ wm(view).getDockableWindow("isabelle-find") match {
+ case dockable: Find_Dockable => Some(dockable)
case _ => None
}
- def docked_output(view: View): Option[Output_Dockable] =
+ def monitor_dockable(view: View): Option[Monitor_Dockable] =
+ wm(view).getDockableWindow("isabelle-monitor") match {
+ case dockable: Monitor_Dockable => Some(dockable)
+ case _ => None
+ }
+
+ def output_dockable(view: View): Option[Output_Dockable] =
wm(view).getDockableWindow("isabelle-output") match {
case dockable: Output_Dockable => Some(dockable)
case _ => None
}
- def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
+ def protocol_dockable(view: View): Option[Protocol_Dockable] =
+ wm(view).getDockableWindow("isabelle-protocol") match {
+ case dockable: Protocol_Dockable => Some(dockable)
+ case _ => None
+ }
+
+ def raw_output_dockable(view: View): Option[Raw_Output_Dockable] =
wm(view).getDockableWindow("isabelle-raw-output") match {
case dockable: Raw_Output_Dockable => Some(dockable)
case _ => None
}
- def docked_simplifier_trace(view: View): Option[Simplifier_Trace_Dockable] =
- wm(view).getDockableWindow("isabelle-simp-trace") match {
+ def simplifier_trace_dockable(view: View): Option[Simplifier_Trace_Dockable] =
+ wm(view).getDockableWindow("isabelle-simplifier-trace") match {
case dockable: Simplifier_Trace_Dockable => Some(dockable)
case _ => None
}
- def docked_protocol(view: View): Option[Protocol_Dockable] =
- wm(view).getDockableWindow("isabelle-protocol") match {
- case dockable: Protocol_Dockable => Some(dockable)
+ def sledgehammer_dockable(view: View): Option[Sledgehammer_Dockable] =
+ wm(view).getDockableWindow("isabelle-sledgehammer") match {
+ case dockable: Sledgehammer_Dockable => Some(dockable)
+ case _ => None
+ }
+
+ def symbols_dockable(view: View): Option[Symbols_Dockable] =
+ wm(view).getDockableWindow("isabelle-symbols") match {
+ case dockable: Symbols_Dockable => Some(dockable)
case _ => None
}
- def docked_monitor(view: View): Option[Monitor_Dockable] =
- wm(view).getDockableWindow("isabelle-monitor") match {
- case dockable: Monitor_Dockable => Some(dockable)
+ def syslog_dockable(view: View): Option[Syslog_Dockable] =
+ wm(view).getDockableWindow("isabelle-syslog") match {
+ case dockable: Syslog_Dockable => Some(dockable)
+ case _ => None
+ }
+
+ def theories_dockable(view: View): Option[Theories_Dockable] =
+ wm(view).getDockableWindow("isabelle-theories") match {
+ case dockable: Theories_Dockable => Some(dockable)
+ case _ => None
+ }
+
+ def timing_dockable(view: View): Option[Timing_Dockable] =
+ wm(view).getDockableWindow("isabelle-timing") match {
+ case dockable: Timing_Dockable => Some(dockable)
case _ => None
}
--- a/src/Tools/jEdit/src/jEdit.props Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Tools/jEdit/src/jEdit.props Tue Feb 18 23:08:55 2014 +0100
@@ -188,8 +188,8 @@
isabelle-output.dock-position=bottom
isabelle-output.height=174
isabelle-output.width=412
+isabelle-simplifier-trace.dock-position=bottom
isabelle-sledgehammer.dock-position=bottom
-isabelle-simp-trace.dock-position=bottom
isabelle-symbols.dock-position=bottom
isabelle-theories.dock-position=right
isabelle.complete.label=Complete Isabelle text
--- a/src/Tools/jEdit/src/jedit_lib.scala Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Tue Feb 18 23:08:55 2014 +0100
@@ -222,9 +222,10 @@
try {
val p = text_area.offsetToXY(range.start)
val (q, r) =
- if (stop >= end) (text_area.offsetToXY(end), char_width * (stop - end))
- else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
+ if (try_get_text(buffer, Text.Range(stop - 1, stop)) == Some("\n"))
(text_area.offsetToXY(stop - 1), char_width)
+ else if (stop >= end)
+ (text_area.offsetToXY(end), char_width * (stop - end))
else (text_area.offsetToXY(stop), 0)
(p, q, r)
}
--- a/src/Tools/jEdit/src/rendering.scala Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Tue Feb 18 23:08:55 2014 +0100
@@ -241,10 +241,10 @@
/* markup selectors */
private val highlight_include =
- Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
- Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING, Markup.TYPING, Markup.FREE,
- Markup.SKOLEM, Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE,
- Markup.DOCUMENT_SOURCE)
+ Set(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
+ Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
+ Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
+ Markup.VAR, Markup.TFREE, Markup.TVAR)
def highlight(range: Text.Range): Option[Text.Info[Color]] =
{
@@ -258,7 +258,21 @@
}
- private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH, Markup.URL)
+ private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
+
+ private def hyperlink_file(line: Int, name: String): Option[PIDE.editor.Hyperlink] =
+ if (Path.is_ok(name))
+ Isabelle_System.source_file(Path.explode(name)).map(path =>
+ PIDE.editor.hyperlink_file(Isabelle_System.platform_path(path), line))
+ else None
+
+ private def hyperlink_command(id: Document_ID.Generic, offset: Text.Offset)
+ : Option[PIDE.editor.Hyperlink] =
+ snapshot.state.find_command(snapshot.version, id) match {
+ case Some((node, command)) =>
+ PIDE.editor.hyperlink_command(snapshot, command, offset)
+ case None => None
+ }
def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
{
@@ -281,26 +295,22 @@
case (Markup.KIND, Markup.ML_STRUCT) => true
case _ => false }) =>
- props match {
- case Position.Def_Line_File(line, name) if Path.is_ok(name) =>
- Isabelle_System.source_file(Path.explode(name)) match {
- case Some(path) =>
- val jedit_file = Isabelle_System.platform_path(path)
- val link = PIDE.editor.hyperlink_file(jedit_file, line)
- Some(Text.Info(snapshot.convert(info_range), link) :: links)
- case None => None
- }
+ val opt_link =
+ props match {
+ case Position.Def_Line_File(line, name) => hyperlink_file(line, name)
+ case Position.Def_Id_Offset(id, offset) => hyperlink_command(id, offset)
+ case _ => None
+ }
+ opt_link.map(link => (Text.Info(snapshot.convert(info_range), link) :: links))
- case Position.Def_Id_Offset(id, offset) =>
- snapshot.state.find_command(snapshot.version, id) match {
- case Some((node, command)) =>
- PIDE.editor.hyperlink_command(snapshot, command, offset)
- .map(link => (Text.Info(snapshot.convert(info_range), link) :: links))
- case None => None
- }
-
- case _ => None
- }
+ case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
+ val opt_link =
+ props match {
+ case Position.Line_File(line, name) => hyperlink_file(line, name)
+ case Position.Id_Offset(id, offset) => hyperlink_command(id, offset)
+ case _ => None
+ }
+ opt_link.map(link => (Text.Info(snapshot.convert(info_range), link) :: links))
case _ => None
}) match { case Text.Info(_, info :: _) :: _ => Some(info) case _ => None }
@@ -365,23 +375,18 @@
private val tooltips: Map[String, String] =
Map(
- Markup.SORT -> "sort",
- Markup.TYP -> "type",
- Markup.TERM -> "term",
- Markup.PROP -> "proposition",
Markup.TOKEN_RANGE -> "inner syntax token",
Markup.FREE -> "free variable",
Markup.SKOLEM -> "skolem variable",
Markup.BOUND -> "bound variable",
Markup.VAR -> "schematic variable",
Markup.TFREE -> "free type variable",
- Markup.TVAR -> "schematic type variable",
- Markup.ML_SOURCE -> "ML source",
- Markup.DOCUMENT_SOURCE -> "document source")
+ Markup.TVAR -> "schematic type variable")
private val tooltip_elements =
- Set(Markup.TIMING, Markup.ENTITY, Markup.SORTING, Markup.TYPING,
- Markup.ML_TYPING, Markup.PATH, Markup.URL) ++ tooltips.keys
+ Set(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
+ Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++
+ tooltips.keys
private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
@@ -424,6 +429,8 @@
Some(add(prev, r, (true, pretty_typing("::", body))))
case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
Some(add(prev, r, (false, pretty_typing("ML:", body))))
+ case (prev, Text.Info(r, XML.Elem(Markup.Language(name), _))) =>
+ Some(add(prev, r, (true, XML.Text("language: " + name))))
case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
if (tooltips.isDefinedAt(name))
Some(add(prev, r, (true, XML.Text(tooltips(name)))))
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Tue Feb 18 23:08:55 2014 +0100
@@ -10,7 +10,6 @@
import isabelle._
import scala.actors.Actor._
-
import scala.swing.{Button, CheckBox, Orientation, Separator}
import scala.swing.event.ButtonClicked
@@ -19,6 +18,7 @@
import org.gjt.sp.jedit.View
+
class Simplifier_Trace_Dockable(view: View, position: String) extends Dockable(view, position)
{
Swing_Thread.require()
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala Tue Feb 18 17:52:28 2014 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Tue Feb 18 23:08:55 2014 +0100
@@ -10,12 +10,9 @@
import isabelle._
import scala.annotation.tailrec
-
import scala.collection.immutable.SortedMap
-
import scala.swing.{BorderPanel, CheckBox, Component, Dimension, Frame, Label, TextField}
import scala.swing.event.{Key, KeyPressed}
-
import scala.util.matching.Regex
import java.awt.BorderLayout
@@ -25,17 +22,15 @@
import org.gjt.sp.jedit.View
+
private object Simplifier_Trace_Window
{
-
- import Markup.Simp_Trace_Item
-
sealed trait Trace_Tree
{
var children: SortedMap[Long, Elem_Tree] = SortedMap.empty
val serial: Long
val parent: Option[Trace_Tree]
- var hints: List[Simp_Trace_Item.Data]
+ var hints: List[Simplifier_Trace.Item.Data]
def set_interesting(): Unit
}
@@ -43,17 +38,19 @@
{
val parent = None
val hints = Nil
- def hints_=(xs: List[Simp_Trace_Item.Data]) = throw new IllegalStateException("Root_Tree.hints")
+ def hints_=(xs: List[Simplifier_Trace.Item.Data]) =
+ throw new IllegalStateException("Root_Tree.hints")
def set_interesting() = ()
def format(regex: Option[Regex]): XML.Body =
Pretty.separate(children.values.map(_.format(regex)._2)(collection.breakOut))
}
- final class Elem_Tree(data: Simp_Trace_Item.Data, val parent: Option[Trace_Tree]) extends Trace_Tree
+ final class Elem_Tree(data: Simplifier_Trace.Item.Data, val parent: Option[Trace_Tree])
+ extends Trace_Tree
{
val serial = data.serial
- var hints = List.empty[Simp_Trace_Item.Data]
+ var hints = List.empty[Simplifier_Trace.Item.Data]
var interesting: Boolean = false
def set_interesting(): Unit =
@@ -76,7 +73,7 @@
Some(XML.Elem(Markup(Markup.ITEM, Nil), List(res)))
}
- def format_hint(data: Simp_Trace_Item.Data): XML.Tree =
+ def format_hint(data: Simplifier_Trace.Item.Data): XML.Tree =
Pretty.block(Pretty.separate(
XML.Text(data.text) ::
data.content
@@ -111,19 +108,19 @@
}
@tailrec
- def walk_trace(rest: List[Simp_Trace_Item.Data], lookup: Map[Long, Trace_Tree]): Unit =
+ def walk_trace(rest: List[Simplifier_Trace.Item.Data], lookup: Map[Long, Trace_Tree]): Unit =
rest match {
case Nil =>
()
case head :: tail =>
lookup.get(head.parent) match {
case Some(parent) =>
- if (head.markup == Simp_Trace_Item.HINT)
+ if (head.markup == Markup.SIMP_TRACE_HINT)
{
parent.hints ::= head
walk_trace(tail, lookup)
}
- else if (head.markup == Simp_Trace_Item.IGNORE)
+ else if (head.markup == Markup.SIMP_TRACE_IGNORE)
{
parent.parent match {
case None =>
@@ -137,7 +134,7 @@
{
val entry = new Elem_Tree(head, Some(parent))
parent.children += ((head.serial, entry))
- if (head.markup == Simp_Trace_Item.STEP || head.markup == Simp_Trace_Item.LOG)
+ if (head.markup == Markup.SIMP_TRACE_STEP || head.markup == Markup.SIMP_TRACE_LOG)
entry.set_interesting()
walk_trace(tail, lookup + (head.serial -> entry))
}
@@ -149,11 +146,10 @@
}
-class Simplifier_Trace_Window(view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame
+
+class Simplifier_Trace_Window(
+ view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame
{
-
- import Simplifier_Trace_Window._
-
Swing_Thread.require()
val area = new Pretty_Text_Area(view)
@@ -165,11 +161,11 @@
private val tree = trace.entries.headOption match {
case Some(first) =>
- val tree = new Root_Tree(first.parent)
- walk_trace(trace.entries, Map(first.parent -> tree))
+ val tree = new Simplifier_Trace_Window.Root_Tree(first.parent)
+ Simplifier_Trace_Window.walk_trace(trace.entries, Map(first.parent -> tree))
tree
case None =>
- new Root_Tree(0)
+ new Simplifier_Trace_Window.Root_Tree(0)
}
do_update(None)