# HG changeset patch # User haftmann # Date 1313960215 -7200 # Node ID 78c43fb3adb05358f7669ebdc22a24735a821b65 # Parent 36598b3eb20973476bce6c8f3b01ac2ed09333a4# Parent 53f4f82876064122db4c0a004eef97f472284d21 avoid pred/set mixture diff -r 53f4f8287606 -r 78c43fb3adb0 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy --- 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) = (\\ i. 1)" apply(subst euclidean_eq) diff -r 53f4f8287606 -r 78c43fb3adb0 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- 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 (\x. scaleR c x)" + by (simp add: linear_def scaleR_add_right) + +lemma injective_scaleR: "c \ 0 \ inj (\(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 \ 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) \ {a + v| v . v \ span {x - a | x . x \ 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 \ s" shows "affine hull (insert a s) = {a + v | v . v \ span {x - a | x. x \ 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 \ s" shows "affine hull s = {a + v | v. v \ span {x - a | x. x \ 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 \ affine s" +lemma subspace_imp_affine: "subspace s \ 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 *:"\x y z ::real. x + y + z = 1 \ x = 1 - y - z" - "\x y z ::_::euclidean_space. x + y + z = 1 \ 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 \ convex s" unfolding affine_def convex_def by auto -lemma subspace_imp_convex: - fixes s :: "(_::euclidean_space) set" shows "subspace s \ convex s" +lemma subspace_imp_convex: "subspace s \ 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) \ (span s)" +lemma affine_hull_subset_span: "(affine hull s) \ (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) \ (span s)" +lemma convex_hull_subset_span: "(convex hull s) \ (span s)" by (metis hull_minimal span_inc subspace_imp_convex subspace_span) lemma convex_hull_subset_affine_hull: "(convex hull s) \ (affine hull s)" @@ -1402,12 +1376,11 @@ lemma affine_dependent_imp_dependent: - fixes s :: "(_::euclidean_space) set" shows "affine_dependent s \ dependent s" + shows "affine_dependent s \ 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 \ s}" "a \ 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 diff -r 53f4f8287606 -r 78c43fb3adb0 src/HOL/Multivariate_Analysis/Linear_Algebra.thy --- 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 \ 'b) = DIM('b::euclidean_space) + DIM('a::euclidean_space)" (* FIXME: why this orientation? Why not "DIM('a) + DIM('b)" ? *) diff -r 53f4f8287606 -r 78c43fb3adb0 src/HOL/Multivariate_Analysis/document/root.tex --- 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''}} diff -r 53f4f8287606 -r 78c43fb3adb0 src/HOL/Tools/Function/function_common.ML --- 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) diff -r 53f4f8287606 -r 78c43fb3adb0 src/Pure/Isar/args.ML --- 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)); diff -r 53f4f8287606 -r 78c43fb3adb0 src/Pure/Isar/outer_syntax.ML --- 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 diff -r 53f4f8287606 -r 78c43fb3adb0 src/Pure/Isar/parse.ML --- 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 *) diff -r 53f4f8287606 -r 78c43fb3adb0 src/Pure/Isar/parse_spec.ML --- 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; diff -r 53f4f8287606 -r 78c43fb3adb0 src/Pure/Thy/thy_header.ML --- 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 || diff -r 53f4f8287606 -r 78c43fb3adb0 src/Pure/Thy/thy_syntax.ML --- 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 diff -r 53f4f8287606 -r 78c43fb3adb0 src/Tools/jEdit/src/document_model.scala --- 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) } } diff -r 53f4f8287606 -r 78c43fb3adb0 src/Tools/jEdit/src/token_markup.scala --- 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 + } }