--- a/src/Doc/antiquote_setup.ML Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Doc/antiquote_setup.ML Sat Mar 01 23:48:55 2014 +0100
@@ -86,7 +86,9 @@
then txt1 ^ ": " ^ txt2
else txt1 ^ " : " ^ txt2;
val txt' = if kind = "" then txt else kind ^ " " ^ txt;
- val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none (ml (txt1, txt2)); (* ML_Lex.read (!?) *)
+ val _ = (* ML_Lex.read (!?) *)
+ ML_Context.eval_source_in (SOME ctxt) false
+ {delimited = false, text = ml (txt1, txt2), pos = Position.none};
val kind' = if kind = "" then "ML" else "ML " ^ kind;
in
"\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^
--- a/src/HOL/Library/BigO.thy Sat Mar 01 20:40:31 2014 +0100
+++ b/src/HOL/Library/BigO.thy Sat Mar 01 23:48:55 2014 +0100
@@ -19,7 +19,7 @@
\item We have eliminated the @{text O} operator on sets. (Most uses of this seem
to be inessential.)
\item We no longer use @{text "+"} as output syntax for @{text "+o"}
-\item Lemmas involving @{text "sumr"} have been replaced by more general lemmas
+\item Lemmas involving @{text "sumr"} have been replaced by more general lemmas
involving `@{text "setsum"}.
\item The library has been expanded, with e.g.~support for expressions of
the form @{text "f < g + O(h)"}.
@@ -34,14 +34,12 @@
subsection {* Definitions *}
-definition
- bigo :: "('a => 'b::linordered_idom) => ('a => 'b) set" ("(1O'(_'))") where
- "O(f::('a => 'b)) =
- {h. EX c. ALL x. abs (h x) <= c * abs (f x)}"
+definition bigo :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(1O'(_'))")
+ where "O(f:: 'a \<Rightarrow> 'b) = {h. \<exists>c. \<forall>x. abs (h x) \<le> c * abs (f x)}"
-lemma bigo_pos_const: "(EX (c::'a::linordered_idom).
- ALL x. (abs (h x)) <= (c * (abs (f x))))
- = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
+lemma bigo_pos_const:
+ "(\<exists>c::'a::linordered_idom. \<forall>x. abs (h x) \<le> c * abs (f x)) \<longleftrightarrow>
+ (\<exists>c. 0 < c \<and> (\<forall>x. abs (h x) \<le> c * abs (f x)))"
apply auto
apply (case_tac "c = 0")
apply simp
@@ -49,7 +47,7 @@
apply simp
apply (rule_tac x = "abs c" in exI)
apply auto
- apply (subgoal_tac "c * abs(f x) <= abs c * abs (f x)")
+ apply (subgoal_tac "c * abs (f x) \<le> abs c * abs (f x)")
apply (erule_tac x = x in allE)
apply force
apply (rule mult_right_mono)
@@ -57,42 +55,40 @@
apply (rule abs_ge_zero)
done
-lemma bigo_alt_def: "O(f) =
- {h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}"
+lemma bigo_alt_def: "O(f) = {h. \<exists>c. 0 < c \<and> (\<forall>x. abs (h x) \<le> c * abs (f x))}"
by (auto simp add: bigo_def bigo_pos_const)
-lemma bigo_elt_subset [intro]: "f : O(g) ==> O(f) <= O(g)"
+lemma bigo_elt_subset [intro]: "f \<in> O(g) \<Longrightarrow> O(f) \<le> O(g)"
apply (auto simp add: bigo_alt_def)
apply (rule_tac x = "ca * c" in exI)
apply (rule conjI)
apply (rule mult_pos_pos)
- apply (assumption)+
+ apply assumption+
apply (rule allI)
apply (drule_tac x = "xa" in spec)+
- apply (subgoal_tac "ca * abs(f xa) <= ca * (c * abs(g xa))")
+ apply (subgoal_tac "ca * abs (f xa) \<le> ca * (c * abs (g xa))")
apply (erule order_trans)
apply (simp add: mult_ac)
apply (rule mult_left_mono, assumption)
apply (rule order_less_imp_le, assumption)
done
-lemma bigo_refl [intro]: "f : O(f)"
+lemma bigo_refl [intro]: "f \<in> O(f)"
apply(auto simp add: bigo_def)
apply(rule_tac x = 1 in exI)
apply simp
done
-lemma bigo_zero: "0 : O(g)"
+lemma bigo_zero: "0 \<in> O(g)"
apply (auto simp add: bigo_def func_zero)
apply (rule_tac x = 0 in exI)
apply auto
done
-lemma bigo_zero2: "O(%x.0) = {%x.0}"
- by (auto simp add: bigo_def)
+lemma bigo_zero2: "O(\<lambda>x. 0) = {\<lambda>x. 0}"
+ by (auto simp add: bigo_def)
-lemma bigo_plus_self_subset [intro]:
- "O(f) + O(f) <= O(f)"
+lemma bigo_plus_self_subset [intro]: "O(f) + O(f) \<subseteq> O(f)"
apply (auto simp add: bigo_alt_def set_plus_def)
apply (rule_tac x = "c + ca" in exI)
apply auto
@@ -102,30 +98,29 @@
apply (rule add_mono)
apply force
apply force
-done
+ done
lemma bigo_plus_idemp [simp]: "O(f) + O(f) = O(f)"
apply (rule equalityI)
apply (rule bigo_plus_self_subset)
- apply (rule set_zero_plus2)
+ apply (rule set_zero_plus2)
apply (rule bigo_zero)
done
-lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) + O(g)"
+lemma bigo_plus_subset [intro]: "O(f + g) \<subseteq> O(f) + O(g)"
apply (rule subsetI)
apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def)
apply (subst bigo_pos_const [symmetric])+
- apply (rule_tac x =
- "%n. if abs (g n) <= (abs (f n)) then x n else 0" in exI)
+ apply (rule_tac x = "\<lambda>n. if abs (g n) \<le> (abs (f n)) then x n else 0" in exI)
apply (rule conjI)
apply (rule_tac x = "c + c" in exI)
apply (clarsimp)
apply (auto)
- apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (f xa)")
+ apply (subgoal_tac "c * abs (f xa + g xa) \<le> (c + c) * abs (f xa)")
apply (erule_tac x = xa in allE)
apply (erule order_trans)
apply (simp)
- apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
+ apply (subgoal_tac "c * abs (f xa + g xa) \<le> c * (abs (f xa) + abs (g xa))")
apply (erule order_trans)
apply (simp add: ring_distribs)
apply (rule mult_left_mono)
@@ -133,16 +128,15 @@
apply (simp add: order_less_le)
apply (rule mult_nonneg_nonneg)
apply auto
- apply (rule_tac x = "%n. if (abs (f n)) < abs (g n) then x n else 0"
- in exI)
+ apply (rule_tac x = "\<lambda>n. if (abs (f n)) < abs (g n) then x n else 0" in exI)
apply (rule conjI)
apply (rule_tac x = "c + c" in exI)
apply auto
- apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (g xa)")
+ apply (subgoal_tac "c * abs (f xa + g xa) \<le> (c + c) * abs (g xa)")
apply (erule_tac x = xa in allE)
apply (erule order_trans)
- apply (simp)
- apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
+ apply simp
+ apply (subgoal_tac "c * abs (f xa + g xa) \<le> c * (abs (f xa) + abs (g xa))")
apply (erule order_trans)
apply (simp add: ring_distribs)
apply (rule mult_left_mono)
@@ -153,41 +147,39 @@
apply simp
done
-lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A + B <= O(f)"
- apply (subgoal_tac "A + B <= O(f) + O(f)")
+lemma bigo_plus_subset2 [intro]: "A \<subseteq> O(f) \<Longrightarrow> B \<subseteq> O(f) \<Longrightarrow> A + B \<subseteq> O(f)"
+ apply (subgoal_tac "A + B \<subseteq> O(f) + O(f)")
apply (erule order_trans)
apply simp
apply (auto del: subsetI simp del: bigo_plus_idemp)
done
-lemma bigo_plus_eq: "ALL x. 0 <= f x ==> ALL x. 0 <= g x ==>
- O(f + g) = O(f) + O(g)"
+lemma bigo_plus_eq: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. 0 \<le> g x \<Longrightarrow> O(f + g) = O(f) + O(g)"
apply (rule equalityI)
apply (rule bigo_plus_subset)
apply (simp add: bigo_alt_def set_plus_def func_plus)
apply clarify
apply (rule_tac x = "max c ca" in exI)
apply (rule conjI)
- apply (subgoal_tac "c <= max c ca")
+ apply (subgoal_tac "c \<le> max c ca")
apply (erule order_less_le_trans)
apply assumption
apply (rule max.cobounded1)
apply clarify
apply (drule_tac x = "xa" in spec)+
- apply (subgoal_tac "0 <= f xa + g xa")
+ apply (subgoal_tac "0 \<le> f xa + g xa")
apply (simp add: ring_distribs)
- apply (subgoal_tac "abs(a xa + b xa) <= abs(a xa) + abs(b xa)")
- apply (subgoal_tac "abs(a xa) + abs(b xa) <=
- max c ca * f xa + max c ca * g xa")
- apply (force)
+ apply (subgoal_tac "abs (a xa + b xa) \<le> abs (a xa) + abs (b xa)")
+ apply (subgoal_tac "abs (a xa) + abs (b xa) \<le> max c ca * f xa + max c ca * g xa")
+ apply force
apply (rule add_mono)
- apply (subgoal_tac "c * f xa <= max c ca * f xa")
- apply (force)
+ apply (subgoal_tac "c * f xa \<le> max c ca * f xa")
+ apply force
apply (rule mult_right_mono)
apply (rule max.cobounded1)
apply assumption
- apply (subgoal_tac "ca * g xa <= max c ca * g xa")
- apply (force)
+ apply (subgoal_tac "ca * g xa \<le> max c ca * g xa")
+ apply force
apply (rule mult_right_mono)
apply (rule max.cobounded2)
apply assumption
@@ -196,8 +188,7 @@
apply assumption+
done
-lemma bigo_bounded_alt: "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==>
- f : O(g)"
+lemma bigo_bounded_alt: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. f x \<le> c * g x \<Longrightarrow> f \<in> O(g)"
apply (auto simp add: bigo_def)
apply (rule_tac x = "abs c" in exI)
apply auto
@@ -205,14 +196,12 @@
apply (simp add: abs_mult [symmetric])
done
-lemma bigo_bounded: "ALL x. 0 <= f x ==> ALL x. f x <= g x ==>
- f : O(g)"
+lemma bigo_bounded: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. f x \<le> g x \<Longrightarrow> f \<in> O(g)"
apply (erule bigo_bounded_alt [of f 1 g])
apply simp
done
-lemma bigo_bounded2: "ALL x. lb x <= f x ==> ALL x. f x <= lb x + g x ==>
- f : lb +o O(g)"
+lemma bigo_bounded2: "\<forall>x. lb x \<le> f x \<Longrightarrow> \<forall>x. f x \<le> lb x + g x \<Longrightarrow> f \<in> lb +o O(g)"
apply (rule set_minus_imp_plus)
apply (rule bigo_bounded)
apply (auto simp add: fun_Compl_def func_plus)
@@ -222,21 +211,21 @@
apply force
done
-lemma bigo_abs: "(%x. abs(f x)) =o O(f)"
+lemma bigo_abs: "(\<lambda>x. abs (f x)) =o O(f)"
apply (unfold bigo_def)
apply auto
apply (rule_tac x = 1 in exI)
apply auto
done
-lemma bigo_abs2: "f =o O(%x. abs(f x))"
+lemma bigo_abs2: "f =o O(\<lambda>x. abs (f x))"
apply (unfold bigo_def)
apply auto
apply (rule_tac x = 1 in exI)
apply auto
done
-lemma bigo_abs3: "O(f) = O(%x. abs(f x))"
+lemma bigo_abs3: "O(f) = O(\<lambda>x. abs (f x))"
apply (rule equalityI)
apply (rule bigo_elt_subset)
apply (rule bigo_abs2)
@@ -244,65 +233,63 @@
apply (rule bigo_abs)
done
-lemma bigo_abs4: "f =o g +o O(h) ==>
- (%x. abs (f x)) =o (%x. abs (g x)) +o O(h)"
+lemma bigo_abs4: "f =o g +o O(h) \<Longrightarrow> (\<lambda>x. abs (f x)) =o (\<lambda>x. abs (g x)) +o O(h)"
apply (drule set_plus_imp_minus)
apply (rule set_minus_imp_plus)
apply (subst fun_diff_def)
proof -
- assume a: "f - g : O(h)"
- have "(%x. abs (f x) - abs (g x)) =o O(%x. abs(abs (f x) - abs (g x)))"
+ assume a: "f - g \<in> O(h)"
+ have "(\<lambda>x. abs (f x) - abs (g x)) =o O(\<lambda>x. abs (abs (f x) - abs (g x)))"
by (rule bigo_abs2)
- also have "... <= O(%x. abs (f x - g x))"
+ also have "\<dots> \<subseteq> O(\<lambda>x. abs (f x - g x))"
apply (rule bigo_elt_subset)
apply (rule bigo_bounded)
apply force
apply (rule allI)
apply (rule abs_triangle_ineq3)
done
- also have "... <= O(f - g)"
+ also have "\<dots> \<subseteq> O(f - g)"
apply (rule bigo_elt_subset)
apply (subst fun_diff_def)
apply (rule bigo_abs)
done
- also from a have "... <= O(h)"
+ also from a have "\<dots> \<subseteq> O(h)"
by (rule bigo_elt_subset)
- finally show "(%x. abs (f x) - abs (g x)) : O(h)".
+ finally show "(\<lambda>x. abs (f x) - abs (g x)) \<in> O(h)".
qed
-lemma bigo_abs5: "f =o O(g) ==> (%x. abs(f x)) =o O(g)"
+lemma bigo_abs5: "f =o O(g) \<Longrightarrow> (\<lambda>x. abs (f x)) =o O(g)"
by (unfold bigo_def, auto)
-lemma bigo_elt_subset2 [intro]: "f : g +o O(h) ==> O(f) <= O(g) + O(h)"
+lemma bigo_elt_subset2 [intro]: "f \<in> g +o O(h) \<Longrightarrow> O(f) \<subseteq> O(g) + O(h)"
proof -
- assume "f : g +o O(h)"
- also have "... <= O(g) + O(h)"
+ assume "f \<in> g +o O(h)"
+ also have "\<dots> \<subseteq> O(g) + O(h)"
by (auto del: subsetI)
- also have "... = O(%x. abs(g x)) + O(%x. abs(h x))"
+ also have "\<dots> = O(\<lambda>x. abs (g x)) + O(\<lambda>x. abs (h x))"
apply (subst bigo_abs3 [symmetric])+
apply (rule refl)
done
- also have "... = O((%x. abs(g x)) + (%x. abs(h x)))"
- by (rule bigo_plus_eq [symmetric], auto)
- finally have "f : ...".
- then have "O(f) <= ..."
+ also have "\<dots> = O((\<lambda>x. abs (g x)) + (\<lambda>x. abs (h x)))"
+ by (rule bigo_plus_eq [symmetric]) auto
+ finally have "f \<in> \<dots>" .
+ then have "O(f) \<subseteq> \<dots>"
by (elim bigo_elt_subset)
- also have "... = O(%x. abs(g x)) + O(%x. abs(h x))"
+ also have "\<dots> = O(\<lambda>x. abs (g x)) + O(\<lambda>x. abs (h x))"
by (rule bigo_plus_eq, auto)
finally show ?thesis
by (simp add: bigo_abs3 [symmetric])
qed
-lemma bigo_mult [intro]: "O(f)*O(g) <= O(f * g)"
+lemma bigo_mult [intro]: "O(f)*O(g) \<subseteq> O(f * g)"
apply (rule subsetI)
apply (subst bigo_def)
apply (auto simp add: bigo_alt_def set_times_def func_times)
apply (rule_tac x = "c * ca" in exI)
- apply(rule allI)
- apply(erule_tac x = x in allE)+
- apply(subgoal_tac "c * ca * abs(f x * g x) =
- (c * abs(f x)) * (ca * abs(g x))")
- apply(erule ssubst)
+ apply (rule allI)
+ apply (erule_tac x = x in allE)+
+ apply (subgoal_tac "c * ca * abs (f x * g x) = (c * abs (f x)) * (ca * abs (g x))")
+ apply (erule ssubst)
apply (subst abs_mult)
apply (rule mult_mono)
apply assumption+
@@ -311,24 +298,24 @@
apply (simp add: mult_ac abs_mult)
done
-lemma bigo_mult2 [intro]: "f *o O(g) <= O(f * g)"
+lemma bigo_mult2 [intro]: "f *o O(g) \<subseteq> O(f * g)"
apply (auto simp add: bigo_def elt_set_times_def func_times abs_mult)
apply (rule_tac x = c in exI)
apply auto
apply (drule_tac x = x in spec)
- apply (subgoal_tac "abs(f x) * abs(b x) <= abs(f x) * (c * abs(g x))")
+ apply (subgoal_tac "abs (f x) * abs (b x) \<le> abs (f x) * (c * abs (g x))")
apply (force simp add: mult_ac)
apply (rule mult_left_mono, assumption)
apply (rule abs_ge_zero)
done
-lemma bigo_mult3: "f : O(h) ==> g : O(j) ==> f * g : O(h * j)"
+lemma bigo_mult3: "f \<in> O(h) \<Longrightarrow> g \<in> O(j) \<Longrightarrow> f * g \<in> O(h * j)"
apply (rule subsetD)
apply (rule bigo_mult)
apply (erule set_times_intro, assumption)
done
-lemma bigo_mult4 [intro]:"f : k +o O(h) ==> g * f : (g * k) +o O(g * h)"
+lemma bigo_mult4 [intro]: "f \<in> k +o O(h) \<Longrightarrow> g * f \<in> (g * k) +o O(g * h)"
apply (drule set_plus_imp_minus)
apply (rule set_minus_imp_plus)
apply (drule bigo_mult3 [where g = g and j = g])
@@ -336,110 +323,117 @@
done
lemma bigo_mult5:
- assumes "ALL x. f x ~= 0"
- shows "O(f * g) <= (f::'a => ('b::linordered_field)) *o O(g)"
+ fixes f :: "'a \<Rightarrow> 'b::linordered_field"
+ assumes "\<forall>x. f x \<noteq> 0"
+ shows "O(f * g) \<subseteq> f *o O(g)"
proof
fix h
- assume "h : O(f * g)"
- then have "(%x. 1 / (f x)) * h : (%x. 1 / f x) *o O(f * g)"
+ assume "h \<in> O(f * g)"
+ then have "(\<lambda>x. 1 / (f x)) * h \<in> (\<lambda>x. 1 / f x) *o O(f * g)"
by auto
- also have "... <= O((%x. 1 / f x) * (f * g))"
+ also have "\<dots> \<subseteq> O((\<lambda>x. 1 / f x) * (f * g))"
by (rule bigo_mult2)
- also have "(%x. 1 / f x) * (f * g) = g"
- apply (simp add: func_times)
+ also have "(\<lambda>x. 1 / f x) * (f * g) = g"
+ apply (simp add: func_times)
apply (rule ext)
apply (simp add: assms nonzero_divide_eq_eq mult_ac)
done
- finally have "(%x. (1::'b) / f x) * h : O(g)" .
- then have "f * ((%x. (1::'b) / f x) * h) : f *o O(g)"
+ finally have "(\<lambda>x. (1::'b) / f x) * h \<in> O(g)" .
+ then have "f * ((\<lambda>x. (1::'b) / f x) * h) \<in> f *o O(g)"
by auto
- also have "f * ((%x. (1::'b) / f x) * h) = h"
- apply (simp add: func_times)
+ also have "f * ((\<lambda>x. (1::'b) / f x) * h) = h"
+ apply (simp add: func_times)
apply (rule ext)
apply (simp add: assms nonzero_divide_eq_eq mult_ac)
done
- finally show "h : f *o O(g)" .
+ finally show "h \<in> f *o O(g)" .
qed
-lemma bigo_mult6: "ALL x. f x ~= 0 ==>
- O(f * g) = (f::'a => ('b::linordered_field)) *o O(g)"
+lemma bigo_mult6:
+ fixes f :: "'a \<Rightarrow> 'b::linordered_field"
+ shows "\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) = f *o O(g)"
apply (rule equalityI)
apply (erule bigo_mult5)
apply (rule bigo_mult2)
done
-lemma bigo_mult7: "ALL x. f x ~= 0 ==>
- O(f * g) <= O(f::'a => ('b::linordered_field)) * O(g)"
+lemma bigo_mult7:
+ fixes f :: "'a \<Rightarrow> 'b::linordered_field"
+ shows "\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) \<subseteq> O(f) * O(g)"
apply (subst bigo_mult6)
apply assumption
apply (rule set_times_mono3)
apply (rule bigo_refl)
done
-lemma bigo_mult8: "ALL x. f x ~= 0 ==>
- O(f * g) = O(f::'a => ('b::linordered_field)) * O(g)"
+lemma bigo_mult8:
+ fixes f :: "'a \<Rightarrow> 'b::linordered_field"
+ shows "\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) = O(f) * O(g)"
apply (rule equalityI)
apply (erule bigo_mult7)
apply (rule bigo_mult)
done
-lemma bigo_minus [intro]: "f : O(g) ==> - f : O(g)"
+lemma bigo_minus [intro]: "f \<in> O(g) \<Longrightarrow> - f \<in> O(g)"
by (auto simp add: bigo_def fun_Compl_def)
-lemma bigo_minus2: "f : g +o O(h) ==> -f : -g +o O(h)"
+lemma bigo_minus2: "f \<in> g +o O(h) \<Longrightarrow> - f \<in> -g +o O(h)"
apply (rule set_minus_imp_plus)
apply (drule set_plus_imp_minus)
apply (drule bigo_minus)
apply simp
done
-lemma bigo_minus3: "O(-f) = O(f)"
+lemma bigo_minus3: "O(- f) = O(f)"
by (auto simp add: bigo_def fun_Compl_def)
-lemma bigo_plus_absorb_lemma1: "f : O(g) ==> f +o O(g) <= O(g)"
+lemma bigo_plus_absorb_lemma1: "f \<in> O(g) \<Longrightarrow> f +o O(g) \<subseteq> O(g)"
proof -
- assume a: "f : O(g)"
- show "f +o O(g) <= O(g)"
+ assume a: "f \<in> O(g)"
+ show "f +o O(g) \<subseteq> O(g)"
proof -
- have "f : O(f)" by auto
- then have "f +o O(g) <= O(f) + O(g)"
+ have "f \<in> O(f)" by auto
+ then have "f +o O(g) \<subseteq> O(f) + O(g)"
by (auto del: subsetI)
- also have "... <= O(g) + O(g)"
+ also have "\<dots> \<subseteq> O(g) + O(g)"
proof -
- from a have "O(f) <= O(g)" by (auto del: subsetI)
+ from a have "O(f) \<subseteq> O(g)" by (auto del: subsetI)
thus ?thesis by (auto del: subsetI)
qed
- also have "... <= O(g)" by simp
+ also have "\<dots> \<subseteq> O(g)" by simp
finally show ?thesis .
qed
qed
-lemma bigo_plus_absorb_lemma2: "f : O(g) ==> O(g) <= f +o O(g)"
+lemma bigo_plus_absorb_lemma2: "f \<in> O(g) \<Longrightarrow> O(g) \<subseteq> f +o O(g)"
proof -
- assume a: "f : O(g)"
- show "O(g) <= f +o O(g)"
+ assume a: "f \<in> O(g)"
+ show "O(g) \<subseteq> f +o O(g)"
proof -
- from a have "-f : O(g)" by auto
- then have "-f +o O(g) <= O(g)" by (elim bigo_plus_absorb_lemma1)
- then have "f +o (-f +o O(g)) <= f +o O(g)" by auto
- also have "f +o (-f +o O(g)) = O(g)"
+ from a have "- f \<in> O(g)"
+ by auto
+ then have "- f +o O(g) \<subseteq> O(g)"
+ by (elim bigo_plus_absorb_lemma1)
+ then have "f +o (- f +o O(g)) \<subseteq> f +o O(g)"
+ by auto
+ also have "f +o (- f +o O(g)) = O(g)"
by (simp add: set_plus_rearranges)
finally show ?thesis .
qed
qed
-lemma bigo_plus_absorb [simp]: "f : O(g) ==> f +o O(g) = O(g)"
+lemma bigo_plus_absorb [simp]: "f \<in> O(g) \<Longrightarrow> f +o O(g) = O(g)"
apply (rule equalityI)
apply (erule bigo_plus_absorb_lemma1)
apply (erule bigo_plus_absorb_lemma2)
done
-lemma bigo_plus_absorb2 [intro]: "f : O(g) ==> A <= O(g) ==> f +o A <= O(g)"
- apply (subgoal_tac "f +o A <= f +o O(g)")
+lemma bigo_plus_absorb2 [intro]: "f \<in> O(g) \<Longrightarrow> A \<subseteq> O(g) \<Longrightarrow> f +o A \<subseteq> O(g)"
+ apply (subgoal_tac "f +o A \<subseteq> f +o O(g)")
apply force+
done
-lemma bigo_add_commute_imp: "f : g +o O(h) ==> g : f +o O(h)"
+lemma bigo_add_commute_imp: "f \<in> g +o O(h) \<Longrightarrow> g \<in> f +o O(h)"
apply (subst set_minus_plus [symmetric])
apply (subgoal_tac "g - f = - (f - g)")
apply (erule ssubst)
@@ -449,63 +443,88 @@
apply (simp add: add_ac)
done
-lemma bigo_add_commute: "(f : g +o O(h)) = (g : f +o O(h))"
+lemma bigo_add_commute: "f \<in> g +o O(h) \<longleftrightarrow> g \<in> f +o O(h)"
apply (rule iffI)
apply (erule bigo_add_commute_imp)+
done
-lemma bigo_const1: "(%x. c) : O(%x. 1)"
+lemma bigo_const1: "(\<lambda>x. c) \<in> O(\<lambda>x. 1)"
by (auto simp add: bigo_def mult_ac)
-lemma bigo_const2 [intro]: "O(%x. c) <= O(%x. 1)"
+lemma bigo_const2 [intro]: "O(\<lambda>x. c) \<subseteq> O(\<lambda>x. 1)"
apply (rule bigo_elt_subset)
apply (rule bigo_const1)
done
-lemma bigo_const3: "(c::'a::linordered_field) ~= 0 ==> (%x. 1) : O(%x. c)"
+lemma bigo_const3:
+ fixes c :: "'a::linordered_field"
+ shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. 1) \<in> O(\<lambda>x. c)"
apply (simp add: bigo_def)
- apply (rule_tac x = "abs(inverse c)" in exI)
+ apply (rule_tac x = "abs (inverse c)" in exI)
apply (simp add: abs_mult [symmetric])
done
-lemma bigo_const4: "(c::'a::linordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)"
- by (rule bigo_elt_subset, rule bigo_const3, assumption)
+lemma bigo_const4:
+ fixes c :: "'a::linordered_field"
+ shows "c \<noteq> 0 \<Longrightarrow> O(\<lambda>x. 1) \<subseteq> O(\<lambda>x. c)"
+ apply (rule bigo_elt_subset)
+ apply (rule bigo_const3)
+ apply assumption
+ done
-lemma bigo_const [simp]: "(c::'a::linordered_field) ~= 0 ==>
- O(%x. c) = O(%x. 1)"
- by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption)
+lemma bigo_const [simp]:
+ fixes c :: "'a::linordered_field"
+ shows "c \<noteq> 0 \<Longrightarrow> O(\<lambda>x. c) = O(\<lambda>x. 1)"
+ apply (rule equalityI)
+ apply (rule bigo_const2)
+ apply (rule bigo_const4)
+ apply assumption
+ done
-lemma bigo_const_mult1: "(%x. c * f x) : O(f)"
+lemma bigo_const_mult1: "(\<lambda>x. c * f x) \<in> O(f)"
apply (simp add: bigo_def)
- apply (rule_tac x = "abs(c)" in exI)
+ apply (rule_tac x = "abs c" in exI)
apply (auto simp add: abs_mult [symmetric])
done
-lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)"
- by (rule bigo_elt_subset, rule bigo_const_mult1)
+lemma bigo_const_mult2: "O(\<lambda>x. c * f x) \<subseteq> O(f)"
+ apply (rule bigo_elt_subset)
+ apply (rule bigo_const_mult1)
+ done
-lemma bigo_const_mult3: "(c::'a::linordered_field) ~= 0 ==> f : O(%x. c * f x)"
+lemma bigo_const_mult3:
+ fixes c :: "'a::linordered_field"
+ shows "c \<noteq> 0 \<Longrightarrow> f \<in> O(\<lambda>x. c * f x)"
apply (simp add: bigo_def)
- apply (rule_tac x = "abs(inverse c)" in exI)
+ apply (rule_tac x = "abs (inverse c)" in exI)
apply (simp add: abs_mult [symmetric] mult_assoc [symmetric])
done
-lemma bigo_const_mult4: "(c::'a::linordered_field) ~= 0 ==>
- O(f) <= O(%x. c * f x)"
- by (rule bigo_elt_subset, rule bigo_const_mult3, assumption)
+lemma bigo_const_mult4:
+ fixes c :: "'a::linordered_field"
+ shows "c \<noteq> 0 \<Longrightarrow> O(f) \<subseteq> O(\<lambda>x. c * f x)"
+ apply (rule bigo_elt_subset)
+ apply (rule bigo_const_mult3)
+ apply assumption
+ done
-lemma bigo_const_mult [simp]: "(c::'a::linordered_field) ~= 0 ==>
- O(%x. c * f x) = O(f)"
- by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4)
+lemma bigo_const_mult [simp]:
+ fixes c :: "'a::linordered_field"
+ shows "c \<noteq> 0 \<Longrightarrow> O(\<lambda>x. c * f x) = O(f)"
+ apply (rule equalityI)
+ apply (rule bigo_const_mult2)
+ apply (erule bigo_const_mult4)
+ done
-lemma bigo_const_mult5 [simp]: "(c::'a::linordered_field) ~= 0 ==>
- (%x. c) *o O(f) = O(f)"
+lemma bigo_const_mult5 [simp]:
+ fixes c :: "'a::linordered_field"
+ shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c) *o O(f) = O(f)"
apply (auto del: subsetI)
apply (rule order_trans)
apply (rule bigo_mult2)
apply (simp add: func_times)
apply (auto intro!: simp add: bigo_def elt_set_times_def func_times)
- apply (rule_tac x = "%y. inverse c * x y" in exI)
+ apply (rule_tac x = "\<lambda>y. inverse c * x y" in exI)
apply (simp add: mult_assoc [symmetric] abs_mult)
apply (rule_tac x = "abs (inverse c) * ca" in exI)
apply (rule allI)
@@ -515,11 +534,11 @@
apply force
done
-lemma bigo_const_mult6 [intro]: "(%x. c) *o O(f) <= O(f)"
+lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) \<subseteq> O(f)"
apply (auto intro!: simp add: bigo_def elt_set_times_def func_times)
- apply (rule_tac x = "ca * (abs c)" in exI)
+ apply (rule_tac x = "ca * abs c" in exI)
apply (rule allI)
- apply (subgoal_tac "ca * abs(c) * abs(f x) = abs(c) * (ca * abs(f x))")
+ apply (subgoal_tac "ca * abs c * abs (f x) = abs c * (ca * abs (f x))")
apply (erule ssubst)
apply (subst abs_mult)
apply (rule mult_left_mono)
@@ -528,33 +547,34 @@
apply(simp add: mult_ac)
done
-lemma bigo_const_mult7 [intro]: "f =o O(g) ==> (%x. c * f x) =o O(g)"
+lemma bigo_const_mult7 [intro]: "f =o O(g) \<Longrightarrow> (\<lambda>x. c * f x) =o O(g)"
proof -
assume "f =o O(g)"
- then have "(%x. c) * f =o (%x. c) *o O(g)"
+ then have "(\<lambda>x. c) * f =o (\<lambda>x. c) *o O(g)"
by auto
- also have "(%x. c) * f = (%x. c * f x)"
+ also have "(\<lambda>x. c) * f = (\<lambda>x. c * f x)"
by (simp add: func_times)
- also have "(%x. c) *o O(g) <= O(g)"
+ also have "(\<lambda>x. c) *o O(g) \<subseteq> O(g)"
by (auto del: subsetI)
finally show ?thesis .
qed
-lemma bigo_compose1: "f =o O(g) ==> (%x. f(k x)) =o O(%x. g(k x))"
-by (unfold bigo_def, auto)
+lemma bigo_compose1: "f =o O(g) \<Longrightarrow> (\<lambda>x. f (k x)) =o O(\<lambda>x. g (k x))"
+ unfolding bigo_def by auto
-lemma bigo_compose2: "f =o g +o O(h) ==> (%x. f(k x)) =o (%x. g(k x)) +o
- O(%x. h(k x))"
+lemma bigo_compose2: "f =o g +o O(h) \<Longrightarrow>
+ (\<lambda>x. f (k x)) =o (\<lambda>x. g (k x)) +o O(\<lambda>x. h(k x))"
apply (simp only: set_minus_plus [symmetric] fun_Compl_def func_plus)
- apply (drule bigo_compose1) apply (simp add: fun_diff_def)
+ apply (drule bigo_compose1)
+ apply (simp add: fun_diff_def)
done
subsection {* Setsum *}
-lemma bigo_setsum_main: "ALL x. ALL y : A x. 0 <= h x y ==>
- EX c. ALL x. ALL y : A x. abs(f x y) <= c * (h x y) ==>
- (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)"
+lemma bigo_setsum_main: "\<forall>x. \<forall>y \<in> A x. 0 \<le> h x y \<Longrightarrow>
+ \<exists>c. \<forall>x. \<forall>y \<in> A x. abs (f x y) \<le> c * (h x y) \<Longrightarrow>
+ (\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)"
apply (auto simp add: bigo_def)
apply (rule_tac x = "abs c" in exI)
apply (subst abs_of_nonneg) back back
@@ -571,14 +591,14 @@
apply assumption+
apply (drule bspec)
apply assumption+
- apply (rule mult_right_mono)
+ apply (rule mult_right_mono)
apply (rule abs_ge_self)
apply force
done
-lemma bigo_setsum1: "ALL x y. 0 <= h x y ==>
- EX c. ALL x y. abs(f x y) <= c * (h x y) ==>
- (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)"
+lemma bigo_setsum1: "\<forall>x y. 0 \<le> h x y \<Longrightarrow>
+ \<exists>c. \<forall>x y. abs (f x y) \<le> c * h x y \<Longrightarrow>
+ (\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)"
apply (rule bigo_setsum_main)
apply force
apply clarsimp
@@ -586,14 +606,13 @@
apply force
done
-lemma bigo_setsum2: "ALL y. 0 <= h y ==>
- EX c. ALL y. abs(f y) <= c * (h y) ==>
- (%x. SUM y : A x. f y) =o O(%x. SUM y : A x. h y)"
- by (rule bigo_setsum1, auto)
+lemma bigo_setsum2: "\<forall>y. 0 \<le> h y \<Longrightarrow>
+ \<exists>c. \<forall>y. abs (f y) \<le> c * (h y) \<Longrightarrow>
+ (\<lambda>x. \<Sum>y \<in> A x. f y) =o O(\<lambda>x. \<Sum>y \<in> A x. h y)"
+ by (rule bigo_setsum1) auto
-lemma bigo_setsum3: "f =o O(h) ==>
- (%x. SUM y : A x. (l x y) * f(k x y)) =o
- O(%x. SUM y : A x. abs(l x y * h(k x y)))"
+lemma bigo_setsum3: "f =o O(h) \<Longrightarrow>
+ (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o O(\<lambda>x. \<Sum>y \<in> A x. abs (l x y * h (k x y)))"
apply (rule bigo_setsum1)
apply (rule allI)+
apply (rule abs_ge_zero)
@@ -608,10 +627,10 @@
apply (rule abs_ge_zero)
done
-lemma bigo_setsum4: "f =o g +o O(h) ==>
- (%x. SUM y : A x. l x y * f(k x y)) =o
- (%x. SUM y : A x. l x y * g(k x y)) +o
- O(%x. SUM y : A x. abs(l x y * h(k x y)))"
+lemma bigo_setsum4: "f =o g +o O(h) \<Longrightarrow>
+ (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o
+ (\<lambda>x. \<Sum>y \<in> A x. l x y * g (k x y)) +o
+ O(\<lambda>x. \<Sum>y \<in> A x. abs (l x y * h (k x y)))"
apply (rule set_minus_imp_plus)
apply (subst fun_diff_def)
apply (subst setsum_subtractf [symmetric])
@@ -621,12 +640,12 @@
apply (erule set_plus_imp_minus)
done
-lemma bigo_setsum5: "f =o O(h) ==> ALL x y. 0 <= l x y ==>
- ALL x. 0 <= h x ==>
- (%x. SUM y : A x. (l x y) * f(k x y)) =o
- O(%x. SUM y : A x. (l x y) * h(k x y))"
- apply (subgoal_tac "(%x. SUM y : A x. (l x y) * h(k x y)) =
- (%x. SUM y : A x. abs((l x y) * h(k x y)))")
+lemma bigo_setsum5: "f =o O(h) \<Longrightarrow> \<forall>x y. 0 \<le> l x y \<Longrightarrow>
+ \<forall>x. 0 \<le> h x \<Longrightarrow>
+ (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o
+ O(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y))"
+ apply (subgoal_tac "(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y)) =
+ (\<lambda>x. \<Sum>y \<in> A x. abs (l x y * h (k x y)))")
apply (erule ssubst)
apply (erule bigo_setsum3)
apply (rule ext)
@@ -636,11 +655,11 @@
apply auto
done
-lemma bigo_setsum6: "f =o g +o O(h) ==> ALL x y. 0 <= l x y ==>
- ALL x. 0 <= h x ==>
- (%x. SUM y : A x. (l x y) * f(k x y)) =o
- (%x. SUM y : A x. (l x y) * g(k x y)) +o
- O(%x. SUM y : A x. (l x y) * h(k x y))"
+lemma bigo_setsum6: "f =o g +o O(h) \<Longrightarrow> \<forall>x y. 0 \<le> l x y \<Longrightarrow>
+ \<forall>x. 0 \<le> h x \<Longrightarrow>
+ (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o
+ (\<lambda>x. \<Sum>y \<in> A x. l x y * g (k x y)) +o
+ O(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y))"
apply (rule set_minus_imp_plus)
apply (subst fun_diff_def)
apply (subst setsum_subtractf [symmetric])
@@ -654,33 +673,32 @@
subsection {* Misc useful stuff *}
-lemma bigo_useful_intro: "A <= O(f) ==> B <= O(f) ==>
- A + B <= O(f)"
+lemma bigo_useful_intro: "A \<subseteq> O(f) \<Longrightarrow> B \<subseteq> O(f) \<Longrightarrow> A + B \<subseteq> O(f)"
apply (subst bigo_plus_idemp [symmetric])
apply (rule set_plus_mono2)
apply assumption+
done
-lemma bigo_useful_add: "f =o O(h) ==> g =o O(h) ==> f + g =o O(h)"
+lemma bigo_useful_add: "f =o O(h) \<Longrightarrow> g =o O(h) \<Longrightarrow> f + g =o O(h)"
apply (subst bigo_plus_idemp [symmetric])
apply (rule set_plus_intro)
apply assumption+
done
-
-lemma bigo_useful_const_mult: "(c::'a::linordered_field) ~= 0 ==>
- (%x. c) * f =o O(h) ==> f =o O(h)"
+
+lemma bigo_useful_const_mult:
+ fixes c :: "'a::linordered_field"
+ shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c) * f =o O(h) \<Longrightarrow> f =o O(h)"
apply (rule subsetD)
- apply (subgoal_tac "(%x. 1 / c) *o O(h) <= O(h)")
+ apply (subgoal_tac "(\<lambda>x. 1 / c) *o O(h) \<subseteq> O(h)")
apply assumption
apply (rule bigo_const_mult6)
- apply (subgoal_tac "f = (%x. 1 / c) * ((%x. c) * f)")
+ apply (subgoal_tac "f = (\<lambda>x. 1 / c) * ((\<lambda>x. c) * f)")
apply (erule ssubst)
apply (erule set_times_intro2)
apply (simp add: func_times)
done
-lemma bigo_fix: "(%x. f ((x::nat) + 1)) =o O(%x. h(x + 1)) ==> f 0 = 0 ==>
- f =o O(h)"
+lemma bigo_fix: "(\<lambda>x::nat. f (x + 1)) =o O(\<lambda>x. h (x + 1)) \<Longrightarrow> f 0 = 0 \<Longrightarrow> f =o O(h)"
apply (simp add: bigo_alt_def)
apply auto
apply (rule_tac x = c in exI)
@@ -696,9 +714,9 @@
apply simp
done
-lemma bigo_fix2:
- "(%x. f ((x::nat) + 1)) =o (%x. g(x + 1)) +o O(%x. h(x + 1)) ==>
- f 0 = g 0 ==> f =o g +o O(h)"
+lemma bigo_fix2:
+ "(\<lambda>x. f ((x::nat) + 1)) =o (\<lambda>x. g(x + 1)) +o O(\<lambda>x. h(x + 1)) \<Longrightarrow>
+ f 0 = g 0 \<Longrightarrow> f =o g +o O(h)"
apply (rule set_minus_imp_plus)
apply (rule bigo_fix)
apply (subst fun_diff_def)
@@ -711,13 +729,10 @@
subsection {* Less than or equal to *}
-definition
- lesso :: "('a => 'b::linordered_idom) => ('a => 'b) => ('a => 'b)"
- (infixl "<o" 70) where
- "f <o g = (%x. max (f x - g x) 0)"
+definition lesso :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" (infixl "<o" 70)
+ where "f <o g = (\<lambda>x. max (f x - g x) 0)"
-lemma bigo_lesseq1: "f =o O(h) ==> ALL x. abs (g x) <= abs (f x) ==>
- g =o O(h)"
+lemma bigo_lesseq1: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) \<le> abs (f x) \<Longrightarrow> g =o O(h)"
apply (unfold bigo_def)
apply clarsimp
apply (rule_tac x = c in exI)
@@ -726,8 +741,7 @@
apply (erule spec)+
done
-lemma bigo_lesseq2: "f =o O(h) ==> ALL x. abs (g x) <= f x ==>
- g =o O(h)"
+lemma bigo_lesseq2: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) \<le> f x \<Longrightarrow> g =o O(h)"
apply (erule bigo_lesseq1)
apply (rule allI)
apply (drule_tac x = x in spec)
@@ -736,26 +750,24 @@
apply (rule abs_ge_self)
done
-lemma bigo_lesseq3: "f =o O(h) ==> ALL x. 0 <= g x ==> ALL x. g x <= f x ==>
- g =o O(h)"
+lemma bigo_lesseq3: "f =o O(h) \<Longrightarrow> \<forall>x. 0 \<le> g x \<Longrightarrow> \<forall>x. g x \<le> f x \<Longrightarrow> g =o O(h)"
apply (erule bigo_lesseq2)
apply (rule allI)
apply (subst abs_of_nonneg)
apply (erule spec)+
done
-lemma bigo_lesseq4: "f =o O(h) ==>
- ALL x. 0 <= g x ==> ALL x. g x <= abs (f x) ==>
- g =o O(h)"
+lemma bigo_lesseq4: "f =o O(h) \<Longrightarrow>
+ \<forall>x. 0 \<le> g x \<Longrightarrow> \<forall>x. g x \<le> abs (f x) \<Longrightarrow> g =o O(h)"
apply (erule bigo_lesseq1)
apply (rule allI)
apply (subst abs_of_nonneg)
apply (erule spec)+
done
-lemma bigo_lesso1: "ALL x. f x <= g x ==> f <o g =o O(h)"
+lemma bigo_lesso1: "\<forall>x. f x \<le> g x \<Longrightarrow> f <o g =o O(h)"
apply (unfold lesso_def)
- apply (subgoal_tac "(%x. max (f x - g x) 0) = 0")
+ apply (subgoal_tac "(\<lambda>x. max (f x - g x) 0) = 0")
apply (erule ssubst)
apply (rule bigo_zero)
apply (unfold func_zero)
@@ -763,9 +775,8 @@
apply (simp split: split_max)
done
-lemma bigo_lesso2: "f =o g +o O(h) ==>
- ALL x. 0 <= k x ==> ALL x. k x <= f x ==>
- k <o g =o O(h)"
+lemma bigo_lesso2: "f =o g +o O(h) \<Longrightarrow>
+ \<forall>x. 0 \<le> k x \<Longrightarrow> \<forall>x. k x \<le> f x \<Longrightarrow> k <o g =o O(h)"
apply (unfold lesso_def)
apply (rule bigo_lesseq4)
apply (erule set_plus_imp_minus)
@@ -773,7 +784,7 @@
apply (rule max.cobounded2)
apply (rule allI)
apply (subst fun_diff_def)
- apply (case_tac "0 <= k x - g x")
+ apply (case_tac "0 \<le> k x - g x")
apply simp
apply (subst abs_of_nonneg)
apply (drule_tac x = x in spec) back
@@ -781,15 +792,14 @@
apply (subst diff_conv_add_uminus)+
apply (rule add_right_mono)
apply (erule spec)
- apply (rule order_trans)
+ apply (rule order_trans)
prefer 2
apply (rule abs_ge_zero)
apply (simp add: algebra_simps)
done
-lemma bigo_lesso3: "f =o g +o O(h) ==>
- ALL x. 0 <= k x ==> ALL x. g x <= k x ==>
- f <o k =o O(h)"
+lemma bigo_lesso3: "f =o g +o O(h) \<Longrightarrow>
+ \<forall>x. 0 \<le> k x \<Longrightarrow> \<forall>x. g x \<le> k x \<Longrightarrow> f <o k =o O(h)"
apply (unfold lesso_def)
apply (rule bigo_lesseq4)
apply (erule set_plus_imp_minus)
@@ -797,7 +807,7 @@
apply (rule max.cobounded2)
apply (rule allI)
apply (subst fun_diff_def)
- apply (case_tac "0 <= f x - k x")
+ apply (case_tac "0 \<le> f x - k x")
apply simp
apply (subst abs_of_nonneg)
apply (drule_tac x = x in spec) back
@@ -806,14 +816,15 @@
apply (rule add_left_mono)
apply (rule le_imp_neg_le)
apply (erule spec)
- apply (rule order_trans)
+ apply (rule order_trans)
prefer 2
apply (rule abs_ge_zero)
apply (simp add: algebra_simps)
done
-lemma bigo_lesso4: "f <o g =o O(k::'a=>'b::linordered_field) ==>
- g =o h +o O(k) ==> f <o h =o O(k)"
+lemma bigo_lesso4:
+ fixes k :: "'a \<Rightarrow> 'b::linordered_field"
+ shows "f <o g =o O(k) \<Longrightarrow> g =o h +o O(k) \<Longrightarrow> f <o h =o O(k)"
apply (unfold lesso_def)
apply (drule set_plus_imp_minus)
apply (drule bigo_abs5) back
@@ -822,25 +833,22 @@
apply assumption
apply (erule bigo_lesseq2) back
apply (rule allI)
- apply (auto simp add: func_plus fun_diff_def algebra_simps
- split: split_max abs_split)
+ apply (auto simp add: func_plus fun_diff_def algebra_simps split: split_max abs_split)
done
-lemma bigo_lesso5: "f <o g =o O(h) ==>
- EX C. ALL x. f x <= g x + C * abs(h x)"
+lemma bigo_lesso5: "f <o g =o O(h) \<Longrightarrow> \<exists>C. \<forall>x. f x \<le> g x + C * abs (h x)"
apply (simp only: lesso_def bigo_alt_def)
apply clarsimp
apply (rule_tac x = c in exI)
apply (rule allI)
apply (drule_tac x = x in spec)
- apply (subgoal_tac "abs(max (f x - g x) 0) = max (f x - g x) 0")
- apply (clarsimp simp add: algebra_simps)
+ apply (subgoal_tac "abs (max (f x - g x) 0) = max (f x - g x) 0")
+ apply (clarsimp simp add: algebra_simps)
apply (rule abs_of_nonneg)
apply (rule max.cobounded2)
done
-lemma lesso_add: "f <o g =o O(h) ==>
- k <o l =o O(h) ==> (f + k) <o (g + l) =o O(h)"
+lemma lesso_add: "f <o g =o O(h) \<Longrightarrow> k <o l =o O(h) \<Longrightarrow> (f + k) <o (g + l) =o O(h)"
apply (unfold lesso_def)
apply (rule bigo_lesseq3)
apply (erule bigo_useful_add)
@@ -849,7 +857,7 @@
apply (auto split: split_max simp add: func_plus)
done
-lemma bigo_LIMSEQ1: "f =o O(g) ==> g ----> 0 ==> f ----> (0::real)"
+lemma bigo_LIMSEQ1: "f =o O(g) \<Longrightarrow> g ----> 0 \<Longrightarrow> f ----> (0::real)"
apply (simp add: LIMSEQ_iff bigo_alt_def)
apply clarify
apply (drule_tac x = "r / c" in spec)
@@ -866,21 +874,20 @@
apply (rule order_le_less_trans)
apply assumption
apply (rule order_less_le_trans)
- apply (subgoal_tac "c * abs(g n) < c * (r / c)")
+ apply (subgoal_tac "c * abs (g n) < c * (r / c)")
apply assumption
apply (erule mult_strict_left_mono)
apply assumption
apply simp
-done
+ done
-lemma bigo_LIMSEQ2: "f =o g +o O(h) ==> h ----> 0 ==> f ----> a
- ==> g ----> (a::real)"
+lemma bigo_LIMSEQ2: "f =o g +o O(h) \<Longrightarrow> h ----> 0 \<Longrightarrow> f ----> a \<Longrightarrow> g ----> (a::real)"
apply (drule set_plus_imp_minus)
apply (drule bigo_LIMSEQ1)
apply assumption
apply (simp only: fun_diff_def)
apply (erule LIMSEQ_diff_approach_zero2)
apply assumption
-done
+ done
end
--- a/src/HOL/ex/Cartouche_Examples.thy Sat Mar 01 20:40:31 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy Sat Mar 01 23:48:55 2014 +0100
@@ -114,13 +114,13 @@
setup -- "document antiquotation"
{*
Thy_Output.antiquotation @{binding ML_cartouche}
- (Scan.lift Args.cartouche_source_position) (fn {context, ...} => fn (txt, pos) =>
+ (Scan.lift Args.cartouche_source_position) (fn {context, ...} => fn source =>
let
val toks =
ML_Lex.read Position.none "fn _ => (" @
- ML_Lex.read pos txt @
+ ML_Lex.read_source source @
ML_Lex.read Position.none ");";
- val _ = ML_Context.eval_in (SOME context) false pos toks;
+ val _ = ML_Context.eval_in (SOME context) false (#pos source) toks;
in "" end);
*}
@@ -177,19 +177,19 @@
structure ML_Tactic:
sig
val set: (Proof.context -> tactic) -> Proof.context -> Proof.context
- val ml_tactic: string * Position.T -> Proof.context -> tactic
+ val ml_tactic: Symbol_Pos.source -> Proof.context -> tactic
end =
struct
structure Data = Proof_Data(type T = Proof.context -> tactic fun init _ = K no_tac);
val set = Data.put;
- fun ml_tactic (txt, pos) ctxt =
+ fun ml_tactic source ctxt =
let
val ctxt' = ctxt |> Context.proof_map
- (ML_Context.expression pos
+ (ML_Context.expression (#pos source)
"fun tactic (ctxt : Proof.context) : tactic"
- "Context.map_proof (ML_Tactic.set tactic)" (ML_Lex.read pos txt));
+ "Context.map_proof (ML_Tactic.set tactic)" (ML_Lex.read_source source));
in Data.get ctxt' ctxt end;
end;
*}
--- a/src/Pure/General/symbol_pos.ML Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Pure/General/symbol_pos.ML Sat Mar 01 23:48:55 2014 +0100
@@ -40,6 +40,8 @@
val implode: T list -> text
val implode_range: Position.T -> Position.T -> T list -> text * Position.range
val explode: text * Position.T -> T list
+ type source = {delimited: bool, text: text, pos: Position.T}
+ val source_content: source -> string * Position.T
val scan_ident: T list -> T list * T list
val is_identifier: string -> bool
end;
@@ -255,6 +257,14 @@
in fold (fn (s, p) => if s = Symbol.DEL then I else cons (s, p)) res [] end;
+(* full source information *)
+
+type source = {delimited: bool, text: text, pos: Position.T};
+
+fun source_content {delimited = _, text, pos} =
+ let val syms = explode (text, pos) in (content syms, pos) end;
+
+
(* identifiers *)
local
--- a/src/Pure/Isar/args.ML Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Pure/Isar/args.ML Sat Mar 01 23:48:55 2014 +0100
@@ -30,9 +30,9 @@
val mode: string -> bool parser
val maybe: 'a parser -> 'a option parser
val cartouche_inner_syntax: string parser
- val cartouche_source_position: (Symbol_Pos.text * Position.T) parser
+ val cartouche_source_position: Symbol_Pos.source parser
val name_inner_syntax: string parser
- val name_source_position: (Symbol_Pos.text * Position.T) parser
+ val name_source_position: Symbol_Pos.source parser
val name: string parser
val binding: binding parser
val alt_name: string parser
--- a/src/Pure/Isar/attrib.ML Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Pure/Isar/attrib.ML Sat Mar 01 23:48:55 2014 +0100
@@ -35,8 +35,7 @@
Context.generic -> (string * thm list) list * Context.generic
val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
- val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
- theory -> theory
+ val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory
val internal: (morphism -> attribute) -> src
val add_del: attribute -> attribute -> attribute context_parser
val thm_sel: Facts.interval list parser
@@ -185,12 +184,12 @@
add_attribute name
(fn src => fn (ctxt, th) => let val (a, ctxt') = syntax scan src ctxt in a (ctxt', th) end);
-fun attribute_setup name (txt, pos) cmt =
- Context.theory_map (ML_Context.expression pos
+fun attribute_setup name source cmt =
+ Context.theory_map (ML_Context.expression (#pos source)
"val (name, scan, comment): binding * attribute context_parser * string"
"Context.map_theory (Attrib.setup name scan comment)"
(ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
- ML_Lex.read pos txt @
+ ML_Lex.read_source source @
ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
--- a/src/Pure/Isar/isar_cmd.ML Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Sat Mar 01 23:48:55 2014 +0100
@@ -6,20 +6,20 @@
signature ISAR_CMD =
sig
- val global_setup: Symbol_Pos.text * Position.T -> theory -> theory
- val local_setup: Symbol_Pos.text * Position.T -> Proof.context -> Proof.context
- val parse_ast_translation: Symbol_Pos.text * Position.T -> theory -> theory
- val parse_translation: Symbol_Pos.text * Position.T -> theory -> theory
- val print_translation: Symbol_Pos.text * Position.T -> theory -> theory
- val typed_print_translation: Symbol_Pos.text * Position.T -> theory -> theory
- val print_ast_translation: Symbol_Pos.text * Position.T -> theory -> theory
+ val global_setup: Symbol_Pos.source -> theory -> theory
+ val local_setup: Symbol_Pos.source -> Proof.context -> Proof.context
+ val parse_ast_translation: Symbol_Pos.source -> theory -> theory
+ val parse_translation: Symbol_Pos.source -> theory -> theory
+ val print_translation: Symbol_Pos.source -> theory -> theory
+ val typed_print_translation: Symbol_Pos.source -> theory -> theory
+ val print_ast_translation: Symbol_Pos.source -> theory -> theory
val translations: (xstring * string) Syntax.trrule list -> theory -> theory
val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
- val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
+ val oracle: bstring * Position.T -> Symbol_Pos.source -> theory -> theory
val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
val declaration: {syntax: bool, pervasive: bool} ->
- Symbol_Pos.text * Position.T -> local_theory -> local_theory
- val simproc_setup: string * Position.T -> string list -> Symbol_Pos.text * Position.T ->
+ Symbol_Pos.source -> local_theory -> local_theory
+ val simproc_setup: string * Position.T -> string list -> Symbol_Pos.source ->
string list -> local_theory -> local_theory
val hide_class: bool -> xstring list -> theory -> theory
val hide_type: bool -> xstring list -> theory -> theory
@@ -36,7 +36,7 @@
val immediate_proof: Toplevel.transition -> Toplevel.transition
val done_proof: Toplevel.transition -> Toplevel.transition
val skip_proof: Toplevel.transition -> Toplevel.transition
- val ml_diag: bool -> Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
+ val ml_diag: bool -> Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
val diag_state: Proof.context -> Toplevel.state
val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
val print_theorems: bool -> Toplevel.transition -> Toplevel.transition
@@ -56,10 +56,10 @@
val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
val print_type: (string list * (string * string option)) ->
Toplevel.transition -> Toplevel.transition
- val header_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
- val local_theory_markup: (xstring * Position.T) option * (Symbol_Pos.text * Position.T) ->
+ val header_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
+ val local_theory_markup: (xstring * Position.T) option * (Symbol_Pos.source) ->
Toplevel.transition -> Toplevel.transition
- val proof_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
+ val proof_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
end;
structure Isar_Cmd: ISAR_CMD =
@@ -70,50 +70,50 @@
(* generic setup *)
-fun global_setup (txt, pos) =
- ML_Lex.read pos txt
- |> ML_Context.expression pos "val setup: theory -> theory" "Context.map_theory setup"
+fun global_setup source =
+ ML_Lex.read_source source
+ |> ML_Context.expression (#pos source) "val setup: theory -> theory" "Context.map_theory setup"
|> Context.theory_map;
-fun local_setup (txt, pos) =
- ML_Lex.read pos txt
- |> ML_Context.expression pos "val setup: local_theory -> local_theory" "Context.map_proof setup"
+fun local_setup source =
+ ML_Lex.read_source source
+ |> ML_Context.expression (#pos source) "val setup: local_theory -> local_theory" "Context.map_proof setup"
|> Context.proof_map;
(* translation functions *)
-fun parse_ast_translation (txt, pos) =
- ML_Lex.read pos txt
- |> ML_Context.expression pos
+fun parse_ast_translation source =
+ ML_Lex.read_source source
+ |> ML_Context.expression (#pos source)
"val parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
"Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
|> Context.theory_map;
-fun parse_translation (txt, pos) =
- ML_Lex.read pos txt
- |> ML_Context.expression pos
+fun parse_translation source =
+ ML_Lex.read_source source
+ |> ML_Context.expression (#pos source)
"val parse_translation: (string * (Proof.context -> term list -> term)) list"
"Context.map_theory (Sign.parse_translation parse_translation)"
|> Context.theory_map;
-fun print_translation (txt, pos) =
- ML_Lex.read pos txt
- |> ML_Context.expression pos
+fun print_translation source =
+ ML_Lex.read_source source
+ |> ML_Context.expression (#pos source)
"val print_translation: (string * (Proof.context -> term list -> term)) list"
"Context.map_theory (Sign.print_translation print_translation)"
|> Context.theory_map;
-fun typed_print_translation (txt, pos) =
- ML_Lex.read pos txt
- |> ML_Context.expression pos
+fun typed_print_translation source =
+ ML_Lex.read_source source
+ |> ML_Context.expression (#pos source)
"val typed_print_translation: (string * (Proof.context -> typ -> term list -> term)) list"
"Context.map_theory (Sign.typed_print_translation typed_print_translation)"
|> Context.theory_map;
-fun print_ast_translation (txt, pos) =
- ML_Lex.read pos txt
- |> ML_Context.expression pos
+fun print_ast_translation source =
+ ML_Lex.read_source source
+ |> ML_Context.expression (#pos source)
"val print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
"Context.map_theory (Sign.print_ast_translation print_ast_translation)"
|> Context.theory_map;
@@ -135,18 +135,19 @@
(* oracles *)
-fun oracle (name, pos) (body_txt, body_pos) =
+fun oracle (name, pos) source =
let
- val body = ML_Lex.read body_pos body_txt;
+ val body = ML_Lex.read_source source;
val ants =
ML_Lex.read Position.none
("local\n\
\ val binding = " ^ ML_Syntax.make_binding (name, pos) ^ ";\n\
\ val body = ") @ body @ ML_Lex.read Position.none (";\n\
\in\n\
- \ val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\
+ \ val " ^ name ^
+ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\
\end;\n");
- in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false body_pos ants)) end;
+ in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false (#pos source) ants)) end;
(* old-style defs *)
@@ -161,9 +162,9 @@
(* declarations *)
-fun declaration {syntax, pervasive} (txt, pos) =
- ML_Lex.read pos txt
- |> ML_Context.expression pos
+fun declaration {syntax, pervasive} source =
+ ML_Lex.read_source source
+ |> ML_Context.expression (#pos source)
"val declaration: Morphism.declaration"
("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
\pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
@@ -172,9 +173,9 @@
(* simprocs *)
-fun simproc_setup name lhss (txt, pos) identifier =
- ML_Lex.read pos txt
- |> ML_Context.expression pos
+fun simproc_setup name lhss source identifier =
+ ML_Lex.read_source source
+ |> ML_Context.expression (#pos source)
"val proc: Morphism.morphism -> Proof.context -> cterm -> thm option"
("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \
\lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
@@ -253,11 +254,11 @@
fun init _ = Toplevel.toplevel;
);
-fun ml_diag verbose (txt, pos) = Toplevel.keep (fn state =>
+fun ml_diag verbose source = Toplevel.keep (fn state =>
let val opt_ctxt =
try Toplevel.generic_theory_of state
|> Option.map (Context.proof_of #> Diag_State.put state)
- in ML_Context.eval_text_in opt_ctxt verbose pos txt end);
+ in ML_Context.eval_source_in opt_ctxt verbose source end);
val diag_state = Diag_State.get;
--- a/src/Pure/Isar/isar_syn.ML Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML Sat Mar 01 23:48:55 2014 +0100
@@ -248,16 +248,17 @@
val _ =
Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory"
- (Parse.ML_source >> (fn (txt, pos) =>
+ (Parse.ML_source >> (fn source =>
Toplevel.generic_theory
- (ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #>
+ (ML_Context.exec (fn () => ML_Context.eval_source true source) #>
Local_Theory.propagate_ml_env)));
val _ =
Outer_Syntax.command @{command_spec "ML_prf"} "ML text within proof"
- (Parse.ML_source >> (fn (txt, pos) =>
+ (Parse.ML_source >> (fn source =>
Toplevel.proof (Proof.map_context (Context.proof_map
- (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> Proof.propagate_ml_env)));
+ (ML_Context.exec (fn () => ML_Context.eval_source true source))) #>
+ Proof.propagate_ml_env)));
val _ =
Outer_Syntax.command @{command_spec "ML_val"} "diagnostic ML text"
--- a/src/Pure/Isar/method.ML Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Pure/Isar/method.ML Sat Mar 01 23:48:55 2014 +0100
@@ -42,8 +42,8 @@
val drule: Proof.context -> int -> thm list -> method
val frule: Proof.context -> int -> thm list -> method
val set_tactic: (thm list -> tactic) -> Proof.context -> Proof.context
- val tactic: string * Position.T -> Proof.context -> method
- val raw_tactic: string * Position.T -> Proof.context -> method
+ val tactic: Symbol_Pos.source -> Proof.context -> method
+ val raw_tactic: Symbol_Pos.source -> Proof.context -> method
type src = Args.src
type combinator_info
val no_combinator_info: combinator_info
@@ -68,8 +68,7 @@
val check_source: Proof.context -> src -> src
val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
- val method_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
- theory -> theory
+ val method_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory
type modifier = (Proof.context -> Proof.context) * attribute
val section: modifier parser list -> thm list context_parser
val sections: modifier parser list -> thm list list context_parser
@@ -266,16 +265,16 @@
val set_tactic = ML_Tactic.put;
-fun ml_tactic (txt, pos) ctxt =
+fun ml_tactic source ctxt =
let
val ctxt' = ctxt |> Context.proof_map
- (ML_Context.expression pos
+ (ML_Context.expression (#pos source)
"fun tactic (facts: thm list) : tactic"
- "Context.map_proof (Method.set_tactic tactic)" (ML_Lex.read pos txt));
+ "Context.map_proof (Method.set_tactic tactic)" (ML_Lex.read_source source));
in Context.setmp_thread_data (SOME (Context.Proof ctxt)) (ML_Tactic.get ctxt') end;
-fun tactic txt ctxt = METHOD (ml_tactic txt ctxt);
-fun raw_tactic txt ctxt = RAW_METHOD (ml_tactic txt ctxt);
+fun tactic source ctxt = METHOD (ml_tactic source ctxt);
+fun raw_tactic source ctxt = RAW_METHOD (ml_tactic source ctxt);
@@ -366,12 +365,12 @@
add_method name
(fn src => fn ctxt => let val (m, ctxt') = syntax scan src ctxt in m ctxt' end);
-fun method_setup name (txt, pos) cmt =
- Context.theory_map (ML_Context.expression pos
+fun method_setup name source cmt =
+ Context.theory_map (ML_Context.expression (#pos source)
"val (name, scan, comment): binding * (Proof.context -> Proof.method) context_parser * string"
"Context.map_theory (Method.setup name scan comment)"
(ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
- ML_Lex.read pos txt @
+ ML_Lex.read_source source @
ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
--- a/src/Pure/Isar/parse.ML Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Pure/Isar/parse.ML Sat Mar 01 23:48:55 2014 +0100
@@ -16,7 +16,7 @@
val triple_swap: ('a * 'b) * 'c -> ('a * 'c) * 'b
val not_eof: Token.T parser
val position: 'a parser -> ('a * Position.T) parser
- val source_position: 'a parser -> (Symbol_Pos.text * Position.T) parser
+ val source_position: 'a parser -> Symbol_Pos.source parser
val inner_syntax: 'a parser -> string parser
val command: string parser
val keyword: string parser
@@ -93,8 +93,8 @@
val simple_fixes: (binding * string option) list parser
val fixes: (binding * string option * mixfix) list parser
val for_fixes: (binding * string option * mixfix) list parser
- val ML_source: (Symbol_Pos.text * Position.T) parser
- val document_source: (Symbol_Pos.text * Position.T) parser
+ val ML_source: Symbol_Pos.source parser
+ val document_source: Symbol_Pos.source parser
val term_group: string parser
val prop_group: string parser
val term: string parser
--- a/src/Pure/Isar/proof_context.ML Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML Sat Mar 01 23:48:55 2014 +0100
@@ -377,8 +377,8 @@
fun read_class ctxt text =
let
val tsig = tsig_of ctxt;
- val (syms, pos) = Syntax.read_token text;
- val c = Type.cert_class tsig (Type.intern_class tsig (Symbol_Pos.content syms))
+ val (s, pos) = Symbol_Pos.source_content (Syntax.read_token text);
+ val c = Type.cert_class tsig (Type.intern_class tsig s)
handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
val _ = Context_Position.report ctxt pos (Name_Space.markup (Type.class_space tsig) c);
in c end;
@@ -439,8 +439,6 @@
local
-val token_content = Syntax.read_token #>> Symbol_Pos.content;
-
fun prep_const_proper ctxt strict (c, pos) =
let
fun err msg = error (msg ^ Position.here pos);
@@ -461,7 +459,7 @@
fun read_type_name ctxt strict text =
let
val tsig = tsig_of ctxt;
- val (c, pos) = token_content text;
+ val (c, pos) = Symbol_Pos.source_content (Syntax.read_token text);
in
if Lexicon.is_tid c then
(Context_Position.report ctxt pos Markup.tfree;
@@ -486,11 +484,12 @@
| T => error ("Not a type constructor: " ^ Syntax.string_of_typ ctxt T));
-fun read_const_proper ctxt strict = prep_const_proper ctxt strict o token_content;
+fun read_const_proper ctxt strict =
+ prep_const_proper ctxt strict o Symbol_Pos.source_content o Syntax.read_token;
fun read_const ctxt strict ty text =
let
- val (c, pos) = token_content text;
+ val (c, pos) = Symbol_Pos.source_content (Syntax.read_token text);
val _ = no_skolem false c;
in
(case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of
--- a/src/Pure/Isar/token.ML Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Pure/Isar/token.ML Sat Mar 01 23:48:55 2014 +0100
@@ -40,7 +40,7 @@
val is_blank: T -> bool
val is_newline: T -> bool
val inner_syntax_of: T -> string
- val source_position_of: T -> Symbol_Pos.text * Position.T
+ val source_position_of: T -> Symbol_Pos.source
val content_of: T -> string
val markup: T -> Markup.T * string
val unparse: T -> string
@@ -127,6 +127,8 @@
| Sync => "sync marker"
| EOF => "end-of-input";
+val delimited_kind = member (op =) [String, AltString, Verbatim, Cartouche, Comment];
+
(* position *)
@@ -206,11 +208,16 @@
(* token content *)
-fun inner_syntax_of (Token ((source, (pos, _)), (_, x), _)) =
+fun inner_syntax_of (Token ((source, (pos, _)), (kind, x), _)) =
if YXML.detect x then x
- else YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source]));
+ else
+ let
+ val delimited = delimited_kind kind;
+ val tree = XML.Elem (Markup.token delimited (Position.properties_of pos), [XML.Text source]);
+ in YXML.string_of tree end;
-fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos);
+fun source_position_of (Token ((source, (pos, _)), (kind, _), _)) =
+ {delimited = delimited_kind kind, text = source, pos = pos};
fun content_of (Token (_, (_, x), _)) = x;
--- a/src/Pure/ML/ml_context.ML Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Pure/ML/ml_context.ML Sat Mar 01 23:48:55 2014 +0100
@@ -31,10 +31,10 @@
val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
val eval: bool -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
- val eval_text: bool -> Position.T -> Symbol_Pos.text -> unit
+ val eval_source: bool -> Symbol_Pos.source -> unit
val eval_in: Proof.context option -> bool -> Position.T ->
ML_Lex.token Antiquote.antiquote list -> unit
- val eval_text_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit
+ val eval_source_in: Proof.context option -> bool -> Symbol_Pos.source -> unit
val expression: Position.T -> string -> string -> ML_Lex.token Antiquote.antiquote list ->
Context.generic -> Context.generic
end
@@ -208,13 +208,14 @@
(* derived versions *)
-fun eval_text verbose pos txt = eval verbose pos (ML_Lex.read pos txt);
+fun eval_source verbose source =
+ eval verbose (#pos source) (ML_Lex.read_source source);
fun eval_in ctxt verbose pos ants =
Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval verbose pos ants) ();
-fun eval_text_in ctxt verbose pos txt =
- Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval_text verbose pos txt) ();
+fun eval_source_in ctxt verbose source =
+ Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval_source verbose source) ();
fun expression pos bind body ants =
exec (fn () => eval false pos
--- a/src/Pure/ML/ml_lex.ML Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML Sat Mar 01 23:48:55 2014 +0100
@@ -26,6 +26,7 @@
Source.source) Source.source
val tokenize: string -> token list
val read: Position.T -> Symbol_Pos.text -> token Antiquote.antiquote list
+ val read_source: Symbol_Pos.source -> token Antiquote.antiquote list
end;
structure ML_Lex: ML_LEX =
@@ -298,10 +299,9 @@
val tokenize = Source.of_string #> Symbol.source #> source #> Source.exhaust;
-fun read pos txt =
+fun read pos text =
let
- val _ = Position.report pos Markup.language_ML;
- val syms = Symbol_Pos.explode (txt, pos);
+ val syms = Symbol_Pos.explode (text, pos);
val termination =
if null syms then []
else
@@ -318,6 +318,9 @@
|> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())));
in input @ termination end;
+fun read_source {delimited, text, pos} =
+ (Position.report pos (Markup.language_ML delimited); read pos text);
+
end;
end;
--- a/src/Pure/PIDE/command.scala Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Pure/PIDE/command.scala Sat Mar 01 23:48:55 2014 +0100
@@ -156,14 +156,11 @@
if id == command.id || id == alt_id =>
command.chunks.get(file_name) match {
case Some(chunk) =>
- chunk.decode(raw_range).try_restrict(chunk.range) match {
+ chunk.incorporate(raw_range) match {
case Some(range) =>
- if (!range.is_singularity) {
- val props = Position.purge(atts)
- val info = Text.Info(range, XML.Elem(Markup(name, props), args))
- state.add_markup(false, file_name, info)
- }
- else state
+ val props = Position.purge(atts)
+ val info = Text.Info(range, XML.Elem(Markup(name, props), args))
+ state.add_markup(false, file_name, info)
case None => bad(); state
}
case None => bad(); state
@@ -219,7 +216,17 @@
def file_name: String
def length: Int
def range: Text.Range
- def decode(r: Text.Range): Text.Range
+ def decode(raw_range: Text.Range): Text.Range
+
+ def incorporate(raw_range: Text.Range): Option[Text.Range] =
+ {
+ def inc(r: Text.Range): Option[Text.Range] =
+ range.try_restrict(decode(r)) match {
+ case Some(r1) if !r1.is_singularity => Some(r1)
+ case _ => None
+ }
+ inc(raw_range) orElse inc(raw_range - 1)
+ }
}
class File(val file_name: String, text: CharSequence) extends Chunk
@@ -227,7 +234,7 @@
val length = text.length
val range = Text.Range(0, length)
private val symbol_index = Symbol.Index(text)
- def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
+ def decode(raw_range: Text.Range): Text.Range = symbol_index.decode(raw_range)
override def toString: String = "Command.File(" + file_name + ")"
}
@@ -367,8 +374,8 @@
def source(range: Text.Range): String = source.substring(range.start, range.stop)
private lazy val symbol_index = Symbol.Index(source)
- def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
- def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
+ def decode(raw_offset: Text.Offset): Text.Offset = symbol_index.decode(raw_offset)
+ def decode(raw_range: Text.Range): Text.Range = symbol_index.decode(raw_range)
/* accumulated results */
--- a/src/Pure/PIDE/document.scala Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Pure/PIDE/document.scala Sat Mar 01 23:48:55 2014 +0100
@@ -376,8 +376,32 @@
}
+ /* markup elements */
- /** global state -- document structure, execution process, editing history **/
+ object Elements
+ {
+ def apply(elems: Set[String]): Elements = new Elements(elems)
+ def apply(elems: String*): Elements = apply(Set(elems: _*))
+ val empty: Elements = apply()
+ val full: Elements = new Full_Elements
+ }
+
+ sealed class Elements private[Document](private val rep: Set[String])
+ {
+ def apply(elem: String): Boolean = rep.contains(elem)
+ def + (elem: String): Elements = new Elements(rep + elem)
+ def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
+ override def toString: String = rep.mkString("Elements(", ",", ")")
+ }
+
+ private class Full_Elements extends Elements(Set.empty)
+ {
+ override def apply(elem: String): Boolean = true
+ override def toString: String = "Full_Elements()"
+ }
+
+
+ /* snapshot */
object Snapshot
{
@@ -403,17 +427,21 @@
def cumulate[A](
range: Text.Range,
info: A,
- elements: String => Boolean,
+ elements: Elements,
result: Command.State => (A, Text.Markup) => Option[A],
status: Boolean = false): List[Text.Info[A]]
def select[A](
range: Text.Range,
- elements: String => Boolean,
+ elements: Elements,
result: Command.State => Text.Markup => Option[A],
status: Boolean = false): List[Text.Info[A]]
}
+
+
+ /** global state -- document structure, execution process, editing history **/
+
type Assign_Update =
List[(Document_ID.Command, List[Document_ID.Exec])] // update of exec state assignment
@@ -672,7 +700,7 @@
def cumulate[A](
range: Text.Range,
info: A,
- elements: String => Boolean,
+ elements: Elements,
result: Command.State => (A, Text.Markup) => Option[A],
status: Boolean = false): List[Text.Info[A]] =
{
@@ -708,7 +736,7 @@
def select[A](
range: Text.Range,
- elements: String => Boolean,
+ elements: Elements,
result: Command.State => Text.Markup => Option[A],
status: Boolean = false): List[Text.Info[A]] =
{
--- a/src/Pure/PIDE/markup.ML Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Pure/PIDE/markup.ML Sat Mar 01 23:48:55 2014 +0100
@@ -20,18 +20,21 @@
val name: string -> T -> T
val kindN: string
val instanceN: string
+ val languageN: string
val symbolsN: string
- val languageN: string
- val language: {name: string, symbols: bool, antiquotes: bool} -> T
+ val delimitedN: string
+ val is_delimited: Properties.T -> bool
+ val language: {name: string, symbols: bool, antiquotes: bool, delimited: bool} -> T
+ val language': {name: string, symbols: bool, antiquotes: bool} -> bool -> T
val language_method: 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_sort: bool -> T
+ val language_type: bool -> T
+ val language_term: bool -> T
+ val language_prop: bool -> T
+ val language_ML: bool -> T
+ val language_document: bool -> T
val language_antiquotation: T
- val language_text: T
+ val language_text: bool -> T
val language_rail: T
val bindingN: string val binding: T
val entityN: string val entity: string -> string -> T
@@ -106,7 +109,7 @@
val cartoucheN: string val cartouche: T
val commentN: string val comment: T
val controlN: string val control: T
- val tokenN: string val token: Properties.T -> T
+ val tokenN: string val token: bool -> Properties.T -> T
val keyword1N: string val keyword1: T
val keyword2N: string val keyword2: T
val keyword3N: string val keyword3: T
@@ -251,24 +254,36 @@
(* embedded languages *)
+val languageN = "language";
val symbolsN = "symbols";
val antiquotesN = "antiquotes";
-val languageN = "language";
+val delimitedN = "delimited"
+
+fun is_delimited props =
+ Properties.get props delimitedN = SOME "true";
-fun language {name, symbols, antiquotes} =
+fun language {name, symbols, antiquotes, delimited} =
(languageN,
- [(nameN, name), (symbolsN, print_bool symbols), (antiquotesN, print_bool antiquotes)]);
+ [(nameN, name),
+ (symbolsN, print_bool symbols),
+ (antiquotesN, print_bool antiquotes),
+ (delimitedN, print_bool delimited)]);
-val language_method = language {name = "method", symbols = true, antiquotes = false};
-val language_sort = language {name = "sort", symbols = true, antiquotes = false};
-val language_type = language {name = "type", symbols = true, antiquotes = false};
-val language_term = language {name = "term", symbols = true, antiquotes = false};
-val language_prop = language {name = "prop", symbols = true, antiquotes = false};
-val language_ML = language {name = "ML", symbols = false, antiquotes = true};
-val language_document = language {name = "document", symbols = false, antiquotes = true};
-val language_antiquotation = language {name = "antiquotation", symbols = true, antiquotes = false};
-val language_text = language {name = "text", symbols = true, antiquotes = false};
-val language_rail = language {name = "rail", symbols = true, antiquotes = true};
+fun language' {name, symbols, antiquotes} delimited =
+ language {name = name, symbols = symbols, antiquotes = antiquotes, delimited = delimited};
+
+val language_method =
+ language {name = "method", symbols = true, antiquotes = false, delimited = false};
+val language_sort = language' {name = "sort", symbols = true, antiquotes = false};
+val language_type = language' {name = "type", symbols = true, antiquotes = false};
+val language_term = language' {name = "term", symbols = true, antiquotes = false};
+val language_prop = language' {name = "prop", symbols = true, antiquotes = false};
+val language_ML = language' {name = "ML", symbols = false, antiquotes = true};
+val language_document = language' {name = "document", symbols = false, antiquotes = true};
+val language_antiquotation =
+ language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
+val language_text = language' {name = "text", symbols = true, antiquotes = false};
+val language_rail = language {name = "rail", symbols = true, antiquotes = true, delimited = true};
(* formal entities *)
@@ -411,7 +426,7 @@
val (controlN, control) = markup_elem "control";
val tokenN = "token";
-fun token props = (tokenN, props);
+fun token delimited props = (tokenN, (delimitedN, print_bool delimited) :: props);
(* timing *)
--- a/src/Pure/PIDE/markup.scala Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Pure/PIDE/markup.scala Sat Mar 01 23:48:55 2014 +0100
@@ -94,6 +94,7 @@
val Symbols = new Properties.Boolean("symbols")
val Antiquotes = new Properties.Boolean("antiquotes")
+ val Delimited = new Properties.Boolean("delimited")
val LANGUAGE = "language"
object Language
@@ -101,12 +102,12 @@
val ML = "ML"
val UNKNOWN = "unknown"
- def unapply(markup: Markup): Option[(String, Boolean, Boolean)] =
+ def unapply(markup: Markup): Option[(String, Boolean, Boolean, Boolean)] =
markup match {
case Markup(LANGUAGE, props) =>
- (props, props, props) match {
- case (Name(name), Symbols(symbols), Antiquotes(antiquotes)) =>
- Some((name, symbols, antiquotes))
+ (props, props, props, props) match {
+ case (Name(name), Symbols(symbols), Antiquotes(antiquotes), Delimited(delimited)) =>
+ Some((name, symbols, antiquotes, delimited))
case _ => None
}
case _ => None
--- a/src/Pure/PIDE/markup_tree.scala Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Pure/PIDE/markup_tree.scala Sat Mar 01 23:48:55 2014 +0100
@@ -51,10 +51,10 @@
{
def markup: List[XML.Elem] = rev_markup.reverse
- def filter_markup(pred: String => Boolean): List[XML.Elem] =
+ def filter_markup(elements: Document.Elements): List[XML.Elem] =
{
var result: List[XML.Elem] = Nil
- for { elem <- rev_markup; if (pred(elem.name)) }
+ for { elem <- rev_markup; if (elements(elem.name)) }
result ::= elem
result.toList
}
@@ -194,7 +194,7 @@
def to_XML(text: CharSequence): XML.Body =
to_XML(Text.Range(0, text.length), text, (_: XML.Elem) => true)
- def cumulate[A](root_range: Text.Range, root_info: A, elements: String => Boolean,
+ def cumulate[A](root_range: Text.Range, root_info: A, elements: Document.Elements,
result: (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
{
def results(x: A, entry: Entry): Option[A] =
--- a/src/Pure/PIDE/protocol.scala Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Pure/PIDE/protocol.scala Sat Mar 01 23:48:55 2014 +0100
@@ -77,11 +77,11 @@
def command_status(markups: List[Markup]): Status =
(Status.init /: markups)(command_status(_, _))
- val command_status_elements: Set[String] =
- Set(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
+ val command_status_elements =
+ Document.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
Markup.FINISHED, Markup.FAILED)
- val status_elements: Set[String] =
+ val status_elements =
command_status_elements + Markup.WARNING + Markup.ERROR
@@ -165,7 +165,8 @@
/* result messages */
- private val clean_elements = Set(Markup.REPORT, Markup.NO_REPORT)
+ private val clean_elements =
+ Document.Elements(Markup.REPORT, Markup.NO_REPORT)
def clean_message(body: XML.Body): XML.Body =
body filter {
@@ -276,7 +277,7 @@
/* reported positions */
private val position_elements =
- Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
+ Document.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
def message_positions(
command_id: Document_ID.Command,
@@ -288,8 +289,8 @@
props match {
case Position.Reported(id, file_name, raw_range)
if (id == command_id || id == alt_id) && file_name == chunk.file_name =>
- chunk.decode(raw_range).try_restrict(chunk.range) match {
- case Some(range) if !range.is_singularity => set + range
+ chunk.incorporate(raw_range) match {
+ case Some(range) => set + range
case _ => set
}
case _ => set
--- a/src/Pure/Syntax/syntax.ML Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Pure/Syntax/syntax.ML Sat Mar 01 23:48:55 2014 +0100
@@ -14,10 +14,10 @@
val ambiguity_warning: bool Config.T
val ambiguity_limit_raw: Config.raw
val ambiguity_limit: int Config.T
- val read_token: string -> Symbol_Pos.T list * Position.T
val read_token_pos: string -> Position.T
+ val read_token: string -> Symbol_Pos.source
val parse_token: Proof.context -> (XML.tree list -> 'a) ->
- Markup.T -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a
+ (bool -> Markup.T) -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a
val parse_sort: Proof.context -> string -> sort
val parse_typ: Proof.context -> string -> typ
val parse_term: Proof.context -> string -> term
@@ -159,26 +159,33 @@
(* outer syntax token -- with optional YXML content *)
+local
+
fun token_position (XML.Elem ((name, props), _)) =
- if name = Markup.tokenN then Position.of_properties props
- else Position.none
- | token_position (XML.Text _) = Position.none;
+ if name = Markup.tokenN
+ then (Markup.is_delimited props, Position.of_properties props)
+ else (false, Position.none)
+ | token_position (XML.Text _) = (false, Position.none);
-fun explode_token tree =
+fun token_source tree =
let
val text = XML.content_of [tree];
- val pos = token_position tree;
- in (Symbol_Pos.explode (text, pos), pos) end;
+ val (delimited, pos) = token_position tree;
+ in {delimited = delimited, text = text, pos = pos} end;
-fun read_token str = explode_token (YXML.parse str handle Fail msg => error msg);
-fun read_token_pos str = token_position (YXML.parse str handle Fail msg => error msg);
+in
+
+fun read_token_pos str = #2 (token_position (YXML.parse str handle Fail msg => error msg));
+
+fun read_token str = token_source (YXML.parse str handle Fail msg => error msg);
fun parse_token ctxt decode markup parse str =
let
fun parse_tree tree =
let
- val (syms, pos) = explode_token tree;
- val _ = Context_Position.report ctxt pos markup;
+ val {delimited, text, pos} = token_source tree;
+ val syms = Symbol_Pos.explode (text, pos);
+ val _ = Context_Position.report ctxt pos (markup delimited);
in parse (syms, pos) end;
in
(case YXML.parse_body str handle Fail msg => error msg of
@@ -188,6 +195,8 @@
| body => decode body)
end;
+end;
+
(* (un)parsing *)
--- a/src/Pure/Syntax/syntax_phases.ML Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Sat Mar 01 23:48:55 2014 +0100
@@ -440,7 +440,8 @@
else decode_appl ps asts
| decode ps (Ast.Appl asts) = decode_appl ps asts;
- val (syms, pos) = Syntax.read_token str;
+ val {text, pos, ...} = Syntax.read_token str;
+ val syms = Symbol_Pos.explode (text, pos);
val ast =
parse_asts ctxt true root (syms, pos)
|> uncurry (report_result ctxt pos)
@@ -749,8 +750,8 @@
in
-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;
+val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast (Markup.language_sort false);
+val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast (Markup.language_type false);
fun unparse_term ctxt =
let
@@ -760,7 +761,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.language_term ctxt
+ (Markup.language_term false) ctxt
end;
end;
--- a/src/Pure/Thy/latex.ML Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Pure/Thy/latex.ML Sat Mar 01 23:48:55 2014 +0100
@@ -121,8 +121,8 @@
enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
else if Token.is_kind Token.Verbatim tok then
let
- val (txt, pos) = Token.source_position_of tok;
- val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
+ val {text, pos, ...} = Token.source_position_of tok;
+ val ants = Antiquote.read (Symbol_Pos.explode (text, pos), pos);
val out = implode (map output_syms_antiq ants);
in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
else if Token.is_kind Token.Cartouche tok then
--- a/src/Pure/Thy/thy_output.ML Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML Sat Mar 01 23:48:55 2014 +0100
@@ -25,7 +25,7 @@
datatype markup = Markup | MarkupEnv | Verbatim
val eval_antiq: Scan.lexicon -> Toplevel.state -> Antiquote.antiq -> string
val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
- val check_text: Symbol_Pos.text * Position.T -> Toplevel.state -> unit
+ val check_text: Symbol_Pos.source -> Toplevel.state -> unit
val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
(Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
val pretty_text: Proof.context -> string -> Pretty.T
@@ -184,10 +184,10 @@
end;
-fun check_text (txt, pos) state =
- (Position.report pos Markup.language_document;
+fun check_text {delimited, text, pos} state =
+ (Position.report pos (Markup.language_document delimited);
if Toplevel.is_skipped_proof state then ()
- else ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
+ else ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (text, pos)));
@@ -360,9 +360,9 @@
Parse.position (Scan.one (Token.is_command andf is_markup mark o Token.content_of)) --
Scan.repeat tag --
Parse.!!!! ((improper -- locale -- improper) |-- Parse.document_source --| improper_end)
- >> (fn (((tok, pos), tags), txt) =>
+ >> (fn (((tok, pos'), tags), {text, pos, ...}) =>
let val name = Token.content_of tok
- in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end));
+ in (SOME (name, pos', tags), (mk (name, (text, pos)), (flag, d))) end));
val command = Scan.peek (fn d =>
Parse.position (Scan.one (Token.is_command)) --
@@ -373,7 +373,7 @@
val cmt = Scan.peek (fn d =>
Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.document_source)
- >> (fn txt => (NONE, (MarkupToken ("cmt", txt), ("", d)))));
+ >> (fn {text, pos, ...} => (NONE, (MarkupToken ("cmt", (text, pos)), ("", d)))));
val other = Scan.peek (fn d =>
Parse.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d)))));
@@ -467,8 +467,12 @@
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_text_report ctxt source =
+ let
+ val {delimited, pos, ...} = source;
+ val _ = Context_Position.report ctxt pos (Markup.language_text delimited);
+ val (s, _) = Symbol_Pos.source_content source;
+ in pretty_text ctxt s end;
fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
@@ -574,7 +578,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 (Parse.position Args.name)) pretty_text_report #>
+ basic_entity (Binding.name "text") (Scan.lift Args.name_source_position) 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);
@@ -638,15 +642,18 @@
local
fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
- (fn {context, ...} => fn (txt, pos) =>
- (ML_Context.eval_in (SOME context) false pos (ml pos txt);
- Symbol_Pos.content (Symbol_Pos.explode (txt, pos))
+ (fn {context, ...} => fn source =>
+ (ML_Context.eval_in (SOME context) false (#pos source) (ml source);
+ Symbol_Pos.source_content source
+ |> #1
|> (if Config.get context quotes then quote else I)
|> (if Config.get context display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
else verb_text)));
-fun ml_enclose bg en pos txt =
- ML_Lex.read Position.none bg @ ML_Lex.read pos txt @ ML_Lex.read Position.none en;
+fun ml_enclose bg en source =
+ ML_Lex.read Position.none bg @
+ ML_Lex.read_source source @
+ ML_Lex.read Position.none en;
in
@@ -658,11 +665,11 @@
(ml_enclose "functor XXX() = struct structure XX = " " end;") #>
ml_text (Binding.name "ML_functor") (* FIXME formal treatment of functor name (!?) *)
- (fn pos => fn txt =>
+ (fn source =>
ML_Lex.read Position.none ("ML_Env.check_functor " ^
- ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (txt, pos))))) #>
+ ML_Syntax.print_string (#1 (Symbol_Pos.source_content source)))) #>
- ml_text (Binding.name "ML_text") (K (K [])));
+ ml_text (Binding.name "ML_text") (K []));
end;
--- a/src/Pure/Thy/thy_syntax.ML Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.ML Sat Mar 01 23:48:55 2014 +0100
@@ -44,14 +44,15 @@
fun reports_of_token tok =
let
+ val {text, pos, ...} = Token.source_position_of tok;
val malformed_symbols =
- Symbol_Pos.explode (Token.source_position_of tok)
+ Symbol_Pos.explode (text, pos)
|> map_filter (fn (sym, pos) =>
if Symbol.is_malformed sym
then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
- val (markup, txt) = Token.markup tok;
- val reports = ((Token.pos_of tok, markup), txt) :: malformed_symbols;
+ val (markup, msg) = Token.markup tok;
+ val reports = ((Token.pos_of tok, markup), msg) :: malformed_symbols;
in (is_malformed, reports) end;
in
--- a/src/Pure/Tools/rail.ML Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Pure/Tools/rail.ML Sat Mar 01 23:48:55 2014 +0100
@@ -192,10 +192,11 @@
in
-fun read ctxt (s, pos) =
+fun read ctxt (source: Symbol_Pos.source) =
let
+ val {text, pos, ...} = source;
val _ = Context_Position.report ctxt pos Markup.language_rail;
- val toks = tokenize (Symbol_Pos.explode (s, pos));
+ val toks = tokenize (Symbol_Pos.explode (text, pos));
val _ = Context_Position.reports ctxt (maps reports_of_token toks);
in #1 (Scan.error (Scan.finite stopper (rules --| !!! (Scan.ahead (Scan.one is_eof)))) toks) end;
--- a/src/Pure/pure_syn.ML Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Pure/pure_syn.ML Sat Mar 01 23:48:55 2014 +0100
@@ -24,9 +24,10 @@
let
val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
val provide = Thy_Load.provide (src_path, digest);
+ val source = {delimited = true, text = cat_lines lines, pos = pos};
in
gthy
- |> ML_Context.exec (fn () => ML_Context.eval_text true pos (cat_lines lines))
+ |> ML_Context.exec (fn () => ML_Context.eval_source true source)
|> Local_Theory.propagate_ml_env
|> Context.mapping provide (Local_Theory.background_theory provide)
end)));
--- a/src/Tools/Code/code_thingol.ML Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Tools/Code/code_thingol.ML Sat Mar 01 23:48:55 2014 +0100
@@ -882,7 +882,7 @@
(fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy');
fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');
fun read_const_expr str =
- (case Syntax.parse_token ctxt (K NONE) Markup.empty (SOME o Symbol_Pos.implode o #1) str of
+ (case Syntax.parse_token ctxt (K NONE) (K Markup.empty) (SOME o Symbol_Pos.implode o #1) str of
SOME "_" => ([], consts_of thy)
| SOME s =>
if String.isSuffix "._" s
--- a/src/Tools/jEdit/lib/Tools/jedit Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Sat Mar 01 23:48:55 2014 +0100
@@ -16,6 +16,7 @@
"src/documentation_dockable.scala"
"src/find_dockable.scala"
"src/fold_handling.scala"
+ "src/font_info.scala"
"src/graphview_dockable.scala"
"src/info_dockable.scala"
"src/isabelle.scala"
--- a/src/Tools/jEdit/src/actions.xml Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Tools/jEdit/src/actions.xml Sat Mar 01 23:48:55 2014 +0100
@@ -34,27 +34,27 @@
</ACTION>
<ACTION NAME="isabelle.reset-font-size">
<CODE>
- isabelle.jedit.Isabelle.reset_font_size(view);
+ isabelle.jedit.Isabelle.reset_font_size();
</CODE>
</ACTION>
<ACTION NAME="isabelle.increase-font-size">
<CODE>
- isabelle.jedit.Isabelle.increase_font_size(view);
+ isabelle.jedit.Isabelle.increase_font_size();
</CODE>
</ACTION>
<ACTION NAME="isabelle.increase-font-size2">
<CODE>
- isabelle.jedit.Isabelle.increase_font_size(view);
+ isabelle.jedit.Isabelle.increase_font_size();
</CODE>
</ACTION>
<ACTION NAME="isabelle.decrease-font-size">
<CODE>
- isabelle.jedit.Isabelle.decrease_font_size(view);
+ isabelle.jedit.Isabelle.decrease_font_size();
</CODE>
</ACTION>
<ACTION NAME="isabelle.decrease-font-size2">
<CODE>
- isabelle.jedit.Isabelle.decrease_font_size(view);
+ isabelle.jedit.Isabelle.decrease_font_size();
</CODE>
</ACTION>
<ACTION NAME="isabelle.complete">
--- a/src/Tools/jEdit/src/completion_popup.scala Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Sat Mar 01 23:48:55 2014 +0100
@@ -150,7 +150,7 @@
val context =
(opt_rendering orElse PIDE.document_view(text_area).map(_.get_rendering()) match {
case Some(rendering) =>
- rendering.language_context(before_caret_range(rendering))
+ rendering.completion_language(before_caret_range(rendering))
case None => None
}) getOrElse syntax.language_context
@@ -196,7 +196,8 @@
def open_popup(result: Completion.Result)
{
val font =
- painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
+ painter.getFont.deriveFont(
+ Font_Info.main_size(PIDE.options.real("jedit_popup_font_scale")))
val range = result.range
def invalidate(): Unit = JEdit_Lib.invalidate_range(text_area, range)
--- a/src/Tools/jEdit/src/find_dockable.scala Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Tools/jEdit/src/find_dockable.scala Sat Mar 01 23:48:55 2014 +0100
@@ -56,8 +56,8 @@
{
Swing_Thread.require()
- pretty_text_area.resize(Rendering.font_family(),
- (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
+ pretty_text_area.resize(
+ Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
}
private val delay_resize =
@@ -121,7 +121,7 @@
{ val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
setColumns(40)
setToolTipText(query_label.tooltip)
- setFont(GUI.imitate_font(Rendering.font_family(), getFont, 1.2))
+ setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
}
private case class Context_Entry(val name: String, val description: String)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/font_info.scala Sat Mar 01 23:48:55 2014 +0100
@@ -0,0 +1,94 @@
+/* Title: Tools/jEdit/src/font_info.scala
+ Author: Makarius
+
+Font information, derived from main jEdit view font.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+
+import java.awt.Font
+
+import org.gjt.sp.jedit.{jEdit, View}
+
+
+object Font_Info
+{
+ /* size range */
+
+ val min_size = 5
+ val max_size = 250
+
+ def restrict_size(size: Float): Float = size max min_size min max_size
+
+
+ /* main jEdit font */
+
+ def main_family(): String = jEdit.getProperty("view.font")
+
+ def main_size(scale: Double = 1.0): Float =
+ restrict_size(jEdit.getIntegerProperty("view.fontsize", 16).toFloat * scale.toFloat)
+
+ def main(scale: Double = 1.0): Font_Info =
+ Font_Info(main_family(), main_size(scale))
+
+
+ /* incremental size change */
+
+ object main_change
+ {
+ private def change_size(change: Float => Float)
+ {
+ Swing_Thread.require()
+
+ val size0 = main_size()
+ val size = restrict_size(change(size0)).round
+ if (size != size0) {
+ jEdit.setIntegerProperty("view.fontsize", size)
+ jEdit.propertiesChanged()
+ jEdit.saveSettings()
+ jEdit.getActiveView().getStatus.setMessageAndClear("Text font size: " + size)
+ }
+ }
+
+ // owned by Swing thread
+ private var steps = 0
+ private val delay = Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
+ {
+ change_size(size =>
+ {
+ var i = size.round
+ while (steps != 0 && i > 0) {
+ if (steps > 0)
+ { i += (i / 10) max 1; steps -= 1 }
+ else
+ { i -= (i / 10) max 1; steps += 1 }
+ }
+ steps = 0
+ i.toFloat
+ })
+ }
+
+ def step(i: Int)
+ {
+ steps += i
+ delay.invoke()
+ }
+
+ def reset(size: Float)
+ {
+ delay.revoke()
+ steps = 0
+ change_size(_ => size)
+ }
+ }
+}
+
+sealed case class Font_Info(family: String, size: Float)
+{
+ def font: Font = new Font(family, Font.PLAIN, size.round)
+}
+
--- a/src/Tools/jEdit/src/info_dockable.scala Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala Sat Mar 01 23:48:55 2014 +0100
@@ -76,8 +76,8 @@
{
Swing_Thread.require()
- pretty_text_area.resize(Rendering.font_family(),
- (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
+ pretty_text_area.resize(
+ Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
}
--- a/src/Tools/jEdit/src/isabelle.scala Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Sat Mar 01 23:48:55 2014 +0100
@@ -186,14 +186,11 @@
/* font size */
- def reset_font_size(view: View): Unit =
- Rendering.font_size_change(view, _ => PIDE.options.int("jedit_reset_font_size"))
-
- def increase_font_size(view: View): Unit =
- Rendering.font_size_change(view, i => i + ((i / 10) max 1))
-
- def decrease_font_size(view: View): Unit =
- Rendering.font_size_change(view, i => i - ((i / 10) max 1))
+ def reset_font_size() {
+ Font_Info.main_change.reset(PIDE.options.int("jedit_reset_font_size").toFloat)
+ }
+ def increase_font_size() { Font_Info.main_change.step(1) }
+ def decrease_font_size() { Font_Info.main_change.step(-1) }
/* structured edits */
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Sat Mar 01 23:48:55 2014 +0100
@@ -30,7 +30,7 @@
protected var _end = int_to_pos(end)
override def getIcon: Icon = null
override def getShortString: String =
- "<html><span style=\"font-family: " + Rendering.font_family() + ";\">" +
+ "<html><span style=\"font-family: " + Font_Info.main_family() + ";\">" +
HTML.encode(_name) + "</span></html>"
override def getLongString: String = _name
override def getName: String = _name
--- a/src/Tools/jEdit/src/jedit_editor.scala Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Sat Mar 01 23:48:55 2014 +0100
@@ -156,7 +156,7 @@
override def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
new Hyperlink { def follow(view: View) = goto(view, name, line, column) }
- override def hyperlink_command(snapshot: Document.Snapshot, command: Command, offset: Int = 0)
+ override def hyperlink_command(snapshot: Document.Snapshot, command: Command, raw_offset: Int = 0)
: Option[Hyperlink] =
{
if (snapshot.is_outdated) None
@@ -167,8 +167,8 @@
val file_name = command.node_name.node
val sources =
node.commands.iterator.takeWhile(_ != command).map(_.source) ++
- (if (offset == 0) Iterator.empty
- else Iterator.single(command.source(Text.Range(0, command.decode(offset)))))
+ (if (raw_offset == 0) Iterator.empty
+ else Iterator.single(command.source(Text.Range(0, command.decode(raw_offset)))))
val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
Some(new Hyperlink { def follow(view: View) { goto(view, file_name, line, column) } })
}
--- a/src/Tools/jEdit/src/output_dockable.scala Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Sat Mar 01 23:48:55 2014 +0100
@@ -41,8 +41,8 @@
{
Swing_Thread.require()
- pretty_text_area.resize(Rendering.font_family(),
- (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
+ pretty_text_area.resize(
+ Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
}
private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
--- a/src/Tools/jEdit/src/pretty_text_area.scala Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Sat Mar 01 23:48:55 2014 +0100
@@ -61,8 +61,7 @@
Swing_Thread.require()
- private var current_font_family = "Dialog"
- private var current_font_size: Int = 12
+ private var current_font_info: Font_Info = Font_Info.main()
private var current_body: XML.Body = Nil
private var current_base_snapshot = Document.Snapshot.init
private var current_base_results = Command.Results.empty
@@ -80,18 +79,19 @@
{
Swing_Thread.require()
- val font = new Font(current_font_family, Font.PLAIN, current_font_size)
+ val font = current_font_info.font
getPainter.setFont(font)
getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
getPainter.setFractionalFontMetricsEnabled(jEdit.getBooleanProperty("view.fracFontMetrics"))
- getPainter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size))
+ getPainter.setStyles(
+ SyntaxUtilities.loadStyles(current_font_info.family, current_font_info.size.round))
val fold_line_style = new Array[SyntaxStyle](4)
for (i <- 0 to 3) {
fold_line_style(i) =
SyntaxUtilities.parseStyle(
jEdit.getProperty("view.style.foldLine." + i),
- current_font_family, current_font_size, true)
+ current_font_info.family, current_font_info.size.round, true)
}
getPainter.setFoldLineStyle(fold_line_style)
@@ -139,12 +139,11 @@
}
}
- def resize(font_family: String, font_size: Int)
+ def resize(font_info: Font_Info)
{
Swing_Thread.require()
- current_font_family = font_family
- current_font_size = font_size
+ current_font_info = font_info
refresh()
}
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Sat Mar 01 23:48:55 2014 +0100
@@ -199,8 +199,7 @@
}
})
- pretty_text_area.resize(Rendering.font_family(),
- Rendering.font_size("jedit_popup_font_scale").round)
+ pretty_text_area.resize(Font_Info.main(PIDE.options.real("jedit_popup_font_scale")))
/* main content */
--- a/src/Tools/jEdit/src/rendering.scala Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Sat Mar 01 23:48:55 2014 +0100
@@ -41,27 +41,6 @@
Markup.ERROR -> error_pri, Markup.ERROR_MESSAGE -> error_pri)
- /* jEdit font */
-
- def font_family(): String = jEdit.getProperty("view.font")
-
- private def view_font_size(): Int = jEdit.getIntegerProperty("view.fontsize", 16)
- private val font_size0 = 5
- private val font_size1 = 250
-
- def font_size(scale: String): Float =
- (view_font_size() * PIDE.options.real(scale)).toFloat max font_size0 min font_size1
-
- def font_size_change(view: View, change: Int => Int)
- {
- val size = change(view_font_size()) max font_size0 min font_size1
- jEdit.setIntegerProperty("view.fontsize", size)
- jEdit.propertiesChanged()
- jEdit.saveSettings()
- view.getStatus.setMessageAndClear("Text font size: " + size)
- }
-
-
/* popup window bounds */
def popup_bounds: Double = (PIDE.options.real("jedit_popup_bounds") max 0.2) min 0.8
@@ -150,28 +129,29 @@
/* markup elements */
- private val completion_names_elements = Set(Markup.COMPLETION)
+ private val completion_names_elements =
+ Document.Elements(Markup.COMPLETION)
- private val language_context_elements =
- Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
+ private val completion_language_elements =
+ Document.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
Markup.ML_STRING, Markup.ML_COMMENT)
private val highlight_elements =
- Set(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
+ Document.Elements(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)
private val hyperlink_elements =
- Set(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
+ Document.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
private val active_elements =
- Set(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
+ Document.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
Markup.SENDBACK, Markup.SIMP_TRACE)
private val tooltip_message_elements =
- Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
+ Document.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
private val tooltip_descriptions =
Map(
@@ -184,22 +164,23 @@
Markup.TVAR -> "schematic type variable")
private val tooltip_elements =
- Set(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
+ Document.Elements(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++
- tooltip_descriptions.keys
+ Document.Elements(tooltip_descriptions.keySet)
private val gutter_elements =
- Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
+ Document.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
private val squiggly_elements =
- Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
+ Document.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
private val line_background_elements =
- Set(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE,
+ Document.Elements(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE,
Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE,
Markup.INFORMATION)
- private val separator_elements = Set(Markup.SEPARATOR)
+ private val separator_elements =
+ Document.Elements(Markup.SEPARATOR)
private val background_elements =
Protocol.command_status_elements + Markup.WRITELN_MESSAGE +
@@ -208,13 +189,14 @@
active_elements
private val foreground_elements =
- Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
+ Document.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
Markup.CARTOUCHE, Markup.ANTIQUOTED)
- private val bullet_elements = Set(Markup.BULLET)
+ private val bullet_elements =
+ Document.Elements(Markup.BULLET)
private val fold_depth_elements =
- Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
+ Document.Elements(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
}
@@ -285,11 +267,12 @@
}).headOption.map(_.info)
}
- def language_context(range: Text.Range): Option[Completion.Language_Context] =
- snapshot.select(range, Rendering.language_context_elements, _ =>
+ def completion_language(range: Text.Range): Option[Completion.Language_Context] =
+ snapshot.select(range, Rendering.completion_language_elements, _ =>
{
- case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes), _)) =>
- Some(Completion.Language_Context(language, symbols, antiquotes))
+ case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes, delimited), _)) =>
+ if (delimited) Some(Completion.Language_Context(language, symbols, antiquotes))
+ else None
case Text.Info(_, elem)
if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
Some(Completion.Language_Context.ML_inner)
@@ -421,7 +404,7 @@
def command_results(range: Text.Range): Command.Results =
{
val results =
- snapshot.select[Command.Results](range, _ => true, command_state =>
+ snapshot.select[Command.Results](range, Document.Elements.full, command_state =>
{ case _ => Some(command_state.results) }).map(_.info)
(Command.Results.empty /: results)(_ ++ _)
}
@@ -503,7 +486,7 @@
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(language, _, _), _))) =>
+ case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
Some(add(prev, r, (true, XML.Text("language: " + language))))
case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
Rendering.tooltip_descriptions.get(name).
@@ -703,7 +686,8 @@
Markup.ML_STRING -> inner_quoted_color,
Markup.ML_COMMENT -> inner_comment_color)
- private lazy val text_color_elements = text_colors.keySet
+ private lazy val text_color_elements =
+ Document.Elements(text_colors.keySet)
def text_color(range: Text.Range, color: Color): List[Text.Info[Color]] =
{
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Sat Mar 01 23:48:55 2014 +0100
@@ -84,7 +84,7 @@
private def do_paint()
{
Swing_Thread.later {
- text_area.resize(Rendering.font_family(), Rendering.font_size("jedit_font_scale").round)
+ text_area.resize(Font_Info.main(PIDE.options.real("jedit_font_scale")))
}
}
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Sat Mar 01 23:48:55 2014 +0100
@@ -181,7 +181,7 @@
def do_paint()
{
Swing_Thread.later {
- area.resize(Rendering.font_family(), Rendering.font_size("jedit_font_scale").round)
+ area.resize(Font_Info.main(PIDE.options.real("jedit_font_scale")))
}
}
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Sat Mar 01 23:48:55 2014 +0100
@@ -57,8 +57,8 @@
{
Swing_Thread.require()
- pretty_text_area.resize(Rendering.font_family(),
- (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
+ pretty_text_area.resize(
+ Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
}
private val delay_resize =
--- a/src/Tools/jEdit/src/symbols_dockable.scala Sat Mar 01 20:40:31 2014 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Sat Mar 01 23:48:55 2014 +0100
@@ -26,7 +26,7 @@
private class Symbol_Component(val symbol: String) extends Button
{
private val decoded = Symbol.decode(symbol)
- private val font_size = Rendering.font_size("jedit_font_scale").round
+ private val font_size = Font_Info.main_size(PIDE.options.real("jedit_font_scale")).round
font =
Symbol.fonts.get(symbol) match {