--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sun Aug 21 19:47:52 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sun Aug 21 22:56:55 2011 +0200
@@ -728,7 +728,7 @@
apply (subst matrix_vector_mul[OF lf])
unfolding adjoint_matrix matrix_of_matrix_vector_mul ..
-section {* lambda skolemization on cartesian products *}
+subsection {* lambda skolemization on cartesian products *}
(* FIXME: rename do choice_cart *)
@@ -1404,7 +1404,7 @@
thus ?case using goal1 by auto
qed
-section "Convex Euclidean Space"
+subsection "Convex Euclidean Space"
lemma Cart_1:"(1::real^'n) = (\<chi>\<chi> i. 1)"
apply(subst euclidean_eq)
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sun Aug 21 19:47:52 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sun Aug 21 22:56:55 2011 +0200
@@ -17,16 +17,13 @@
(* To be moved elsewhere *)
(* ------------------------------------------------------------------------- *)
-lemma linear_scaleR: "linear (%(x :: 'n::euclidean_space). scaleR c x)"
- by (metis linear_conv_bounded_linear bounded_linear_scaleR_right)
-
-lemma injective_scaleR:
-assumes "(c :: real) ~= 0"
-shows "inj (%(x :: 'n::euclidean_space). scaleR c x)"
- by (metis assms injI real_vector.scale_cancel_left)
+lemma linear_scaleR: "linear (\<lambda>x. scaleR c x)"
+ by (simp add: linear_def scaleR_add_right)
+
+lemma injective_scaleR: "c \<noteq> 0 \<Longrightarrow> inj (\<lambda>(x::'a::real_vector). scaleR c x)"
+ by (simp add: inj_on_def)
lemma linear_add_cmul:
-fixes f :: "('m::euclidean_space) => ('n::euclidean_space)"
assumes "linear f"
shows "f(a *\<^sub>R x + b *\<^sub>R y) = a *\<^sub>R f x + b *\<^sub>R f y"
using linear_add[of f] linear_cmul[of f] assms by (simp)
@@ -50,7 +47,7 @@
by (blast dest: inj_onD)
lemma independent_injective_on_span_image:
- assumes iS: "independent (S::(_::euclidean_space) set)"
+ assumes iS: "independent S"
and lf: "linear f" and fi: "inj_on f (span S)"
shows "independent (f ` S)"
proof-
@@ -83,7 +80,6 @@
qed
lemma linear_injective_on_subspace_0:
-fixes f :: "('m::euclidean_space) => ('n::euclidean_space)"
assumes lf: "linear f" and "subspace S"
shows "inj_on f S <-> (!x : S. f x = 0 --> x = 0)"
proof-
@@ -166,7 +162,7 @@
apply(rule ccontr) by auto
lemma translate_inj_on:
-fixes A :: "('n::euclidean_space) set"
+fixes A :: "('a::ab_group_add) set"
shows "inj_on (%x. a+x) A" unfolding inj_on_def by auto
lemma translation_assoc:
@@ -241,7 +237,7 @@
qed
lemma closure_linear_image:
-fixes f :: "('m::euclidean_space) => ('n::euclidean_space)"
+fixes f :: "('m::euclidean_space) => ('n::real_normed_vector)"
assumes "linear f"
shows "f ` (closure S) <= closure (f ` S)"
using image_closure_subset[of S f "closure (f ` S)"] assms linear_conv_bounded_linear[of f]
@@ -262,8 +258,8 @@
qed
lemma closure_direct_sum:
-fixes S :: "('n::euclidean_space) set"
-fixes T :: "('m::euclidean_space) set"
+fixes S :: "('n::real_normed_vector) set"
+fixes T :: "('m::real_normed_vector) set"
shows "closure (S <*> T) = closure S <*> closure T"
proof-
{ fix x assume "x : closure S <*> closure T"
@@ -290,7 +286,7 @@
closure_subset[of S] closure_subset[of T] by auto
qed
-lemma closure_scaleR:
+lemma closure_scaleR: (* TODO: generalize to real_normed_vector *)
fixes S :: "('n::euclidean_space) set"
shows "(op *\<^sub>R c) ` (closure S) = closure ((op *\<^sub>R c) ` S)"
proof-
@@ -347,7 +343,7 @@
using image_affinity_interval[of m 0 a b] by auto
lemma dist_triangle_eq:
- fixes x y z :: "'a::euclidean_space"
+ fixes x y z :: "'a::real_inner"
shows "dist x z = dist x y + dist y z \<longleftrightarrow> norm (x - y) *\<^sub>R (y - z) = norm (y - z) *\<^sub>R (x - y)"
proof- have *:"x - y + (y - z) = x - z" by auto
show ?thesis unfolding dist_norm norm_triangle_eq[of "x - y" "y - z", unfolded *]
@@ -594,7 +590,6 @@
subsection {* Some relations between affine hull and subspaces. *}
lemma affine_hull_insert_subset_span:
- fixes a :: "'a::euclidean_space"
shows "affine hull (insert a s) \<subseteq> {a + v| v . v \<in> span {x - a | x . x \<in> s}}"
unfolding subset_eq Ball_def unfolding affine_hull_explicit span_explicit mem_Collect_eq
apply(rule,rule) apply(erule exE)+ apply(erule conjE)+ proof-
@@ -612,7 +607,6 @@
unfolding as by simp qed
lemma affine_hull_insert_span:
- fixes a :: "'a::euclidean_space"
assumes "a \<notin> s"
shows "affine hull (insert a s) =
{a + v | v . v \<in> span {x - a | x. x \<in> s}}"
@@ -632,7 +626,6 @@
by (auto simp add: setsum_subtractf scaleR_left.setsum algebra_simps *) qed
lemma affine_hull_span:
- fixes a :: "'a::euclidean_space"
assumes "a \<in> s"
shows "affine hull s = {a + v | v. v \<in> span {x - a | x. x \<in> s - {a}}}"
using affine_hull_insert_span[of a "s - {a}", unfolded insert_Diff[OF assms]] by auto
@@ -708,14 +701,12 @@
from this show ?thesis using affine_translation assms by auto
qed
-lemma subspace_imp_affine:
- fixes s :: "(_::euclidean_space) set" shows "subspace s \<Longrightarrow> affine s"
+lemma subspace_imp_affine: "subspace s \<Longrightarrow> affine s"
unfolding subspace_def affine_def by auto
subsection{* Subspace Parallel to an Affine Set *}
lemma subspace_affine:
- fixes S :: "('n::euclidean_space) set"
shows "subspace S <-> (affine S & 0 : S)"
proof-
have h0: "subspace S ==> (affine S & 0 : S)" using subspace_imp_affine[of S] subspace_0 by auto
@@ -740,7 +731,6 @@
qed
lemma affine_diffs_subspace:
- fixes S :: "('n::euclidean_space) set"
assumes "affine S" "a : S"
shows "subspace ((%x. (-a)+x) ` S)"
proof-
@@ -750,7 +740,6 @@
qed
lemma parallel_subspace_explicit:
-fixes a :: "'n::euclidean_space"
assumes "affine S" "a : S"
assumes "L == {y. ? x : S. (-a)+x=y}"
shows "subspace L & affine_parallel S L"
@@ -762,7 +751,6 @@
qed
lemma parallel_subspace_aux:
-fixes A B :: "('n::euclidean_space) set"
assumes "subspace A" "subspace B" "affine_parallel A B"
shows "A>=B"
proof-
@@ -773,7 +761,6 @@
qed
lemma parallel_subspace:
-fixes A B :: "('n::euclidean_space) set"
assumes "subspace A" "subspace B" "affine_parallel A B"
shows "A=B"
proof-
@@ -783,7 +770,6 @@
qed
lemma affine_parallel_subspace:
-fixes S :: "('n::euclidean_space) set"
assumes "affine S" "S ~= {}"
shows "?!L. subspace L & affine_parallel S L"
proof-
@@ -824,7 +810,6 @@
using assms cone_def[of S] by auto
lemma cone_contains_0:
-fixes S :: "('m::euclidean_space) set"
assumes "cone S"
shows "(S ~= {}) <-> (0 : S)"
proof-
@@ -833,15 +818,13 @@
} from this show ?thesis by auto
qed
-lemma cone_0:
-shows "cone {(0 :: 'm::euclidean_space)}"
+lemma cone_0: "cone {0}"
unfolding cone_def by auto
lemma cone_Union[intro]: "(!s:f. cone s) --> (cone (Union f))"
unfolding cone_def by blast
lemma cone_iff:
-fixes S :: "('m::euclidean_space) set"
assumes "S ~= {}"
shows "cone S <-> 0:S & (!c. c>0 --> ((op *\<^sub>R c) ` S) = S)"
proof-
@@ -875,12 +858,10 @@
by (metis cone_empty cone_hull_eq)
lemma cone_hull_empty_iff:
-fixes S :: "('m::euclidean_space) set"
shows "(S = {}) <-> (cone hull S = {})"
by (metis bot_least cone_hull_empty hull_subset xtrans(5))
lemma cone_hull_contains_0:
-fixes S :: "('m::euclidean_space) set"
shows "(S ~= {}) <-> (0 : cone hull S)"
using cone_cone_hull[of S] cone_contains_0[of "cone hull S"] cone_hull_empty_iff[of S] by auto
@@ -890,7 +871,6 @@
by (metis assms cone_cone_hull hull_inc mem_cone)
lemma cone_hull_expl:
-fixes S :: "('m::euclidean_space) set"
shows "cone hull S = {c *\<^sub>R x | c x. c>=0 & x : S}" (is "?lhs = ?rhs")
proof-
{ fix x assume "x : ?rhs"
@@ -1365,7 +1345,7 @@
proof-
have fin:"finite {a,b,c}" "finite {b,c}" "finite {c}" by auto
have *:"\<And>x y z ::real. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z"
- "\<And>x y z ::_::euclidean_space. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z" by (auto simp add: field_simps)
+ by (auto simp add: field_simps)
show ?thesis unfolding convex_hull_finite[OF fin(1)] and convex_hull_finite_step[OF fin(2)] and *
unfolding convex_hull_finite_step[OF fin(3)] apply(rule Collect_cong) apply simp apply auto
apply(rule_tac x=va in exI) apply (rule_tac x="u c" in exI) apply simp
@@ -1379,22 +1359,16 @@
subsection {* Relations among closure notions and corresponding hulls. *}
-text {* TODO: Generalize linear algebra concepts defined in @{text
-Euclidean_Space.thy} so that we can generalize these lemmas. *}
-
lemma affine_imp_convex: "affine s \<Longrightarrow> convex s"
unfolding affine_def convex_def by auto
-lemma subspace_imp_convex:
- fixes s :: "(_::euclidean_space) set" shows "subspace s \<Longrightarrow> convex s"
+lemma subspace_imp_convex: "subspace s \<Longrightarrow> convex s"
using subspace_imp_affine affine_imp_convex by auto
-lemma affine_hull_subset_span:
- fixes s :: "(_::euclidean_space) set" shows "(affine hull s) \<subseteq> (span s)"
+lemma affine_hull_subset_span: "(affine hull s) \<subseteq> (span s)"
by (metis hull_minimal span_inc subspace_imp_affine subspace_span)
-lemma convex_hull_subset_span:
- fixes s :: "(_::euclidean_space) set" shows "(convex hull s) \<subseteq> (span s)"
+lemma convex_hull_subset_span: "(convex hull s) \<subseteq> (span s)"
by (metis hull_minimal span_inc subspace_imp_convex subspace_span)
lemma convex_hull_subset_affine_hull: "(convex hull s) \<subseteq> (affine hull s)"
@@ -1402,12 +1376,11 @@
lemma affine_dependent_imp_dependent:
- fixes s :: "(_::euclidean_space) set" shows "affine_dependent s \<Longrightarrow> dependent s"
+ shows "affine_dependent s \<Longrightarrow> dependent s"
unfolding affine_dependent_def dependent_def
using affine_hull_subset_span by auto
lemma dependent_imp_affine_dependent:
- fixes s :: "(_::euclidean_space) set"
assumes "dependent {x - a| x . x \<in> s}" "a \<notin> s"
shows "affine_dependent (insert a s)"
proof-
@@ -1562,7 +1535,6 @@
by (simp add: affine_dependent_def)
lemma affine_independent_sing:
-fixes a :: "'n::euclidean_space"
shows "~(affine_dependent {a})"
by (simp add: affine_dependent_def)
@@ -1600,7 +1572,6 @@
qed
lemma affine_hull_0_dependent:
- fixes S :: "('n::euclidean_space) set"
assumes "0 : affine hull S"
shows "dependent S"
proof-
@@ -1611,7 +1582,6 @@
qed
lemma affine_dependent_imp_dependent2:
- fixes S :: "('n::euclidean_space) set"
assumes "affine_dependent (insert 0 S)"
shows "dependent S"
proof-
@@ -1627,7 +1597,6 @@
qed
lemma affine_dependent_iff_dependent:
- fixes S :: "('n::euclidean_space) set"
assumes "a ~: S"
shows "affine_dependent (insert a S) <-> dependent ((%x. -a + x) ` S)"
proof-
@@ -1638,7 +1607,6 @@
qed
lemma affine_dependent_iff_dependent2:
- fixes S :: "('n::euclidean_space) set"
assumes "a : S"
shows "affine_dependent S <-> dependent ((%x. -a + x) ` (S-{a}))"
proof-
@@ -1647,7 +1615,6 @@
qed
lemma affine_hull_insert_span_gen:
- fixes a :: "_::euclidean_space"
shows "affine hull (insert a s) = (%x. a+x) ` span ((%x. -a+x) ` s)"
proof-
have h1: "{x - a |x. x : s}=((%x. -a+x) ` s)" by auto
@@ -1666,13 +1633,11 @@
qed
lemma affine_hull_span2:
- fixes a :: "_::euclidean_space"
assumes "a : s"
shows "affine hull s = (%x. a+x) ` span ((%x. -a+x) ` (s-{a}))"
using affine_hull_insert_span_gen[of a "s - {a}", unfolded insert_Diff[OF assms]] by auto
lemma affine_hull_span_gen:
- fixes a :: "_::euclidean_space"
assumes "a : affine hull s"
shows "affine hull s = (%x. a+x) ` span ((%x. -a+x) ` s)"
proof-
@@ -1681,7 +1646,7 @@
qed
lemma affine_hull_span_0:
- assumes "(0 :: _::euclidean_space) : affine hull S"
+ assumes "0 : affine hull S"
shows "affine hull S = span S"
using affine_hull_span_gen[of "0" S] assms by auto
@@ -1859,12 +1824,10 @@
qed
lemma aff_dim_affine_hull:
-fixes S :: "('n::euclidean_space) set"
shows "aff_dim (affine hull S)=aff_dim S"
unfolding aff_dim_def using hull_hull[of _ S] by auto
lemma aff_dim_affine_hull2:
-fixes S T :: "('n::euclidean_space) set"
assumes "affine hull S=affine hull T"
shows "aff_dim S=aff_dim T" unfolding aff_dim_def using assms by auto
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Sun Aug 21 19:47:52 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Sun Aug 21 22:56:55 2011 +0200
@@ -3107,7 +3107,7 @@
shows "basis 0 = (1::complex)" and "basis 1 = ii" and "basis (Suc 0) = ii"
unfolding basis_complex_def by auto
-section {* Products Spaces *}
+subsection {* Products Spaces *}
lemma DIM_prod[simp]: "DIM('a \<times> 'b) = DIM('b::euclidean_space) + DIM('a::euclidean_space)"
(* FIXME: why this orientation? Why not "DIM('a) + DIM('b)" ? *)
--- a/src/HOL/Multivariate_Analysis/document/root.tex Sun Aug 21 19:47:52 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/document/root.tex Sun Aug 21 22:56:55 2011 +0200
@@ -18,9 +18,11 @@
\tableofcontents
\begin{center}
- \includegraphics[scale=0.45]{session_graph}
+ \includegraphics[width=\linewidth]{session_graph}
\end{center}
+\newpage
+
\renewcommand{\isamarkupheader}[1]%
{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
--- a/src/HOL/Tools/Function/function_common.ML Sun Aug 21 19:47:52 2011 +0200
+++ b/src/HOL/Tools/Function/function_common.ML Sun Aug 21 22:56:55 2011 +0200
@@ -333,7 +333,7 @@
local
- val option_parser = Parse.group "option"
+ val option_parser = Parse.group (fn () => "option")
((Parse.reserved "sequential" >> K Sequential)
|| ((Parse.reserved "default" |-- Parse.term) >> Default)
|| (Parse.reserved "domintros" >> K DomIntros)
--- a/src/Pure/Isar/args.ML Sun Aug 21 19:47:52 2011 +0200
+++ b/src/Pure/Isar/args.ML Sun Aug 21 22:56:55 2011 +0200
@@ -227,7 +227,7 @@
fun parse_args is_symid =
let
val keyword_symid = token (Parse.keyword_with is_symid);
- fun atom blk = Parse.group "argument"
+ fun atom blk = Parse.group (fn () => "argument")
(ident || keyword_symid || string || alt_string || token Parse.float_number ||
(if blk then token (Parse.$$$ ",") else Scan.fail));
--- a/src/Pure/Isar/outer_syntax.ML Sun Aug 21 19:47:52 2011 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Sun Aug 21 22:56:55 2011 +0200
@@ -62,7 +62,9 @@
local
fun terminate false = Scan.succeed ()
- | terminate true = Parse.group "end of input" (Scan.option Parse.sync -- Parse.semicolon >> K ());
+ | terminate true =
+ Parse.group (fn () => "end of input")
+ (Scan.option Parse.sync -- Parse.semicolon >> K ());
fun body cmd (name, _) =
(case cmd name of
--- a/src/Pure/Isar/parse.ML Sun Aug 21 19:47:52 2011 +0200
+++ b/src/Pure/Isar/parse.ML Sun Aug 21 22:56:55 2011 +0200
@@ -8,7 +8,7 @@
sig
type 'a parser = Token.T list -> 'a * Token.T list
type 'a context_parser = Context.generic * Token.T list -> 'a * (Context.generic * Token.T list)
- val group: string -> (Token.T list -> 'a) -> Token.T list -> 'a
+ val group: (unit -> string) -> (Token.T list -> 'a) -> Token.T list -> 'a
val !!! : (Token.T list -> 'a) -> Token.T list -> 'a
val !!!! : (Token.T list -> 'a) -> Token.T list -> 'a
val triple1: ('a * 'b) * 'c -> 'a * 'b * 'c
@@ -114,17 +114,15 @@
(* group atomic parsers (no cuts!) *)
-fun fail_with s = Scan.fail_with
- (fn [] => (fn () => s ^ " expected (past end-of-file!)")
+fun group s scan = scan || Scan.fail_with
+ (fn [] => (fn () => s () ^ " expected (past end-of-file!)")
| tok :: _ =>
(fn () =>
(case Token.text_of tok of
(txt, "") =>
- s ^ " expected,\nbut " ^ txt ^ Token.pos_of tok ^ " was found"
+ s () ^ " expected,\nbut " ^ txt ^ Token.pos_of tok ^ " was found"
| (txt1, txt2) =>
- s ^ " expected,\nbut " ^ txt1 ^ Token.pos_of tok ^ " was found:\n" ^ txt2)));
-
-fun group s scan = scan || fail_with s;
+ s () ^ " expected,\nbut " ^ txt1 ^ Token.pos_of tok ^ " was found:\n" ^ txt2)));
(* cut *)
@@ -170,7 +168,8 @@
fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.source_of;
fun kind k =
- group (Token.str_of_kind k) (RESET_VALUE (Scan.one (Token.is_kind k) >> Token.content_of));
+ group (fn () => Token.str_of_kind k)
+ (RESET_VALUE (Scan.one (Token.is_kind k) >> Token.content_of));
val command = kind Token.Command;
val keyword = kind Token.Keyword;
@@ -192,10 +191,11 @@
val keyword_ident_or_symbolic = keyword_with Token.ident_or_symbolic;
fun $$$ x =
- group (Token.str_of_kind Token.Keyword ^ " " ^ quote x) (keyword_with (fn y => x = y));
+ group (fn () => Token.str_of_kind Token.Keyword ^ " " ^ quote x)
+ (keyword_with (fn y => x = y));
fun reserved x =
- group ("reserved identifier " ^ quote x)
+ group (fn () => "reserved identifier " ^ quote x)
(RESET_VALUE (Scan.one (Token.ident_with (fn y => x = y)) >> Token.content_of));
val semicolon = $$$ ";";
@@ -208,7 +208,7 @@
val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *;
val real = float_number >> (the o Real.fromString) || int >> Real.fromInt;
-val tag_name = group "tag name" (short_ident || string);
+val tag_name = group (fn () => "tag name") (short_ident || string);
val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);
val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
@@ -240,11 +240,17 @@
(* names and text *)
-val name = group "name declaration" (short_ident || sym_ident || string || number);
+val name = group (fn () => "name declaration") (short_ident || sym_ident || string || number);
+
val binding = position name >> Binding.make;
-val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
-val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
-val path = group "file name/path specification" name >> Path.explode;
+
+val xname = group (fn () => "name reference")
+ (short_ident || long_ident || sym_ident || string || number);
+
+val text = group (fn () => "text")
+ (short_ident || long_ident || sym_ident || string || number || verbatim);
+
+val path = group (fn () => "file name/path specification") name >> Path.explode;
val liberal_name = keyword_ident_or_symbolic || xname;
@@ -254,7 +260,7 @@
(* sorts and arities *)
-val sort = group "sort" (inner_syntax xname);
+val sort = group (fn () => "sort") (inner_syntax xname);
val arity = xname -- ($$$ "::" |-- !!!
(Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
@@ -265,8 +271,9 @@
(* types *)
-val typ_group = group "type"
- (short_ident || long_ident || sym_ident || type_ident || type_var || string || number);
+val typ_group =
+ group (fn () => "type")
+ (short_ident || long_ident || sym_ident || type_ident || type_var || string || number);
val typ = inner_syntax typ_group;
@@ -324,24 +331,24 @@
(* embedded source text *)
-val ML_source = source_position (group "ML source" text);
-val doc_source = source_position (group "document source" text);
+val ML_source = source_position (group (fn () => "ML source") text);
+val doc_source = source_position (group (fn () => "document source") text);
(* terms *)
val tm = short_ident || long_ident || sym_ident || term_var || number || string;
-val term_group = group "term" tm;
-val prop_group = group "proposition" tm;
+val term_group = group (fn () => "term") tm;
+val prop_group = group (fn () => "proposition") tm;
val term = inner_syntax term_group;
val prop = inner_syntax prop_group;
-val type_const = inner_syntax (group "type constructor" xname);
-val const = inner_syntax (group "constant" xname);
+val type_const = inner_syntax (group (fn () => "type constructor") xname);
+val const = inner_syntax (group (fn () => "constant") xname);
-val literal_fact = inner_syntax (group "literal fact" alt_string);
+val literal_fact = inner_syntax (group (fn () => "literal fact") alt_string);
(* patterns *)
--- a/src/Pure/Isar/parse_spec.ML Sun Aug 21 19:47:52 2011 +0200
+++ b/src/Pure/Isar/parse_spec.ML Sun Aug 21 22:56:55 2011 +0200
@@ -136,7 +136,7 @@
val expr0 = plus1_unless locale_keyword expr1;
in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;
-val context_element = Parse.group "context element" loc_element;
+val context_element = Parse.group (fn () => "context element") loc_element;
end;
--- a/src/Pure/Thy/thy_header.ML Sun Aug 21 19:47:52 2011 +0200
+++ b/src/Pure/Thy/thy_header.ML Sun Aug 21 22:56:55 2011 +0200
@@ -29,8 +29,8 @@
(* header args *)
-val file_name = Parse.group "file name" Parse.name;
-val theory_name = Parse.group "theory name" Parse.name;
+val file_name = Parse.group (fn () => "file name") Parse.name;
+val theory_name = Parse.group (fn () => "theory name") Parse.name;
val file =
Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false ||
--- a/src/Pure/Thy/thy_syntax.ML Sun Aug 21 19:47:52 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.ML Sun Aug 21 22:56:55 2011 +0200
@@ -115,15 +115,15 @@
local
-val is_whitespace = Token.is_kind Token.Space orf Token.is_kind Token.Comment;
+val whitespace = Scan.many (not o Token.is_proper);
+val whitespace1 = Scan.many1 (not o Token.is_proper);
-val body =
- Scan.unless (Scan.many is_whitespace -- Scan.ahead (Parse.command || Parse.eof)) Parse.not_eof;
+val body = Scan.unless (whitespace -- Scan.ahead (Parse.command || Parse.eof)) Parse.not_eof;
val span =
Scan.ahead Parse.command -- Parse.not_eof -- Scan.repeat body
>> (fn ((name, c), bs) => Span (Command name, c :: bs)) ||
- Scan.many1 is_whitespace >> (fn toks => Span (Ignored, toks)) ||
+ whitespace1 >> (fn toks => Span (Ignored, toks)) ||
Scan.repeat1 body >> (fn toks => Span (Malformed, toks));
in
--- a/src/Tools/jEdit/src/document_model.scala Sun Aug 21 19:47:52 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Sun Aug 21 22:56:55 2011 +0200
@@ -139,13 +139,13 @@
{
buffer.addBufferListener(buffer_listener)
pending_edits.init()
- buffer.propertiesChanged()
+ Token_Markup.refresh_buffer(buffer)
}
private def deactivate()
{
pending_edits.flush()
buffer.removeBufferListener(buffer_listener)
- buffer.propertiesChanged()
+ Token_Markup.refresh_buffer(buffer)
}
}
--- a/src/Tools/jEdit/src/token_markup.scala Sun Aug 21 19:47:52 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala Sun Aug 21 22:56:55 2011 +0200
@@ -14,9 +14,10 @@
import java.awt.geom.AffineTransform
import org.gjt.sp.util.SyntaxUtilities
-import org.gjt.sp.jedit.Mode
+import org.gjt.sp.jedit.{jEdit, Mode}
import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler,
ParserRuleSet, ModeProvider, XModeHandler, SyntaxStyle}
+import org.gjt.sp.jedit.buffer.JEditBuffer
import javax.swing.text.Segment
@@ -79,10 +80,14 @@
private def bold_style(style: SyntaxStyle): SyntaxStyle =
font_style(style, _.deriveFont(Font.BOLD))
+ private def hidden_color: Color = new Color(255, 255, 255, 0)
+
class Style_Extender extends SyntaxUtilities.StyleExtender
{
- if (Symbol.font_names.length > 2)
- error("Too many user symbol fonts (max 2 permitted): " + Symbol.font_names.mkString(", "))
+ val max_user_fonts = 2
+ if (Symbol.font_names.length > max_user_fonts)
+ error("Too many user symbol fonts (max " + max_user_fonts + " permitted): " +
+ Symbol.font_names.mkString(", "))
override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
{
@@ -93,11 +98,13 @@
new_styles(subscript(i.toByte)) = script_style(style, -1)
new_styles(superscript(i.toByte)) = script_style(style, 1)
new_styles(bold(i.toByte)) = bold_style(style)
+ for (idx <- 0 until max_user_fonts)
+ new_styles(user_font(idx, i.toByte)) = style
for ((family, idx) <- Symbol.font_index)
new_styles(user_font(idx, i.toByte)) = font_style(style, imitate_font(family, _))
}
new_styles(hidden) =
- new SyntaxStyle(Color.white, null,
+ new SyntaxStyle(hidden_color, null,
{ val font = styles(0).getFont
transform_font(new Font(font.getFamily, 0, 1),
AffineTransform.getScaleInstance(1.0, font.getSize.toDouble)) })
@@ -144,7 +151,7 @@
private val isabelle_rules = new ParserRuleSet("isabelle", "MAIN")
- private class Line_Context(val context: Scan.Context)
+ private class Line_Context(val context: Option[Scan.Context])
extends TokenMarker.LineContext(isabelle_rules, null)
{
override def hashCode: Int = context.hashCode
@@ -160,17 +167,17 @@
override def markTokens(context: TokenMarker.LineContext,
handler: TokenHandler, line: Segment): TokenMarker.LineContext =
{
+ val line_ctxt =
+ context match {
+ case c: Line_Context => c.context
+ case _ => Some(Scan.Finished)
+ }
val context1 =
- if (Isabelle.session.is_ready) {
+ if (line_ctxt.isDefined && Isabelle.session.is_ready) {
val syntax = Isabelle.session.current_syntax()
- val ctxt =
- context match {
- case c: Line_Context => c.context
- case _ => Scan.Finished
- }
- val (tokens, ctxt1) = syntax.scan_context(line, ctxt)
- val context1 = new Line_Context(ctxt1)
+ val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
+ val context1 = new Line_Context(Some(ctxt1))
val extended = extended_styles(line)
@@ -196,7 +203,7 @@
context1
}
else {
- val context1 = new Line_Context(Scan.Finished)
+ val context1 = new Line_Context(None)
handler.handleToken(line, JEditToken.NULL, 0, line.count, context1)
handler.handleToken(line, JEditToken.END, line.count, 0, context1)
context1
@@ -210,12 +217,12 @@
/* mode provider */
+ private val isabelle_token_marker = new Token_Markup.Marker
+
class Mode_Provider(orig_provider: ModeProvider) extends ModeProvider
{
for (mode <- orig_provider.getModes) addMode(mode)
- val isabelle_token_marker = new Token_Markup.Marker
-
override def loadMode(mode: Mode, xmh: XModeHandler)
{
super.loadMode(mode, xmh)
@@ -223,5 +230,12 @@
mode.setTokenMarker(isabelle_token_marker)
}
}
+
+ def refresh_buffer(buffer: JEditBuffer)
+ {
+ buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
+ buffer.setTokenMarker(isabelle_token_marker)
+ buffer.propertiesChanged
+ }
}