# HG changeset patch # User wenzelm # Date 1393714135 -3600 # Node ID eebefb9a2b0185edee29620f257730e2411454a2 # Parent e21d83c8e1c74719dc6799d10b275612c9f7a5b8# Parent b7bdea5336dd68ca83b7a3235fe6bb533627f0da merged diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Doc/antiquote_setup.ML --- 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) ^ "}" ^ diff -r e21d83c8e1c7 -r eebefb9a2b01 src/HOL/Library/BigO.thy --- 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 \ 'b::linordered_idom) \ ('a \ 'b) set" ("(1O'(_'))") + where "O(f:: 'a \ 'b) = {h. \c. \x. abs (h x) \ 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: + "(\c::'a::linordered_idom. \x. abs (h x) \ c * abs (f x)) \ + (\c. 0 < c \ (\x. abs (h x) \ 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) \ 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. \c. 0 < c \ (\x. abs (h x) \ 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 \ O(g) \ O(f) \ 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) \ 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 \ 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 \ 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(\x. 0) = {\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) \ 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) \ 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 = "\n. if abs (g n) \ (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) \ (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) \ 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 = "\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) \ (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) \ 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 \ O(f) \ B \ O(f) \ A + B \ O(f)" + apply (subgoal_tac "A + B \ 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: "\x. 0 \ f x \ \x. 0 \ g x \ 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 \ 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 \ 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) \ 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 (rule add_mono) - apply (subgoal_tac "c * f xa <= max c ca * f xa") - apply (force) + apply (subgoal_tac "c * f xa \ 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 \ 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: "\x. 0 \ f x \ \x. f x \ c * g x \ f \ 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: "\x. 0 \ f x \ \x. f x \ g x \ f \ 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: "\x. lb x \ f x \ \x. f x \ lb x + g x \ f \ 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: "(\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(\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(\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) \ (\x. abs (f x)) =o (\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 \ O(h)" + have "(\x. abs (f x) - abs (g x)) =o O(\x. abs (abs (f x) - abs (g x)))" by (rule bigo_abs2) - also have "... <= O(%x. abs (f x - g x))" + also have "\ \ O(\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 "\ \ 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 "\ \ O(h)" by (rule bigo_elt_subset) - finally show "(%x. abs (f x) - abs (g x)) : O(h)". + finally show "(\x. abs (f x) - abs (g x)) \ O(h)". qed -lemma bigo_abs5: "f =o O(g) ==> (%x. abs(f x)) =o O(g)" +lemma bigo_abs5: "f =o O(g) \ (\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 \ g +o O(h) \ O(f) \ O(g) + O(h)" proof - - assume "f : g +o O(h)" - also have "... <= O(g) + O(h)" + assume "f \ g +o O(h)" + also have "\ \ O(g) + O(h)" by (auto del: subsetI) - also have "... = O(%x. abs(g x)) + O(%x. abs(h x))" + also have "\ = O(\x. abs (g x)) + O(\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 "\ = O((\x. abs (g x)) + (\x. abs (h x)))" + by (rule bigo_plus_eq [symmetric]) auto + finally have "f \ \" . + then have "O(f) \ \" by (elim bigo_elt_subset) - also have "... = O(%x. abs(g x)) + O(%x. abs(h x))" + also have "\ = O(\x. abs (g x)) + O(\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) \ 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) \ 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) \ 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 \ O(h) \ g \ O(j) \ f * g \ 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 \ k +o O(h) \ g * f \ (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 \ 'b::linordered_field" + assumes "\x. f x \ 0" + shows "O(f * g) \ 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 \ O(f * g)" + then have "(\x. 1 / (f x)) * h \ (\x. 1 / f x) *o O(f * g)" by auto - also have "... <= O((%x. 1 / f x) * (f * g))" + also have "\ \ O((\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 "(\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 "(\x. (1::'b) / f x) * h \ O(g)" . + then have "f * ((\x. (1::'b) / f x) * h) \ f *o O(g)" by auto - also have "f * ((%x. (1::'b) / f x) * h) = h" - apply (simp add: func_times) + also have "f * ((\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 \ 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 \ 'b::linordered_field" + shows "\x. f x \ 0 \ 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 \ 'b::linordered_field" + shows "\x. f x \ 0 \ O(f * g) \ 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 \ 'b::linordered_field" + shows "\x. f x \ 0 \ 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 \ O(g) \ - f \ 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 \ g +o O(h) \ - f \ -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 \ O(g) \ f +o O(g) \ O(g)" proof - - assume a: "f : O(g)" - show "f +o O(g) <= O(g)" + assume a: "f \ O(g)" + show "f +o O(g) \ O(g)" proof - - have "f : O(f)" by auto - then have "f +o O(g) <= O(f) + O(g)" + have "f \ O(f)" by auto + then have "f +o O(g) \ O(f) + O(g)" by (auto del: subsetI) - also have "... <= O(g) + O(g)" + also have "\ \ O(g) + O(g)" proof - - from a have "O(f) <= O(g)" by (auto del: subsetI) + from a have "O(f) \ O(g)" by (auto del: subsetI) thus ?thesis by (auto del: subsetI) qed - also have "... <= O(g)" by simp + also have "\ \ 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 \ O(g) \ O(g) \ f +o O(g)" proof - - assume a: "f : O(g)" - show "O(g) <= f +o O(g)" + assume a: "f \ O(g)" + show "O(g) \ 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 \ 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)" 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 \ O(g) \ 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 \ O(g) \ A \ O(g) \ f +o A \ O(g)" + apply (subgoal_tac "f +o A \ 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 \ g +o O(h) \ g \ 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 \ g +o O(h) \ g \ 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: "(\x. c) \ O(\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(\x. c) \ O(\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 \ 0 \ (\x. 1) \ O(\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 \ 0 \ O(\x. 1) \ O(\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 \ 0 \ O(\x. c) = O(\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: "(\x. c * f x) \ 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(\x. c * f x) \ 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 \ 0 \ f \ O(\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 \ 0 \ O(f) \ O(\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 \ 0 \ O(\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 \ 0 \ (\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 = "\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]: "(\x. c) *o O(f) \ 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) \ (\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 "(\x. c) * f =o (\x. c) *o O(g)" by auto - also have "(%x. c) * f = (%x. c * f x)" + also have "(\x. c) * f = (\x. c * f x)" by (simp add: func_times) - also have "(%x. c) *o O(g) <= O(g)" + also have "(\x. c) *o O(g) \ 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) \ (\x. f (k x)) =o O(\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) \ + (\x. f (k x)) =o (\x. g (k x)) +o O(\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: "\x. \y \ A x. 0 \ h x y \ + \c. \x. \y \ A x. abs (f x y) \ c * (h x y) \ + (\x. \y \ A x. f x y) =o O(\x. \y \ 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: "\x y. 0 \ h x y \ + \c. \x y. abs (f x y) \ c * h x y \ + (\x. \y \ A x. f x y) =o O(\x. \y \ 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: "\y. 0 \ h y \ + \c. \y. abs (f y) \ c * (h y) \ + (\x. \y \ A x. f y) =o O(\x. \y \ 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) \ + (\x. \y \ A x. l x y * f (k x y)) =o O(\x. \y \ 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) \ + (\x. \y \ A x. l x y * f (k x y)) =o + (\x. \y \ A x. l x y * g (k x y)) +o + O(\x. \y \ 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) \ \x y. 0 \ l x y \ + \x. 0 \ h x \ + (\x. \y \ A x. l x y * f (k x y)) =o + O(\x. \y \ A x. l x y * h (k x y))" + apply (subgoal_tac "(\x. \y \ A x. l x y * h (k x y)) = + (\x. \y \ 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) \ \x y. 0 \ l x y \ + \x. 0 \ h x \ + (\x. \y \ A x. l x y * f (k x y)) =o + (\x. \y \ A x. l x y * g (k x y)) +o + O(\x. \y \ 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 \ O(f) \ B \ O(f) \ A + B \ 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) \ g =o O(h) \ 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 \ 0 \ (\x. c) * f =o O(h) \ f =o O(h)" apply (rule subsetD) - apply (subgoal_tac "(%x. 1 / c) *o O(h) <= O(h)") + apply (subgoal_tac "(\x. 1 / c) *o O(h) \ O(h)") apply assumption apply (rule bigo_const_mult6) - apply (subgoal_tac "f = (%x. 1 / c) * ((%x. c) * f)") + apply (subgoal_tac "f = (\x. 1 / c) * ((\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: "(\x::nat. f (x + 1)) =o O(\x. h (x + 1)) \ f 0 = 0 \ 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: + "(\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)" 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 " 'b::linordered_idom) \ ('a \ 'b) \ 'a \ 'b" (infixl "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) \ \x. abs (g x) \ abs (f x) \ 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) \ \x. abs (g x) \ f x \ 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) \ \x. 0 \ g x \ \x. g x \ f x \ 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) \ + \x. 0 \ g x \ \x. g x \ abs (f x) \ 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 x. f x \ g x \ f 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 + \x. 0 \ k x \ \x. k x \ f x \ k 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 + \x. 0 \ k x \ \x. g x \ k x \ f 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 'b::linordered_field) ==> - g =o h +o O(k) ==> f 'b::linordered_field" + shows "f g =o h +o O(k) \ f - EX C. ALL x. f x <= g x + C * abs(h x)" +lemma bigo_lesso5: "f \C. \x. f x \ 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 - k (f + k) k (f + k) g ----> 0 ==> f ----> (0::real)" +lemma bigo_LIMSEQ1: "f =o O(g) \ g ----> 0 \ 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) \ h ----> 0 \ f ----> a \ 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 diff -r e21d83c8e1c7 -r eebefb9a2b01 src/HOL/ex/Cartouche_Examples.thy --- 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; *} diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Pure/General/symbol_pos.ML --- 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 diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Pure/Isar/args.ML --- 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 diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Pure/Isar/attrib.ML --- 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 ^ ")"))); diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Pure/Isar/isar_cmd.ML --- 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; diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Pure/Isar/isar_syn.ML --- 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" diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Pure/Isar/method.ML --- 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 ^ ")"))); diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Pure/Isar/parse.ML --- 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 diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Pure/Isar/proof_context.ML --- 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 diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Pure/Isar/token.ML --- 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; diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Pure/ML/ml_context.ML --- 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 diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Pure/ML/ml_lex.ML --- 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; diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Pure/PIDE/command.scala --- 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 */ diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Pure/PIDE/document.scala --- 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]] = { diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Pure/PIDE/markup.ML --- 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 *) diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Pure/PIDE/markup.scala --- 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 diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Pure/PIDE/markup_tree.scala --- 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] = diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Pure/PIDE/protocol.scala --- 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 diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Pure/Syntax/syntax.ML --- 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 *) diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Pure/Syntax/syntax_phases.ML --- 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; diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Pure/Thy/latex.ML --- 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 diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Pure/Thy/thy_output.ML --- 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; diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Pure/Thy/thy_syntax.ML --- 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 diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Pure/Tools/rail.ML --- 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; diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Pure/pure_syn.ML --- 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))); diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Tools/Code/code_thingol.ML --- 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 diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Tools/jEdit/lib/Tools/jedit --- 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" diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Tools/jEdit/src/actions.xml --- 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 @@ - isabelle.jedit.Isabelle.reset_font_size(view); + isabelle.jedit.Isabelle.reset_font_size(); - isabelle.jedit.Isabelle.increase_font_size(view); + isabelle.jedit.Isabelle.increase_font_size(); - isabelle.jedit.Isabelle.increase_font_size(view); + isabelle.jedit.Isabelle.increase_font_size(); - isabelle.jedit.Isabelle.decrease_font_size(view); + isabelle.jedit.Isabelle.decrease_font_size(); - isabelle.jedit.Isabelle.decrease_font_size(view); + isabelle.jedit.Isabelle.decrease_font_size(); diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Tools/jEdit/src/completion_popup.scala --- 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) diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Tools/jEdit/src/find_dockable.scala --- 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) diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Tools/jEdit/src/font_info.scala --- /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) +} + diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Tools/jEdit/src/info_dockable.scala --- 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)) } diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Tools/jEdit/src/isabelle.scala --- 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 */ diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Tools/jEdit/src/isabelle_sidekick.scala --- 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.encode(_name) + "" override def getLongString: String = _name override def getName: String = _name diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Tools/jEdit/src/jedit_editor.scala --- 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) } }) } diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Tools/jEdit/src/output_dockable.scala --- 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]]) diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Tools/jEdit/src/pretty_text_area.scala --- 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() } diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Tools/jEdit/src/pretty_tooltip.scala --- 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 */ diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Tools/jEdit/src/rendering.scala --- 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]] = { diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Tools/jEdit/src/simplifier_trace_dockable.scala --- 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"))) } } diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Tools/jEdit/src/simplifier_trace_window.scala --- 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"))) } } diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Tools/jEdit/src/sledgehammer_dockable.scala --- 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 = diff -r e21d83c8e1c7 -r eebefb9a2b01 src/Tools/jEdit/src/symbols_dockable.scala --- 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 {