--- a/doc-src/manual.bib Wed Sep 08 19:21:46 2010 +0200
+++ b/doc-src/manual.bib Wed Sep 08 19:23:23 2010 +0200
@@ -1372,7 +1372,7 @@
@inproceedings{sutcliffe-2000,
author = "Geoff Sutcliffe",
title = "System Description: {SystemOnTPTP}",
- editor = "J. G. Carbonell and J. Siekmann",
+ editor = "David McAllester",
booktitle = {Automated Deduction --- {CADE}-17 International Conference},
series = "Lecture Notes in Artificial Intelligence",
volume = {1831},
--- a/src/HOL/Auth/Guard/Analz.thy Wed Sep 08 19:21:46 2010 +0200
+++ b/src/HOL/Auth/Guard/Analz.thy Wed Sep 08 19:23:23 2010 +0200
@@ -233,8 +233,7 @@
lemma analz_kparts_analz: "X:analz (kparts H) ==> X:analz H"
by (erule analz.induct, auto dest: kparts_analz)
-lemma analz_kparts_insert: "X:analz (kparts (insert Z H)) ==>
-X:analz (kparts {Z} Un kparts H)"
+lemma analz_kparts_insert: "X:analz (kparts (insert Z H)) ==> X:analz (kparts {Z} Un kparts H)"
by (rule analz_sub, auto)
lemma Nonce_kparts_synth [rule_format]: "Y:synth (analz G)
@@ -247,26 +246,21 @@
apply (drule in_sub, drule_tac X=Y in parts_sub, simp)
by (auto dest: Nonce_kparts_synth)
-lemma Crypt_insert_synth: "[| Crypt K Y:parts (insert X G); X:synth (analz G);
-Nonce n:kparts {Y}; Nonce n ~:analz G |] ==> Crypt K Y:parts G"
-apply (drule parts_insert_substD [where P="%S. Crypt K Y : S"], clarify)
-apply (drule in_sub, drule_tac X="Crypt K Y" in parts_sub, simp, clarsimp)
-apply (ind_cases "Crypt K Y:synth (analz G)")
-by (auto dest: Nonce_kparts_synth)
+lemma Crypt_insert_synth:
+ "[| Crypt K Y:parts (insert X G); X:synth (analz G); Nonce n:kparts {Y}; Nonce n ~:analz G |]
+ ==> Crypt K Y:parts G"
+by (metis Fake_parts_insert_in_Un Nonce_kparts_synth UnE analz_conj_parts synth_simps(5))
+
subsection{*analz is pparts + analz of kparts*}
lemma analz_pparts_kparts: "X:analz H ==> X:pparts H | X:analz (kparts H)"
-apply (erule analz.induct)
-apply (rule_tac X=X in is_MPairE, blast, blast)
-apply (erule disjE, rule_tac X=X in is_MPairE, blast, blast, blast)
-by (erule disjE, rule_tac X=Y in is_MPairE, blast+)
+by (erule analz.induct, auto)
lemma analz_pparts_kparts_eq: "analz H = pparts H Un analz (kparts H)"
by (rule eq, auto dest: analz_pparts_kparts pparts_analz analz_kparts_analz)
lemmas analz_pparts_kparts_substI = analz_pparts_kparts_eq [THEN ssubst]
-lemmas analz_pparts_kparts_substD
-= analz_pparts_kparts_eq [THEN sym, THEN ssubst]
+lemmas analz_pparts_kparts_substD = analz_pparts_kparts_eq [THEN sym, THEN ssubst]
end
--- a/src/HOL/Auth/Guard/Guard_Yahalom.thy Wed Sep 08 19:21:46 2010 +0200
+++ b/src/HOL/Auth/Guard/Guard_Yahalom.thy Wed Sep 08 19:23:23 2010 +0200
@@ -11,7 +11,7 @@
header{*Yahalom Protocol*}
-theory Guard_Yahalom imports Guard_Shared begin
+theory Guard_Yahalom imports "../Shared" Guard_Shared begin
subsection{*messages used in the protocol*}
--- a/src/HOL/Auth/Guard/P1.thy Wed Sep 08 19:21:46 2010 +0200
+++ b/src/HOL/Auth/Guard/P1.thy Wed Sep 08 19:23:23 2010 +0200
@@ -15,7 +15,7 @@
header{*Protocol P1*}
-theory P1 imports Guard_Public List_Msg begin
+theory P1 imports "../Public" Guard_Public List_Msg begin
subsection{*Protocol Definition*}
--- a/src/HOL/Auth/Message.thy Wed Sep 08 19:21:46 2010 +0200
+++ b/src/HOL/Auth/Message.thy Wed Sep 08 19:23:23 2010 +0200
@@ -582,12 +582,13 @@
text{*NO @{text Agent_synth}, as any Agent name can be synthesized.
The same holds for @{term Number}*}
-inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"
-inductive_cases Key_synth [elim!]: "Key K \<in> synth H"
-inductive_cases Hash_synth [elim!]: "Hash X \<in> synth H"
-inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H"
-inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
+inductive_simps synth_simps [iff]:
+ "Nonce n \<in> synth H"
+ "Key K \<in> synth H"
+ "Hash X \<in> synth H"
+ "{|X,Y|} \<in> synth H"
+ "Crypt K X \<in> synth H"
lemma synth_increasing: "H \<subseteq> synth(H)"
by blast
@@ -605,7 +606,7 @@
subsubsection{*Idempotence and transitivity *}
lemma synth_synthD [dest!]: "X\<in> synth (synth H) ==> X\<in> synth H"
-by (erule synth.induct, blast+)
+by (erule synth.induct, auto)
lemma synth_idem: "synth (synth H) = synth H"
by blast
@@ -782,7 +783,7 @@
"X \<notin> synth (analz H)
==> (Hash[X] Y \<in> synth (analz H)) =
(Hash {|X, Y|} \<in> analz H & Y \<in> synth (analz H))"
-by (simp add: HPair_def)
+by (auto simp add: HPair_def)
text{*We do NOT want Crypt... messages broken up in protocols!!*}
--- a/src/HOL/Auth/Shared.thy Wed Sep 08 19:21:46 2010 +0200
+++ b/src/HOL/Auth/Shared.thy Wed Sep 08 19:23:23 2010 +0200
@@ -12,7 +12,7 @@
begin
consts
- shrK :: "agent => key" (*symmetric keys*);
+ shrK :: "agent => key" (*symmetric keys*)
specification (shrK)
inj_shrK: "inj shrK"
@@ -66,7 +66,7 @@
(*Specialized to shared-key model: no @{term invKey}*)
lemma keysFor_parts_insert:
"[| K \<in> keysFor (parts (insert X G)); X \<in> synth (analz H) |]
- ==> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H";
+ ==> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H"
by (force dest: Event.keysFor_parts_insert)
lemma Crypt_imp_keysFor: "Crypt K X \<in> H ==> K \<in> keysFor H"
--- a/src/HOL/IsaMakefile Wed Sep 08 19:21:46 2010 +0200
+++ b/src/HOL/IsaMakefile Wed Sep 08 19:23:23 2010 +0200
@@ -278,7 +278,6 @@
Tools/nat_numeral_simprocs.ML \
Tools/Nitpick/kodkod.ML \
Tools/Nitpick/kodkod_sat.ML \
- Tools/Nitpick/minipick.ML \
Tools/Nitpick/nitpick.ML \
Tools/Nitpick/nitpick_hol.ML \
Tools/Nitpick/nitpick_isar.ML \
@@ -667,11 +666,10 @@
Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \
Nitpick_Examples/Hotel_Nits.thy Nitpick_Examples/Induct_Nits.thy \
Nitpick_Examples/Integer_Nits.thy Nitpick_Examples/Manual_Nits.thy \
- Nitpick_Examples/Mini_Nits.thy Nitpick_Examples/Mono_Nits.thy \
- Nitpick_Examples/Nitpick_Examples.thy Nitpick_Examples/Pattern_Nits.thy \
- Nitpick_Examples/Record_Nits.thy Nitpick_Examples/Refute_Nits.thy \
- Nitpick_Examples/Special_Nits.thy Nitpick_Examples/Tests_Nits.thy \
- Nitpick_Examples/Typedef_Nits.thy
+ Nitpick_Examples/Mono_Nits.thy Nitpick_Examples/Nitpick_Examples.thy \
+ Nitpick_Examples/Pattern_Nits.thy Nitpick_Examples/Record_Nits.thy \
+ Nitpick_Examples/Refute_Nits.thy Nitpick_Examples/Special_Nits.thy \
+ Nitpick_Examples/Tests_Nits.thy Nitpick_Examples/Typedef_Nits.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples
--- a/src/HOL/Nitpick.thy Wed Sep 08 19:21:46 2010 +0200
+++ b/src/HOL/Nitpick.thy Wed Sep 08 19:23:23 2010 +0200
@@ -24,7 +24,6 @@
("Tools/Nitpick/nitpick.ML")
("Tools/Nitpick/nitpick_isar.ML")
("Tools/Nitpick/nitpick_tests.ML")
- ("Tools/Nitpick/minipick.ML")
begin
typedecl bisim_iterator
@@ -237,7 +236,6 @@
use "Tools/Nitpick/nitpick.ML"
use "Tools/Nitpick/nitpick_isar.ML"
use "Tools/Nitpick/nitpick_tests.ML"
-use "Tools/Nitpick/minipick.ML"
setup {* Nitpick_Isar.setup *}
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Wed Sep 08 19:21:46 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Wed Sep 08 19:23:23 2010 +0200
@@ -32,44 +32,6 @@
nitpick [card = 1\<midarrow>12, expect = none]
by auto
-lemma "(split o curry) f = f"
-nitpick [card = 1\<midarrow>12, expect = none]
-by auto
-
-lemma "(curry o split) f = f"
-nitpick [card = 1\<midarrow>12, expect = none]
-by auto
-
-lemma "(split o curry) f = (\<lambda>x. x) f"
-nitpick [card = 1\<midarrow>12, expect = none]
-by auto
-
-lemma "(curry o split) f = (\<lambda>x. x) f"
-nitpick [card = 1\<midarrow>12, expect = none]
-by auto
-
-lemma "((split o curry) f) p = ((\<lambda>x. x) f) p"
-nitpick [card = 1\<midarrow>12, expect = none]
-by auto
-
-lemma "((curry o split) f) x = ((\<lambda>x. x) f) x"
-nitpick [card = 1\<midarrow>12, expect = none]
-by auto
-
-lemma "((curry o split) f) x y = ((\<lambda>x. x) f) x y"
-nitpick [card = 1\<midarrow>12, expect = none]
-by auto
-
-lemma "split o curry = (\<lambda>x. x)"
-nitpick [card = 1\<midarrow>12, expect = none]
-apply (rule ext)+
-by auto
-
-lemma "curry o split = (\<lambda>x. x)"
-nitpick [card = 1\<midarrow>12, expect = none]
-apply (rule ext)+
-by auto
-
lemma "split (\<lambda>x y. f (x, y)) = f"
nitpick [card = 1\<midarrow>12, expect = none]
by auto
@@ -150,31 +112,31 @@
oops
lemma "{a, b} = {b}"
-nitpick [card = 100, expect = genuine]
+nitpick [card = 50, expect = genuine]
oops
lemma "(a\<Colon>'a\<times>'a, a\<Colon>'a\<times>'a) \<in> R"
nitpick [card = 1, expect = genuine]
-nitpick [card = 20, expect = genuine]
+nitpick [card = 10, expect = genuine]
nitpick [card = 5, dont_box, expect = genuine]
oops
lemma "f (g\<Colon>'a\<Rightarrow>'a) = x"
nitpick [card = 3, expect = genuine]
nitpick [card = 3, dont_box, expect = genuine]
-nitpick [card = 10, expect = genuine]
+nitpick [card = 8, expect = genuine]
oops
lemma "f (a, b) = x"
-nitpick [card = 12, expect = genuine]
+nitpick [card = 10, expect = genuine]
oops
lemma "f (a, a) = f (c, d)"
-nitpick [card = 12, expect = genuine]
+nitpick [card = 10, expect = genuine]
oops
lemma "(x\<Colon>'a) = (\<lambda>a. \<lambda>b. \<lambda>c. if c then a else b) x x True"
-nitpick [card = 1\<midarrow>12, expect = none]
+nitpick [card = 1\<midarrow>10, expect = none]
by auto
lemma "\<exists>F. F a b = G a b"
@@ -187,7 +149,7 @@
oops
lemma "(A\<Colon>'a\<times>'a, B\<Colon>'a\<times>'a) \<in> R \<Longrightarrow> (A, B) \<in> R"
-nitpick [card = 20, expect = none]
+nitpick [card = 15, expect = none]
by auto
lemma "(A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R) \<Longrightarrow>
@@ -204,30 +166,30 @@
lemma "x = y"
nitpick [card 'a = 1, expect = none]
nitpick [card 'a = 2, expect = genuine]
-nitpick [card 'a = 200, expect = genuine]
+nitpick [card 'a = 100, expect = genuine]
oops
lemma "\<forall>x. x = y"
nitpick [card 'a = 1, expect = none]
nitpick [card 'a = 2, expect = genuine]
-nitpick [card 'a = 200, expect = genuine]
+nitpick [card 'a = 100, expect = genuine]
oops
lemma "\<forall>x\<Colon>'a \<Rightarrow> bool. x = y"
nitpick [card 'a = 1, expect = genuine]
-nitpick [card 'a = 200, expect = genuine]
+nitpick [card 'a = 100, expect = genuine]
oops
lemma "\<exists>x\<Colon>'a \<Rightarrow> bool. x = y"
-nitpick [card 'a = 1\<midarrow>20, expect = none]
+nitpick [card 'a = 1\<midarrow>15, expect = none]
by auto
lemma "\<exists>x y\<Colon>'a \<Rightarrow> bool. x = y"
-nitpick [card = 1\<midarrow>20, expect = none]
+nitpick [card = 1\<midarrow>15, expect = none]
by auto
lemma "\<forall>x. \<exists>y. f x y = f x (g x)"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<midarrow>4, expect = none]
by auto
lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)"
@@ -241,7 +203,6 @@
lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
f u v w x y z = f u (g u) w (h u w) y (k u w y)"
nitpick [card = 1\<midarrow>2, expect = none]
-nitpick [card = 3, expect = none]
sorry
lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
@@ -288,18 +249,6 @@
nitpick [expect = none]
sorry
-lemma "\<forall>x\<Colon>'a\<times>'b. if (\<exists>y. x = y) then True else False"
-nitpick [expect = none]
-sorry
-
-lemma "(\<not> (\<exists>x. P x)) \<longleftrightarrow> (\<forall>x. \<not> P x)"
-nitpick [expect = none]
-by auto
-
-lemma "(\<not> \<not> (\<exists>x. P x)) \<longleftrightarrow> (\<not> (\<forall>x. \<not> P x))"
-nitpick [expect = none]
-by auto
-
lemma "(\<exists>x\<Colon>'a. \<forall>y. P x y) \<or> (\<exists>x\<Colon>'a \<times> 'a. \<forall>y. P y x)"
nitpick [card 'a = 1, expect = genuine]
nitpick [card 'a = 5, expect = genuine]
@@ -383,10 +332,6 @@
nitpick [card = 20, expect = genuine]
oops
-lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<equiv> x) \<equiv> (\<lambda>y. (x \<equiv> I y))"
-nitpick [expect = none]
-by auto
-
lemma "P x \<equiv> P x"
nitpick [card = 1\<midarrow>10, expect = none]
by auto
@@ -456,14 +401,12 @@
oops
lemma "\<exists>!x. x = undefined"
-nitpick [card = 30, expect = none]
+nitpick [card = 15, expect = none]
by auto
lemma "x = All \<Longrightarrow> False"
nitpick [card = 1, dont_box, expect = genuine]
-nitpick [card = 2, dont_box, expect = genuine]
-nitpick [card = 8, dont_box, expect = genuine]
-nitpick [card = 10, dont_box, expect = unknown]
+nitpick [card = 5, dont_box, expect = genuine]
oops
lemma "\<forall>x. f x y = f x y"
@@ -482,15 +425,9 @@
nitpick [expect = genuine]
oops
-lemma "I = (\<lambda>x. x) \<Longrightarrow> All P = All (\<lambda>x. P (I x))"
-nitpick [expect = none]
-by auto
-
lemma "x = Ex \<Longrightarrow> False"
nitpick [card = 1, dont_box, expect = genuine]
-nitpick [card = 2, dont_box, expect = genuine]
-nitpick [card = 6, dont_box, expect = genuine]
-nitpick [card = 10, dont_box, expect = unknown]
+nitpick [card = 5, dont_box, expect = genuine]
oops
lemma "\<exists>x. f x y = f x y"
@@ -513,10 +450,6 @@
nitpick [expect = genuine]
oops
-lemma "Ex (\<lambda>x. f x y = f y x) = False"
-nitpick [expect = genuine]
-oops
-
lemma "Ex (\<lambda>x. f x y \<noteq> f x y) = False"
nitpick [expect = none]
by auto
@@ -525,11 +458,6 @@
nitpick [expect = none]
by auto
-lemma "I = (\<lambda>x. x) \<Longrightarrow> (op =) = (\<lambda>x. (op= (I x)))"
- "I = (\<lambda>x. x) \<Longrightarrow> (op =) = (\<lambda>x y. x = (I y))"
-nitpick [expect = none]
-by auto
-
lemma "x = y \<Longrightarrow> y = x"
nitpick [expect = none]
by auto
@@ -555,35 +483,10 @@
nitpick [expect = none]
by auto
-lemma "\<not> a \<Longrightarrow> \<not> (a \<and> b)" "\<not> b \<Longrightarrow> \<not> (a \<and> b)"
-nitpick [expect = none]
-by auto
-
-lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<or>) = (\<lambda>x. op \<or> (I x))"
- "I = (\<lambda>x. x) \<Longrightarrow> (op \<or>) = (\<lambda>x y. x \<or> (I y))"
-nitpick [expect = none]
-by auto
-
-lemma "a \<Longrightarrow> a \<or> b" "b \<Longrightarrow> a \<or> b"
-nitpick [expect = none]
-by auto
-
-lemma "\<not> (a \<or> b) \<Longrightarrow> \<not> a" "\<not> (a \<or> b) \<Longrightarrow> \<not> b"
-nitpick [expect = none]
-by auto
-
lemma "(op \<longrightarrow>) = (\<lambda>x. op\<longrightarrow> x)" "(op\<longrightarrow> ) = (\<lambda>x y. x \<longrightarrow> y)"
nitpick [expect = none]
by auto
-lemma "\<not>a \<Longrightarrow> a \<longrightarrow> b" "b \<Longrightarrow> a \<longrightarrow> b"
-nitpick [expect = none]
-by auto
-
-lemma "\<lbrakk>a; \<not> b\<rbrakk> \<Longrightarrow> \<not> (a \<longrightarrow> b)"
-nitpick [expect = none]
-by auto
-
lemma "((if a then b else c) = d) = ((a \<longrightarrow> (b = d)) \<and> (\<not> a \<longrightarrow> (c = d)))"
nitpick [expect = none]
by auto
@@ -592,12 +495,6 @@
nitpick [expect = none]
by auto
-lemma "I = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x. If (I x))"
- "J = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x y. If x (J y))"
- "K = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x y z. If x y (K z))"
-nitpick [expect = none]
-by auto
-
lemma "fst (x, y) = x"
nitpick [expect = none]
by (simp add: fst_def)
@@ -642,10 +539,6 @@
nitpick [expect = none]
by auto
-lemma "I = (\<lambda>x. x) \<Longrightarrow> snd = (\<lambda>x. snd (I x))"
-nitpick [expect = none]
-by auto
-
lemma "fst (x, y) = snd (y, x)"
nitpick [expect = none]
by auto
@@ -662,10 +555,6 @@
nitpick [expect = none]
by auto
-lemma "I = (\<lambda>x. x) \<Longrightarrow> curry Id = (\<lambda>x y. Id (x, I y))"
-nitpick [expect = none]
-by (simp add: curry_def)
-
lemma "{} = (\<lambda>x. False)"
nitpick [expect = none]
by (metis Collect_def empty_def)
@@ -722,10 +611,6 @@
nitpick [expect = none]
by (simp add: mem_def)
-lemma "I = (\<lambda>x. x) \<Longrightarrow> insert = (\<lambda>x. insert (I x))"
-nitpick [expect = none]
-by simp
-
lemma "insert = (\<lambda>x y. insert x (y \<union> y))"
nitpick [expect = none]
by simp
@@ -743,10 +628,6 @@
nitpick [expect = none]
by auto
-lemma "I = (\<lambda>x. x) \<Longrightarrow> rtrancl = (\<lambda>x. rtrancl (I x))"
-nitpick [card = 1\<midarrow>2, expect = none]
-by auto
-
lemma "((x, x), (x, x)) \<in> rtrancl {}"
nitpick [card = 1\<midarrow>5, expect = none]
by auto
@@ -755,42 +636,18 @@
nitpick [card = 1\<midarrow>5, expect = none]
by auto
-lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<union> = (\<lambda>x y. op \<union> x (I y))"
-nitpick [card = 1\<midarrow>5, expect = none]
-by auto
-
lemma "a \<in> A \<Longrightarrow> a \<in> (A \<union> B)" "b \<in> B \<Longrightarrow> b \<in> (A \<union> B)"
nitpick [expect = none]
by auto
-lemma "a \<in> (A \<union> B) \<Longrightarrow> a \<in> A \<or> a \<in> B"
-nitpick [expect = none]
-by auto
-
lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<inter> = (\<lambda>x. op \<inter> (I x))"
nitpick [card = 1\<midarrow>5, expect = none]
by auto
-lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<inter> = (\<lambda>x y. op \<inter> x (I y))"
-nitpick [card = 1\<midarrow>5, expect = none]
-by auto
-
lemma "a \<notin> A \<Longrightarrow> a \<notin> (A \<inter> B)" "b \<notin> B \<Longrightarrow> b \<notin> (A \<inter> B)"
nitpick [card = 1\<midarrow>5, expect = none]
by auto
-lemma "a \<notin> (A \<inter> B) \<Longrightarrow> a \<notin> A \<or> a \<notin> B"
-nitpick [expect = none]
-by auto
-
-lemma "I = (\<lambda>x. x) \<Longrightarrow> op - = (\<lambda>x\<Colon>'a set. op - (I x))"
-nitpick [card = 1\<midarrow>5, expect = none]
-by auto
-
-lemma "I = (\<lambda>x. x) \<Longrightarrow> op - = (\<lambda>x y\<Colon>'a set. op - x (I y))"
-nitpick [card = 1\<midarrow>5, expect = none]
-by auto
-
lemma "x \<in> ((A\<Colon>'a set) - B) \<longleftrightarrow> x \<in> A \<and> x \<notin> B"
nitpick [card = 1\<midarrow>5, expect = none]
by auto
@@ -799,22 +656,10 @@
nitpick [card = 1\<midarrow>5, expect = none]
by auto
-lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subset> = (\<lambda>x y. op \<subset> x (I y))"
-nitpick [card = 1\<midarrow>5, expect = none]
-by auto
-
lemma "A \<subset> B \<Longrightarrow> (\<forall>a \<in> A. a \<in> B) \<and> (\<exists>b \<in> B. b \<notin> A)"
nitpick [card = 1\<midarrow>5, expect = none]
by auto
-lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subseteq> = (\<lambda>x. op \<subseteq> (I x))"
-nitpick [card = 1\<midarrow>5, expect = none]
-by auto
-
-lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subseteq> = (\<lambda>x y. op \<subseteq> x (I y))"
-nitpick [card = 1\<midarrow>5, expect = none]
-by auto
-
lemma "A \<subseteq> B \<Longrightarrow> \<forall>a \<in> A. a \<in> B"
nitpick [card = 1\<midarrow>5, expect = none]
by auto
@@ -843,10 +688,6 @@
nitpick [card 'a = 10, expect = genuine]
oops
-lemma "I = (\<lambda>x. x) \<Longrightarrow> finite = (\<lambda>x. finite (I x))"
-nitpick [card = 1\<midarrow>7, expect = none]
-oops
-
lemma "finite A"
nitpick [expect = none]
oops
--- a/src/HOL/Nitpick_Examples/Nitpick_Examples.thy Wed Sep 08 19:21:46 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Nitpick_Examples.thy Wed Sep 08 19:23:23 2010 +0200
@@ -7,7 +7,7 @@
theory Nitpick_Examples
imports Core_Nits Datatype_Nits Hotel_Nits Induct_Nits Integer_Nits Manual_Nits
- Mini_Nits Mono_Nits Pattern_Nits Record_Nits Refute_Nits Special_Nits
- Tests_Nits Typedef_Nits
+ Mono_Nits Pattern_Nits Record_Nits Refute_Nits Special_Nits Tests_Nits
+ Typedef_Nits
begin
end
--- a/src/HOL/Predicate_Compile_Examples/ROOT.ML Wed Sep 08 19:21:46 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML Wed Sep 08 19:23:23 2010 +0200
@@ -1,3 +1,2 @@
use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples", "Specialisation_Examples", "IMP_1", "IMP_2", "IMP_3", "IMP_4"];
-if getenv "PROLOG_HOME" = "" then () else use_thys ["Code_Prolog_Examples", "Context_Free_Grammar_Example", "Hotel_Example", "Lambda_Example", "List_Examples"];
-setmp_noncritical quick_and_dirty true use_thys ["Reg_Exp_Example"];
+if getenv "PROLOG_HOME" = "" then () else (use_thys ["Code_Prolog_Examples", "Context_Free_Grammar_Example", "Hotel_Example", "Lambda_Example", "List_Examples"]; setmp_noncritical quick_and_dirty true use_thys ["Reg_Exp_Example"])
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Wed Sep 08 19:21:46 2010 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Wed Sep 08 19:23:23 2010 +0200
@@ -71,7 +71,7 @@
[if null markers then "External" else "ExternalV2",
dir ^ dir_sep ^ exec, base ^ ".cnf",
if dev = ToFile then out_file else ""] @ markers @
- (if dev = ToFile then [out_file] else []) @ args
+ (if dev = ToFile then [out_file] else []) @ args
end)
fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =
if incremental andalso mode = Batch then NONE else SOME (name, K ss)
--- a/src/HOL/Tools/Nitpick/minipick.ML Wed Sep 08 19:21:46 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,327 +0,0 @@
-(* Title: HOL/Tools/Nitpick/minipick.ML
- Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009, 2010
-
-Finite model generation for HOL formulas using Kodkod, minimalistic version.
-*)
-
-signature MINIPICK =
-sig
- datatype rep = SRep | RRep
- type styp = Nitpick_Util.styp
-
- val vars_for_bound_var :
- (typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr list
- val rel_expr_for_bound_var :
- (typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr
- val decls_for : rep -> (typ -> int) -> typ list -> typ -> Kodkod.decl list
- val false_atom : Kodkod.rel_expr
- val true_atom : Kodkod.rel_expr
- val formula_from_atom : Kodkod.rel_expr -> Kodkod.formula
- val atom_from_formula : Kodkod.formula -> Kodkod.rel_expr
- val kodkod_problem_from_term :
- Proof.context -> (typ -> int) -> term -> Kodkod.problem
- val solve_any_kodkod_problem : theory -> Kodkod.problem list -> string
-end;
-
-structure Minipick : MINIPICK =
-struct
-
-open Kodkod
-open Nitpick_Util
-open Nitpick_HOL
-open Nitpick_Peephole
-open Nitpick_Kodkod
-
-datatype rep = SRep | RRep
-
-fun check_type ctxt (Type (@{type_name fun}, Ts)) =
- List.app (check_type ctxt) Ts
- | check_type ctxt (Type (@{type_name prod}, Ts)) =
- List.app (check_type ctxt) Ts
- | check_type _ @{typ bool} = ()
- | check_type _ (TFree (_, @{sort "{}"})) = ()
- | check_type _ (TFree (_, @{sort HOL.type})) = ()
- | check_type ctxt T =
- raise NOT_SUPPORTED ("type " ^ quote (Syntax.string_of_typ ctxt T))
-
-fun atom_schema_of SRep card (Type (@{type_name fun}, [T1, T2])) =
- replicate_list (card T1) (atom_schema_of SRep card T2)
- | atom_schema_of RRep card (Type (@{type_name fun}, [T1, @{typ bool}])) =
- atom_schema_of SRep card T1
- | atom_schema_of RRep card (Type (@{type_name fun}, [T1, T2])) =
- atom_schema_of SRep card T1 @ atom_schema_of RRep card T2
- | atom_schema_of _ card (Type (@{type_name prod}, Ts)) =
- maps (atom_schema_of SRep card) Ts
- | atom_schema_of _ card T = [card T]
-val arity_of = length ooo atom_schema_of
-
-fun index_for_bound_var _ [_] 0 = 0
- | index_for_bound_var card (_ :: Ts) 0 =
- index_for_bound_var card Ts 0 + arity_of SRep card (hd Ts)
- | index_for_bound_var card Ts n = index_for_bound_var card (tl Ts) (n - 1)
-fun vars_for_bound_var card R Ts j =
- map (curry Var 1) (index_seq (index_for_bound_var card Ts j)
- (arity_of R card (nth Ts j)))
-val rel_expr_for_bound_var = foldl1 Product oooo vars_for_bound_var
-fun decls_for R card Ts T =
- map2 (curry DeclOne o pair 1)
- (index_seq (index_for_bound_var card (T :: Ts) 0)
- (arity_of R card (nth (T :: Ts) 0)))
- (map (AtomSeq o rpair 0) (atom_schema_of R card T))
-
-val atom_product = foldl1 Product o map Atom
-
-val false_atom = Atom 0
-val true_atom = Atom 1
-
-fun formula_from_atom r = RelEq (r, true_atom)
-fun atom_from_formula f = RelIf (f, true_atom, false_atom)
-
-fun kodkod_formula_from_term ctxt card frees =
- let
- fun R_rep_from_S_rep (Type (@{type_name fun}, [T1, @{typ bool}])) r =
- let
- val jss = atom_schema_of SRep card T1 |> map (rpair 0)
- |> all_combinations
- in
- map2 (fn i => fn js =>
- RelIf (formula_from_atom (Project (r, [Num i])),
- atom_product js, empty_n_ary_rel (length js)))
- (index_seq 0 (length jss)) jss
- |> foldl1 Union
- end
- | R_rep_from_S_rep (Type (@{type_name fun}, [T1, T2])) r =
- let
- val jss = atom_schema_of SRep card T1 |> map (rpair 0)
- |> all_combinations
- val arity2 = arity_of SRep card T2
- in
- map2 (fn i => fn js =>
- Product (atom_product js,
- Project (r, num_seq (i * arity2) arity2)
- |> R_rep_from_S_rep T2))
- (index_seq 0 (length jss)) jss
- |> foldl1 Union
- end
- | R_rep_from_S_rep _ r = r
- fun S_rep_from_R_rep Ts (T as Type (@{type_name fun}, _)) r =
- Comprehension (decls_for SRep card Ts T,
- RelEq (R_rep_from_S_rep T
- (rel_expr_for_bound_var card SRep (T :: Ts) 0), r))
- | S_rep_from_R_rep _ _ r = r
- fun to_F Ts t =
- (case t of
- @{const Not} $ t1 => Not (to_F Ts t1)
- | @{const False} => False
- | @{const True} => True
- | Const (@{const_name All}, _) $ Abs (_, T, t') =>
- All (decls_for SRep card Ts T, to_F (T :: Ts) t')
- | (t0 as Const (@{const_name All}, _)) $ t1 =>
- to_F Ts (t0 $ eta_expand Ts t1 1)
- | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
- Exist (decls_for SRep card Ts T, to_F (T :: Ts) t')
- | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
- to_F Ts (t0 $ eta_expand Ts t1 1)
- | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>
- RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
- | Const (@{const_name ord_class.less_eq},
- Type (@{type_name fun},
- [Type (@{type_name fun}, [_, @{typ bool}]), _]))
- $ t1 $ t2 =>
- Subset (to_R_rep Ts t1, to_R_rep Ts t2)
- | @{const HOL.conj} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
- | @{const HOL.disj} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
- | @{const HOL.implies} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
- | t1 $ t2 => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
- | Free _ => raise SAME ()
- | Term.Var _ => raise SAME ()
- | Bound _ => raise SAME ()
- | Const (s, _) => raise NOT_SUPPORTED ("constant " ^ quote s)
- | _ => raise TERM ("Minipick.kodkod_formula_from_term.to_F", [t]))
- handle SAME () => formula_from_atom (to_R_rep Ts t)
- and to_S_rep Ts t =
- case t of
- Const (@{const_name Pair}, _) $ t1 $ t2 =>
- Product (to_S_rep Ts t1, to_S_rep Ts t2)
- | Const (@{const_name Pair}, _) $ _ => to_S_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name Pair}, _) => to_S_rep Ts (eta_expand Ts t 2)
- | Const (@{const_name fst}, _) $ t1 =>
- let val fst_arity = arity_of SRep card (fastype_of1 (Ts, t)) in
- Project (to_S_rep Ts t1, num_seq 0 fst_arity)
- end
- | Const (@{const_name fst}, _) => to_S_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name snd}, _) $ t1 =>
- let
- val pair_arity = arity_of SRep card (fastype_of1 (Ts, t1))
- val snd_arity = arity_of SRep card (fastype_of1 (Ts, t))
- val fst_arity = pair_arity - snd_arity
- in Project (to_S_rep Ts t1, num_seq fst_arity snd_arity) end
- | Const (@{const_name snd}, _) => to_S_rep Ts (eta_expand Ts t 1)
- | Bound j => rel_expr_for_bound_var card SRep Ts j
- | _ => S_rep_from_R_rep Ts (fastype_of1 (Ts, t)) (to_R_rep Ts t)
- and to_R_rep Ts t =
- (case t of
- @{const Not} => to_R_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name All}, _) => to_R_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name Ex}, _) => to_R_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name HOL.eq}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name HOL.eq}, _) => to_R_rep Ts (eta_expand Ts t 2)
- | Const (@{const_name ord_class.less_eq},
- Type (@{type_name fun},
- [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
- to_R_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name ord_class.less_eq}, _) =>
- to_R_rep Ts (eta_expand Ts t 2)
- | @{const HOL.conj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
- | @{const HOL.conj} => to_R_rep Ts (eta_expand Ts t 2)
- | @{const HOL.disj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
- | @{const HOL.disj} => to_R_rep Ts (eta_expand Ts t 2)
- | @{const HOL.implies} $ _ => to_R_rep Ts (eta_expand Ts t 1)
- | @{const HOL.implies} => to_R_rep Ts (eta_expand Ts t 2)
- | Const (@{const_name bot_class.bot},
- T as Type (@{type_name fun}, [_, @{typ bool}])) =>
- empty_n_ary_rel (arity_of RRep card T)
- | Const (@{const_name insert}, _) $ t1 $ t2 =>
- Union (to_S_rep Ts t1, to_R_rep Ts t2)
- | Const (@{const_name insert}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name insert}, _) => to_R_rep Ts (eta_expand Ts t 2)
- | Const (@{const_name trancl}, _) $ t1 =>
- if arity_of RRep card (fastype_of1 (Ts, t1)) = 2 then
- Closure (to_R_rep Ts t1)
- else
- raise NOT_SUPPORTED "transitive closure for function or pair type"
- | Const (@{const_name trancl}, _) => to_R_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name semilattice_inf_class.inf},
- Type (@{type_name fun},
- [Type (@{type_name fun}, [_, @{typ bool}]), _]))
- $ t1 $ t2 =>
- Intersect (to_R_rep Ts t1, to_R_rep Ts t2)
- | Const (@{const_name semilattice_inf_class.inf}, _) $ _ =>
- to_R_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name semilattice_inf_class.inf}, _) =>
- to_R_rep Ts (eta_expand Ts t 2)
- | Const (@{const_name semilattice_sup_class.sup},
- Type (@{type_name fun},
- [Type (@{type_name fun}, [_, @{typ bool}]), _]))
- $ t1 $ t2 =>
- Union (to_R_rep Ts t1, to_R_rep Ts t2)
- | Const (@{const_name semilattice_sup_class.sup}, _) $ _ =>
- to_R_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name semilattice_sup_class.sup}, _) =>
- to_R_rep Ts (eta_expand Ts t 2)
- | Const (@{const_name minus_class.minus},
- Type (@{type_name fun},
- [Type (@{type_name fun}, [_, @{typ bool}]), _]))
- $ t1 $ t2 =>
- Difference (to_R_rep Ts t1, to_R_rep Ts t2)
- | Const (@{const_name minus_class.minus},
- Type (@{type_name fun},
- [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
- to_R_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name minus_class.minus},
- Type (@{type_name fun},
- [Type (@{type_name fun}, [_, @{typ bool}]), _])) =>
- to_R_rep Ts (eta_expand Ts t 2)
- | Const (@{const_name Pair}, _) $ _ $ _ => raise SAME ()
- | Const (@{const_name Pair}, _) $ _ => raise SAME ()
- | Const (@{const_name Pair}, _) => raise SAME ()
- | Const (@{const_name fst}, _) $ _ => raise SAME ()
- | Const (@{const_name fst}, _) => raise SAME ()
- | Const (@{const_name snd}, _) $ _ => raise SAME ()
- | Const (@{const_name snd}, _) => raise SAME ()
- | Const (_, @{typ bool}) => atom_from_formula (to_F Ts t)
- | Free (x as (_, T)) =>
- Rel (arity_of RRep card T, find_index (curry (op =) x) frees)
- | Term.Var _ => raise NOT_SUPPORTED "schematic variables"
- | Bound _ => raise SAME ()
- | Abs (_, T, t') =>
- (case fastype_of1 (T :: Ts, t') of
- @{typ bool} => Comprehension (decls_for SRep card Ts T,
- to_F (T :: Ts) t')
- | T' => Comprehension (decls_for SRep card Ts T @
- decls_for RRep card (T :: Ts) T',
- Subset (rel_expr_for_bound_var card RRep
- (T' :: T :: Ts) 0,
- to_R_rep (T :: Ts) t')))
- | t1 $ t2 =>
- (case fastype_of1 (Ts, t) of
- @{typ bool} => atom_from_formula (to_F Ts t)
- | T =>
- let val T2 = fastype_of1 (Ts, t2) in
- case arity_of SRep card T2 of
- 1 => Join (to_S_rep Ts t2, to_R_rep Ts t1)
- | arity2 =>
- let val res_arity = arity_of RRep card T in
- Project (Intersect
- (Product (to_S_rep Ts t2,
- atom_schema_of RRep card T
- |> map (AtomSeq o rpair 0) |> foldl1 Product),
- to_R_rep Ts t1),
- num_seq arity2 res_arity)
- end
- end)
- | _ => raise NOT_SUPPORTED ("term " ^
- quote (Syntax.string_of_term ctxt t)))
- handle SAME () => R_rep_from_S_rep (fastype_of1 (Ts, t)) (to_S_rep Ts t)
- in to_F [] end
-
-fun bound_for_free card i (s, T) =
- let val js = atom_schema_of RRep card T in
- ([((length js, i), s)],
- [TupleSet [], atom_schema_of RRep card T |> map (rpair 0)
- |> tuple_set_from_atom_schema])
- end
-
-fun declarative_axiom_for_rel_expr card Ts (Type (@{type_name fun}, [T1, T2]))
- r =
- if body_type T2 = bool_T then
- True
- else
- All (decls_for SRep card Ts T1,
- declarative_axiom_for_rel_expr card (T1 :: Ts) T2
- (List.foldl Join r (vars_for_bound_var card SRep (T1 :: Ts) 0)))
- | declarative_axiom_for_rel_expr _ _ _ r = One r
-fun declarative_axiom_for_free card i (_, T) =
- declarative_axiom_for_rel_expr card [] T (Rel (arity_of RRep card T, i))
-
-fun kodkod_problem_from_term ctxt raw_card t =
- let
- val thy = ProofContext.theory_of ctxt
- fun card (Type (@{type_name fun}, [T1, T2])) =
- reasonable_power (card T2) (card T1)
- | card (Type (@{type_name prod}, [T1, T2])) = card T1 * card T2
- | card @{typ bool} = 2
- | card T = Int.max (1, raw_card T)
- val neg_t = @{const Not} $ Object_Logic.atomize_term thy t
- val _ = fold_types (K o check_type ctxt) neg_t ()
- val frees = Term.add_frees neg_t []
- val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees
- val declarative_axioms =
- map2 (declarative_axiom_for_free card) (index_seq 0 (length frees)) frees
- val formula = kodkod_formula_from_term ctxt card frees neg_t
- |> fold_rev (curry And) declarative_axioms
- val univ_card = univ_card 0 0 0 bounds formula
- in
- {comment = "", settings = [], univ_card = univ_card, tuple_assigns = [],
- bounds = bounds, int_bounds = [], expr_assigns = [], formula = formula}
- end
-
-fun solve_any_kodkod_problem thy problems =
- let
- val {overlord, ...} = Nitpick_Isar.default_params thy []
- val max_threads = 1
- val max_solutions = 1
- in
- case solve_any_problem overlord NONE max_threads max_solutions problems of
- JavaNotInstalled => "unknown"
- | JavaTooOld => "unknown"
- | KodkodiNotInstalled => "unknown"
- | Normal ([], _, _) => "none"
- | Normal _ => "genuine"
- | TimedOut _ => "unknown"
- | Interrupted _ => "unknown"
- | Error (s, _) => error ("Kodkod error: " ^ s)
- end
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Sep 08 19:21:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Sep 08 19:23:23 2010 +0200
@@ -452,8 +452,7 @@
else
()
end
- (* FIXME no threads in user-space *)
- in if blocking then run () else Toplevel.thread true (tap run) |> K () end
+ in if blocking then run () else Future.fork run |> K () end
val setup =
dest_dir_setup
--- a/src/HOL/Tools/try.ML Wed Sep 08 19:21:46 2010 +0200
+++ b/src/HOL/Tools/try.ML Wed Sep 08 19:23:23 2010 +0200
@@ -51,9 +51,9 @@
else "")) I (#goal o Proof.goal)
(apply_named_method_on_first_goal name (Proof.context_of st)) st
-val all_goals_named_methods = ["auto", "safe"]
+val all_goals_named_methods = ["auto"]
val first_goal_named_methods =
- ["simp", "fast", "fastsimp", "force", "best", "blast"]
+ ["simp", "fast", "fastsimp", "force", "best", "blast", "arith"]
val do_methods =
map do_named_method_on_first_goal all_goals_named_methods @
map do_named_method first_goal_named_methods
--- a/src/HOL/Unix/Unix.thy Wed Sep 08 19:21:46 2010 +0200
+++ b/src/HOL/Unix/Unix.thy Wed Sep 08 19:23:23 2010 +0200
@@ -945,7 +945,7 @@
from inv1 inv3 inv4 and user\<^isub>1_not_root
have not_writable: "Writable \<notin> others att"
- by (auto simp add: access_def split: option.splits if_splits)
+ by (auto simp add: access_def split: option.splits)
show ?thesis
proof cases
@@ -1044,8 +1044,7 @@
qed
finally show ?thesis .
qed
- with ys show ?thesis
- by (insert that, auto simp add: update_cons_cons_env)
+ with ys show ?thesis using that by auto
qed
also have "dir(y\<mapsto>file') \<noteq> empty" by simp
ultimately show ?thesis ..
--- a/src/Pure/General/markup.ML Wed Sep 08 19:21:46 2010 +0200
+++ b/src/Pure/General/markup.ML Wed Sep 08 19:23:23 2010 +0200
@@ -58,6 +58,7 @@
val literalN: string val literal: T
val inner_stringN: string val inner_string: T
val inner_commentN: string val inner_comment: T
+ val token_rangeN: string val token_range: T
val sortN: string val sort: T
val typN: string val typ: T
val termN: string val term: T
@@ -119,6 +120,7 @@
val promptN: string val prompt: T
val readyN: string val ready: T
val reportN: string val report: T
+ val badN: string val bad: T
val no_output: output * output
val default_output: T -> output * output
val add_mode: string -> (T -> output * output) -> unit
@@ -239,6 +241,8 @@
val (inner_stringN, inner_string) = markup_elem "inner_string";
val (inner_commentN, inner_comment) = markup_elem "inner_comment";
+val (token_rangeN, token_range) = markup_elem "token_range";
+
val (sortN, sort) = markup_elem "sort";
val (typN, typ) = markup_elem "typ";
val (termN, term) = markup_elem "term";
@@ -345,6 +349,8 @@
val (reportN, report) = markup_elem "report";
+val (badN, bad) = markup_elem "bad";
+
(** print mode operations **)
--- a/src/Pure/General/markup.scala Wed Sep 08 19:21:46 2010 +0200
+++ b/src/Pure/General/markup.scala Wed Sep 08 19:23:23 2010 +0200
@@ -136,6 +136,8 @@
val LITERAL = "literal"
val INNER_COMMENT = "inner_comment"
+ val TOKEN_RANGE = "token_range"
+
val SORT = "sort"
val TYP = "typ"
val TERM = "term"
@@ -247,6 +249,8 @@
val SIGNAL = "signal"
val EXIT = "exit"
+ val BAD = "bad"
+
val Ready = Markup("ready", Nil)
--- a/src/Pure/Isar/proof_context.ML Wed Sep 08 19:21:46 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML Wed Sep 08 19:23:23 2010 +0200
@@ -736,18 +736,22 @@
local
+fun parse_failed ctxt pos msg kind =
+ (Context_Position.report ctxt Markup.bad pos;
+ cat_error msg ("Failed to parse " ^ kind));
+
fun parse_sort ctxt text =
let
val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos)
- handle ERROR msg => cat_error msg "Failed to parse sort";
+ handle ERROR msg => parse_failed ctxt pos msg "sort";
in Type.minimize_sort (tsig_of ctxt) S end;
fun parse_typ ctxt text =
let
val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) (get_sort ctxt) (syms, pos)
- handle ERROR msg => cat_error msg "Failed to parse type";
+ handle ERROR msg => parse_failed ctxt pos msg "type";
in T end;
fun parse_term T ctxt text =
@@ -764,7 +768,7 @@
val t =
Syntax.standard_parse_term check get_sort map_const map_free
ctxt (Type.is_logtype (tsig_of ctxt)) (syn_of ctxt) T' (syms, pos)
- handle ERROR msg => cat_error msg ("Failed to parse " ^ kind);
+ handle ERROR msg => parse_failed ctxt pos msg kind;
in t end;
--- a/src/Pure/PIDE/command.scala Wed Sep 08 19:21:46 2010 +0200
+++ b/src/Pure/PIDE/command.scala Wed Sep 08 19:23:23 2010 +0200
@@ -48,11 +48,11 @@
case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
(this /: msgs)((state, msg) =>
msg match {
- case XML.Elem(Markup(name, atts @ Position.Id_Range(id, range)), args)
- if id == command.id =>
+ case XML.Elem(Markup(name, atts @ Position.Id_Range(id, raw_range)), args)
+ if id == command.id && command.range.contains(command.decode(raw_range)) =>
+ val range = command.decode(raw_range)
val props = Position.purge(atts)
- val info =
- Text.Info[Any](command.decode(range), XML.Elem(Markup(name, props), args))
+ val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
state.add_markup(info)
case _ => System.err.println("Ignored report message: " + msg); state
})
@@ -60,8 +60,8 @@
atts match {
case Markup.Serial(i) =>
val result = XML.Elem(Markup(name, Position.purge(atts)), body)
- (add_result(i, result) /: Isar_Document.reported_positions(command.id, message))(
- (st, range) => st.add_markup(Text.Info(command.decode(range), result)))
+ (add_result(i, result) /: Isar_Document.reported_positions(command, message))(
+ (st, range) => st.add_markup(Text.Info(range, result)))
case _ => System.err.println("Ignored message without serial number: " + message); this
}
}
--- a/src/Pure/PIDE/document.scala Wed Sep 08 19:21:46 2010 +0200
+++ b/src/Pure/PIDE/document.scala Wed Sep 08 19:23:23 2010 +0200
@@ -169,11 +169,11 @@
def lookup_command(id: Command_ID): Option[Command]
def state(command: Command): Command.State
def convert(i: Text.Offset): Text.Offset
- def convert(range: Text.Range): Text.Range = range.map(convert(_))
+ def convert(range: Text.Range): Text.Range
def revert(i: Text.Offset): Text.Offset
- def revert(range: Text.Range): Text.Range = range.map(revert(_))
- def select_markup[A](range: Text.Range)
- (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]]
+ def revert(range: Text.Range): Text.Range
+ def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
+ : Stream[Text.Info[Option[A]]]
}
object State
@@ -304,18 +304,24 @@
def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
- def select_markup[A](range: Text.Range)
- (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] =
+ def convert(range: Text.Range): Text.Range =
+ if (edits.isEmpty) range else range.map(convert(_))
+
+ def revert(range: Text.Range): Text.Range =
+ if (edits.isEmpty) range else range.map(revert(_))
+
+ def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
+ : Stream[Text.Info[Option[A]]] =
{
val former_range = revert(range)
for {
- (command, command_start) <- node.command_range(former_range)
+ (command, command_start) <- node.command_range(former_range).toStream
Text.Info(r0, x) <- state(command).markup.
select((former_range - command_start).restrict(command.range)) {
case Text.Info(r0, info)
if result.isDefinedAt(Text.Info(convert(r0 + command_start), info)) =>
result(Text.Info(convert(r0 + command_start), info))
- } { default }
+ }
val r = convert(r0 + command_start)
if !r.is_singularity
} yield Text.Info(r, x)
--- a/src/Pure/PIDE/isar_document.scala Wed Sep 08 19:21:46 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala Wed Sep 08 19:23:23 2010 +0200
@@ -61,19 +61,27 @@
private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
private val exclude_pos = Set(Markup.LOCATION)
- def reported_positions(command_id: Document.Command_ID, message: XML.Elem): Set[Text.Range] =
+ private def is_state(msg: XML.Tree): Boolean =
+ msg match {
+ case XML.Elem(Markup(Markup.WRITELN, _), List(XML.Elem(Markup(Markup.STATE, _), _))) => true
+ case _ => false
+ }
+
+ def reported_positions(command: Command, message: XML.Elem): Set[Text.Range] =
{
def reported(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
tree match {
- case XML.Elem(Markup(name, Position.Id_Range(id, range)), body)
- if include_pos(name) && id == command_id =>
- body.foldLeft(set + range)(reported)
+ case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body)
+ if include_pos(name) && id == command.id =>
+ val range = command.decode(raw_range).restrict(command.range)
+ body.foldLeft(if (range.is_singularity) set else set + range)(reported)
case XML.Elem(Markup(name, _), body) if !exclude_pos(name) =>
body.foldLeft(set)(reported)
case _ => set
}
val set = reported(Set.empty, message)
- if (set.isEmpty) set ++ Position.Range.unapply(message.markup.properties)
+ if (set.isEmpty && !is_state(message))
+ set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))
else set
}
}
--- a/src/Pure/PIDE/markup_tree.scala Wed Sep 08 19:21:46 2010 +0200
+++ b/src/Pure/PIDE/markup_tree.scala Wed Sep 08 19:23:23 2010 +0200
@@ -43,6 +43,8 @@
}
val empty = new Markup_Tree(Branches.empty)
+
+ type Select[A] = PartialFunction[Text.Info[Any], A]
}
@@ -89,11 +91,13 @@
private def overlapping(range: Text.Range): Stream[(Text.Range, Branches.Entry)] =
Branches.overlapping(range, branches).toStream
- def select[A](root_range: Text.Range)
- (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] =
+ def select[A](root_range: Text.Range)(result: Markup_Tree.Select[A])
+ : Stream[Text.Info[Option[A]]] =
{
- def stream(last: Text.Offset, stack: List[(Text.Info[A], Stream[(Text.Range, Branches.Entry)])])
- : Stream[Text.Info[A]] =
+ def stream(
+ last: Text.Offset,
+ stack: List[(Text.Info[Option[A]], Stream[(Text.Range, Branches.Entry)])])
+ : Stream[Text.Info[Option[A]]] =
{
stack match {
case (parent, (range, (info, tree)) #:: more) :: rest =>
@@ -102,7 +106,7 @@
val start = subrange.start
if (result.isDefinedAt(info)) {
- val next = Text.Info(subrange, result(info))
+ val next = Text.Info[Option[A]](subrange, Some(result(info)))
val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts
else nexts
@@ -117,12 +121,11 @@
case Nil =>
val stop = root_range.stop
- if (last < stop) Stream(Text.Info(Text.Range(last, stop), default))
+ if (last < stop) Stream(Text.Info(Text.Range(last, stop), None))
else Stream.empty
}
}
- stream(root_range.start, List((Text.Info(root_range, default), overlapping(root_range))))
- .iterator
+ stream(root_range.start, List((Text.Info(root_range, None), overlapping(root_range))))
}
def swing_tree(parent: DefaultMutableTreeNode)
--- a/src/Pure/Syntax/lexicon.ML Wed Sep 08 19:21:46 2010 +0200
+++ b/src/Pure/Syntax/lexicon.ML Wed Sep 08 19:23:23 2010 +0200
@@ -66,6 +66,7 @@
val terminals: string list
val is_terminal: string -> bool
val report_token: Proof.context -> token -> unit
+ val report_token_range: Proof.context -> token -> unit
val matching_tokens: token * token -> bool
val valued_token: token -> bool
val predef_term: string -> token option
@@ -188,6 +189,11 @@
fun report_token ctxt (Token (kind, _, (pos, _))) =
Context_Position.report ctxt (token_kind_markup kind) pos;
+fun report_token_range ctxt tok =
+ if is_proper tok
+ then Context_Position.report ctxt Markup.token_range (pos_of_token tok)
+ else ();
+
(* matching_tokens *)
--- a/src/Pure/Syntax/syntax.ML Wed Sep 08 19:21:46 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML Wed Sep 08 19:23:23 2010 +0200
@@ -709,7 +709,8 @@
val _ = List.app (Lexicon.report_token ctxt) toks;
val root' = if root <> "prop" andalso is_logtype root then Syn_Ext.logic else root;
- val pts = Parser.parse ctxt gram root' (filter Lexicon.is_proper toks);
+ val pts = Parser.parse ctxt gram root' (filter Lexicon.is_proper toks)
+ handle ERROR msg => (List.app (Lexicon.report_token_range ctxt) toks; error msg);
val len = length pts;
val limit = Config.get ctxt ambiguity_limit;
--- a/src/Tools/jEdit/dist-template/properties/jedit.props Wed Sep 08 19:21:46 2010 +0200
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props Wed Sep 08 19:23:23 2010 +0200
@@ -177,6 +177,7 @@
end.shortcut=
fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
firstTime=false
+foldPainter=Circle
home.shortcut=
insert-newline-indent.shortcut=
insert-newline.shortcut=ENTER
@@ -203,6 +204,7 @@
view.fontsize=18
view.fracFontMetrics=false
view.gutter.fontsize=12
+view.gutter.selectionAreaWidth=18
view.height=787
view.middleMousePaste=true
view.showToolbar=false
--- a/src/Tools/jEdit/src/jedit/document_model.scala Wed Sep 08 19:21:46 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Wed Sep 08 19:23:23 2010 +0200
@@ -69,87 +69,6 @@
case _ => false
}
}
-
-
- /* mapping to jEdit token types */
- // TODO: as properties or CSS style sheet
-
- val command_style: Map[String, Byte] =
- {
- import Token._
- Map[String, Byte](
- Keyword.THY_END -> KEYWORD2,
- Keyword.THY_SCRIPT -> LABEL,
- Keyword.PRF_SCRIPT -> LABEL,
- Keyword.PRF_ASM -> KEYWORD3,
- Keyword.PRF_ASM_GOAL -> KEYWORD3
- ).withDefaultValue(KEYWORD1)
- }
-
- val token_style: Map[String, Byte] =
- {
- import Token._
- Map[String, Byte](
- // logical entities
- Markup.TCLASS -> NULL,
- Markup.TYCON -> NULL,
- Markup.FIXED_DECL -> FUNCTION,
- Markup.FIXED -> NULL,
- Markup.CONST_DECL -> FUNCTION,
- Markup.CONST -> NULL,
- Markup.FACT_DECL -> FUNCTION,
- Markup.FACT -> NULL,
- Markup.DYNAMIC_FACT -> LABEL,
- Markup.LOCAL_FACT_DECL -> FUNCTION,
- Markup.LOCAL_FACT -> NULL,
- // inner syntax
- Markup.TFREE -> NULL,
- Markup.FREE -> NULL,
- Markup.TVAR -> NULL,
- Markup.SKOLEM -> NULL,
- Markup.BOUND -> NULL,
- Markup.VAR -> NULL,
- Markup.NUM -> DIGIT,
- Markup.FLOAT -> DIGIT,
- Markup.XNUM -> DIGIT,
- Markup.XSTR -> LITERAL4,
- Markup.LITERAL -> OPERATOR,
- Markup.INNER_COMMENT -> COMMENT1,
- Markup.SORT -> NULL,
- Markup.TYP -> NULL,
- Markup.TERM -> NULL,
- Markup.PROP -> NULL,
- Markup.ATTRIBUTE -> NULL,
- Markup.METHOD -> NULL,
- // ML syntax
- Markup.ML_KEYWORD -> KEYWORD1,
- Markup.ML_DELIMITER -> OPERATOR,
- Markup.ML_IDENT -> NULL,
- Markup.ML_TVAR -> NULL,
- Markup.ML_NUMERAL -> DIGIT,
- Markup.ML_CHAR -> LITERAL1,
- Markup.ML_STRING -> LITERAL1,
- Markup.ML_COMMENT -> COMMENT1,
- Markup.ML_MALFORMED -> INVALID,
- // embedded source text
- Markup.ML_SOURCE -> COMMENT3,
- Markup.DOC_SOURCE -> COMMENT3,
- Markup.ANTIQ -> COMMENT4,
- Markup.ML_ANTIQ -> COMMENT4,
- Markup.DOC_ANTIQ -> COMMENT4,
- // outer syntax
- Markup.KEYWORD -> KEYWORD2,
- Markup.OPERATOR -> OPERATOR,
- Markup.COMMAND -> KEYWORD1,
- Markup.IDENT -> NULL,
- Markup.VERBATIM -> COMMENT3,
- Markup.COMMENT -> COMMENT1,
- Markup.CONTROL -> COMMENT3,
- Markup.MALFORMED -> INVALID,
- Markup.STRING -> LITERAL3,
- Markup.ALTSTRING -> LITERAL1
- ).withDefaultValue(NULL)
- }
}
@@ -272,27 +191,18 @@
handler.handleToken(line_segment, style, offset, length, context)
val syntax = session.current_syntax()
- val token_markup: PartialFunction[Text.Info[Any], Byte] =
- {
- case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
- if syntax.keyword_kind(name).isDefined =>
- Document_Model.Token_Markup.command_style(syntax.keyword_kind(name).get)
-
- case Text.Info(_, XML.Elem(Markup(name, _), _))
- if Document_Model.Token_Markup.token_style(name) != Token.NULL =>
- Document_Model.Token_Markup.token_style(name)
- }
+ val tokens = snapshot.select_markup(Text.Range(start, stop))(Isabelle_Markup.tokens(syntax))
var last = start
- for (token <- snapshot.select_markup(Text.Range(start, stop))(token_markup)(Token.NULL)) {
+ for (token <- tokens.iterator) {
val Text.Range(token_start, token_stop) = token.range
if (last < token_start)
handle_token(Token.COMMENT1, last - start, token_start - last)
- handle_token(token.info, token_start - start, token_stop - token_start)
+ handle_token(token.info getOrElse Token.NULL,
+ token_start - start, token_stop - token_start)
last = token_stop
}
- if (last < stop)
- handle_token(Token.COMMENT1, last - start, stop - last)
+ if (last < stop) handle_token(Token.COMMENT1, last - start, stop - last)
handle_token(Token.END, line_segment.count, 0)
handler.setLineContext(context)
--- a/src/Tools/jEdit/src/jedit/document_view.scala Wed Sep 08 19:21:46 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Wed Sep 08 19:23:23 2010 +0200
@@ -13,42 +13,19 @@
import scala.actors.Actor._
import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent, FocusAdapter, FocusEvent}
-import java.awt.{BorderLayout, Graphics, Dimension, Color, Graphics2D}
+import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D}
import javax.swing.{JPanel, ToolTipManager}
import javax.swing.event.{CaretListener, CaretEvent}
-import org.gjt.sp.jedit.OperatingSystem
+import org.gjt.sp.jedit.{jEdit, OperatingSystem}
import org.gjt.sp.jedit.gui.RolloverButton
+import org.gjt.sp.jedit.options.GutterOptionPane
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
import org.gjt.sp.jedit.syntax.SyntaxStyle
object Document_View
{
- /* physical rendering */
-
- def status_color(snapshot: Document.Snapshot, command: Command): Color =
- {
- val state = snapshot.state(command)
- if (snapshot.is_outdated) new Color(240, 240, 240)
- else
- Isar_Document.command_status(state.status) match {
- case Isar_Document.Forked(i) if i > 0 => new Color(255, 228, 225)
- case Isar_Document.Finished => new Color(234, 248, 255)
- case Isar_Document.Failed => new Color(255, 193, 193)
- case Isar_Document.Unprocessed => new Color(255, 228, 225)
- case _ => Color.red
- }
- }
-
- val message_markup: PartialFunction[Text.Info[Any], Color] =
- {
- case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => new Color(220, 220, 220)
- case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => new Color(255, 165, 0)
- case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => new Color(255, 106, 106)
- }
-
-
/* document view of text area */
private val key = new Object
@@ -171,19 +148,17 @@
/* subexpression highlighting */
- private def subexp_range(snapshot: Document.Snapshot, x: Int, y: Int): Option[Text.Range] =
+ private def subexp_range(snapshot: Document.Snapshot, x: Int, y: Int)
+ : Option[(Text.Range, Color)] =
{
- val subexp_markup: PartialFunction[Text.Info[Any], Option[Text.Range]] =
- {
- case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), _)) =>
- Some(snapshot.convert(range))
+ val offset = text_area.xyToOffset(x, y)
+ snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.subexp) match {
+ case Text.Info(_, Some((range, color))) #:: _ => Some((snapshot.convert(range), color))
+ case _ => None
}
- val offset = text_area.xyToOffset(x, y)
- val markup = snapshot.select_markup(Text.Range(offset, offset + 1))(subexp_markup)(None)
- if (markup.hasNext) markup.next.info else None
}
- private var highlight_range: Option[Text.Range] = None
+ private var highlight_range: Option[(Text.Range, Color)] = None
private val focus_listener = new FocusAdapter {
override def focusLost(e: FocusEvent) { highlight_range = None }
@@ -195,10 +170,10 @@
if (!model.buffer.isLoaded) highlight_range = None
else
Isabelle.swing_buffer_lock(model.buffer) {
- highlight_range.map(invalidate_line_range(_))
+ highlight_range map { case (range, _) => invalidate_line_range(range) }
highlight_range =
if (control) subexp_range(model.snapshot(), e.getX(), e.getY()) else None
- highlight_range.map(invalidate_line_range(_))
+ highlight_range map { case (range, _) => invalidate_line_range(range) }
}
}
}
@@ -217,53 +192,70 @@
val saved_color = gfx.getColor
val ascent = text_area.getPainter.getFontMetrics.getAscent
- try {
- for (i <- 0 until physical_lines.length) {
- if (physical_lines(i) != -1) {
- val line_range = proper_line_range(start(i), end(i))
+ for (i <- 0 until physical_lines.length) {
+ if (physical_lines(i) != -1) {
+ val line_range = proper_line_range(start(i), end(i))
- // background color
- val cmds = snapshot.node.command_range(snapshot.revert(line_range))
- for {
- (command, command_start) <- cmds if !command.is_ignored
- val range = line_range.restrict(snapshot.convert(command.range + command_start))
- r <- Isabelle.gfx_range(text_area, range)
- } {
- gfx.setColor(Document_View.status_color(snapshot, command))
- gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
- }
+ // background color: status
+ val cmds = snapshot.node.command_range(snapshot.revert(line_range))
+ for {
+ (command, command_start) <- cmds if !command.is_ignored
+ val range = line_range.restrict(snapshot.convert(command.range + command_start))
+ r <- Isabelle.gfx_range(text_area, range)
+ color <- Isabelle_Markup.status_color(snapshot, command)
+ } {
+ gfx.setColor(color)
+ gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
+ }
+
+ // background color: markup
+ for {
+ Text.Info(range, Some(color)) <-
+ snapshot.select_markup(line_range)(Isabelle_Markup.background).iterator
+ r <- Isabelle.gfx_range(text_area, range)
+ } {
+ gfx.setColor(color)
+ gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
+ }
- // subexpression highlighting -- potentially from other snapshot
- if (highlight_range.isDefined) {
- if (line_range.overlaps(highlight_range.get)) {
- Isabelle.gfx_range(text_area, line_range.restrict(highlight_range.get)) match {
- case None =>
- case Some(r) =>
- gfx.setColor(Color.black)
- gfx.drawRect(r.x, y + i * line_height, r.length, line_height - 1)
- }
+ // sub-expression highlighting -- potentially from other snapshot
+ highlight_range match {
+ case Some((range, color)) if line_range.overlaps(range) =>
+ Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
+ case None =>
+ case Some(r) =>
+ gfx.setColor(color)
+ gfx.drawRect(r.x, y + i * line_height, r.length, line_height - 1)
}
- }
+ case _ =>
+ }
- // squiggly underline
- for {
- Text.Info(range, color) <-
- snapshot.select_markup(line_range)(Document_View.message_markup)(null)
- if color != null
- r <- Isabelle.gfx_range(text_area, range)
- } {
- gfx.setColor(color)
- val x0 = (r.x / 2) * 2
- val y0 = r.y + ascent + 1
- for (x1 <- Range(x0, x0 + r.length, 2)) {
- val y1 = if (x1 % 4 < 2) y0 else y0 + 1
- gfx.drawLine(x1, y1, x1 + 1, y1)
- }
+ // boxed text
+ for {
+ Text.Info(range, Some(color)) <-
+ snapshot.select_markup(line_range)(Isabelle_Markup.box).iterator
+ r <- Isabelle.gfx_range(text_area, range)
+ } {
+ gfx.setColor(color)
+ gfx.drawRect(r.x + 1, y + i * line_height + 1, r.length - 2, line_height - 3)
+ }
+
+ // squiggly underline
+ for {
+ Text.Info(range, Some(color)) <-
+ snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
+ r <- Isabelle.gfx_range(text_area, range)
+ } {
+ gfx.setColor(color)
+ val x0 = (r.x / 2) * 2
+ val y0 = r.y + ascent + 1
+ for (x1 <- Range(x0, x0 + r.length, 2)) {
+ val y1 = if (x1 % 4 < 2) y0 else y0 + 1
+ gfx.drawLine(x1, y1, x1 + 1, y1)
}
}
}
}
- finally { gfx.setColor(saved_color) }
}
}
@@ -272,12 +264,52 @@
Isabelle.swing_buffer_lock(model.buffer) {
val snapshot = model.snapshot()
val offset = text_area.xyToOffset(x, y)
- val markup =
- snapshot.select_markup(Text.Range(offset, offset + 1)) {
- case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
- Isabelle.tooltip(Pretty.string_of(List(Pretty.block(body)), margin = 40))
- } { null }
- if (markup.hasNext) markup.next.info else null
+ snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match
+ {
+ case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
+ case _ => null
+ }
+ }
+ }
+ }
+
+
+ /* gutter_extension */
+
+ private val gutter_extension = new TextAreaExtension
+ {
+ override def paintScreenLineRange(gfx: Graphics2D,
+ first_line: Int, last_line: Int, physical_lines: Array[Int],
+ start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+ {
+ val gutter = text_area.getGutter
+ val width = GutterOptionPane.getSelectionAreaWidth
+ val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
+ val FOLD_MARKER_SIZE = 12
+
+ if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
+ Isabelle.swing_buffer_lock(model.buffer) {
+ val snapshot = model.snapshot()
+ for (i <- 0 until physical_lines.length) {
+ if (physical_lines(i) != -1) {
+ val line_range = proper_line_range(start(i), end(i))
+
+ // gutter icons
+ val icons =
+ (for (Text.Info(_, Some(icon)) <-
+ snapshot.select_markup(line_range)(Isabelle_Markup.gutter_message).iterator)
+ yield icon).toList.sortWith(_ >= _)
+ icons match {
+ case icon :: _ =>
+ val icn = icon.icon
+ val x0 = (FOLD_MARKER_SIZE + width - border_width - icn.getIconWidth) max 10
+ val y0 = y + i * line_height + (((line_height - icn.getIconHeight) / 2) max 0)
+ icn.paintIcon(gutter, gfx, x0, y0)
+ case Nil =>
+ }
+ }
+ }
+ }
}
}
}
@@ -328,13 +360,6 @@
super.removeNotify
}
- override def getToolTipText(event: MouseEvent): String =
- {
- val line = y_to_line(event.getY())
- if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>"
- else ""
- }
-
override def paintComponent(gfx: Graphics)
{
super.paintComponent(gfx)
@@ -342,18 +367,18 @@
val buffer = model.buffer
Isabelle.buffer_lock(buffer) {
val snapshot = model.snapshot()
- val saved_color = gfx.getColor // FIXME needed!?
- try {
- for ((command, start) <- snapshot.node.command_starts if !command.is_ignored) {
- val line1 = buffer.getLineOfOffset(snapshot.convert(start))
- val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
- val y = line_to_y(line1)
- val height = HEIGHT * (line2 - line1)
- gfx.setColor(Document_View.status_color(snapshot, command))
- gfx.fillRect(0, y, getWidth - 1, height)
- }
+ for {
+ (command, start) <- snapshot.node.command_starts
+ if !command.is_ignored
+ val line1 = buffer.getLineOfOffset(snapshot.convert(start))
+ val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
+ val y = line_to_y(line1)
+ val height = HEIGHT * (line2 - line1)
+ color <- Isabelle_Markup.overview_color(snapshot, command)
+ } {
+ gfx.setColor(color)
+ gfx.fillRect(0, y, getWidth - 1, height)
}
- finally { gfx.setColor(saved_color) }
}
}
@@ -371,6 +396,7 @@
{
text_area.getPainter.
addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
+ text_area.getGutter.addExtension(gutter_extension)
text_area.addFocusListener(focus_listener)
text_area.getPainter.addMouseMotionListener(mouse_motion_listener)
text_area.addCaretListener(caret_listener)
@@ -385,6 +411,7 @@
text_area.getPainter.removeMouseMotionListener(mouse_motion_listener)
text_area.removeCaretListener(caret_listener)
text_area.removeLeftOfScrollBar(overview)
+ text_area.getGutter.removeExtension(gutter_extension)
text_area.getPainter.removeExtension(text_area_extension)
}
}
\ No newline at end of file
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Wed Sep 08 19:21:46 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Wed Sep 08 19:23:23 2010 +0200
@@ -72,9 +72,11 @@
case _ => null
}
}
- } { null }
- if (markup.hasNext) markup.next.info else null
-
+ }
+ markup match {
+ case Text.Info(_, Some(link)) #:: _ => link
+ case _ => null
+ }
case None => null
}
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala Wed Sep 08 19:23:23 2010 +0200
@@ -0,0 +1,198 @@
+/* Title: Tools/jEdit/src/jedit/isabelle_markup.scala
+ Author: Makarius
+
+Isabelle specific physical rendering and markup selection.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.Color
+
+import org.gjt.sp.jedit.GUIUtilities
+import org.gjt.sp.jedit.syntax.Token
+
+
+object Isabelle_Markup
+{
+ /* physical rendering */
+
+ val outdated_color = new Color(240, 240, 240)
+ val unfinished_color = new Color(255, 228, 225)
+
+ val regular_color = new Color(192, 192, 192)
+ val warning_color = new Color(255, 168, 0)
+ val error_color = new Color(255, 80, 80)
+ val bad_color = new Color(255, 204, 153, 100)
+
+ class Icon(val priority: Int, val icon: javax.swing.Icon)
+ {
+ def >= (that: Icon): Boolean = this.priority >= that.priority
+ }
+ val warning_icon = new Icon(1, GUIUtilities.loadIcon("16x16/status/dialog-warning.png"))
+ val error_icon = new Icon(2, GUIUtilities.loadIcon("16x16/status/dialog-error.png"))
+
+
+ /* command status */
+
+ def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
+ {
+ val state = snapshot.state(command)
+ if (snapshot.is_outdated) Some(outdated_color)
+ else
+ Isar_Document.command_status(state.status) match {
+ case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
+ case Isar_Document.Unprocessed => Some(unfinished_color)
+ case _ => None
+ }
+ }
+
+ def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
+ {
+ val state = snapshot.state(command)
+ if (snapshot.is_outdated) None
+ else
+ Isar_Document.command_status(state.status) match {
+ case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
+ case Isar_Document.Unprocessed => Some(unfinished_color)
+ case Isar_Document.Failed => Some(error_color)
+ case _ => None
+ }
+ }
+
+
+ /* markup selectors */
+
+ private val subexp_include =
+ Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING)
+
+ val subexp: Markup_Tree.Select[(Text.Range, Color)] =
+ {
+ case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
+ (range, Color.black)
+ }
+
+ val message: Markup_Tree.Select[Color] =
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
+ case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
+ case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
+ }
+
+ val gutter_message: Markup_Tree.Select[Icon] =
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_icon
+ case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
+ }
+
+ val background: Markup_Tree.Select[Color] =
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
+ }
+
+ val box: Markup_Tree.Select[Color] =
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => regular_color
+ }
+
+ val tooltip: Markup_Tree.Select[String] =
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
+ Pretty.string_of(List(Pretty.block(body)), margin = 40)
+ case Text.Info(_, XML.Elem(Markup(Markup.SORT, _), _)) => "sort"
+ case Text.Info(_, XML.Elem(Markup(Markup.TYP, _), _)) => "type"
+ case Text.Info(_, XML.Elem(Markup(Markup.TERM, _), _)) => "term"
+ case Text.Info(_, XML.Elem(Markup(Markup.PROP, _), _)) => "proposition"
+ }
+
+
+ /* token markup -- text styles */
+
+ private val command_style: Map[String, Byte] =
+ {
+ import Token._
+ Map[String, Byte](
+ Keyword.THY_END -> KEYWORD2,
+ Keyword.THY_SCRIPT -> LABEL,
+ Keyword.PRF_SCRIPT -> LABEL,
+ Keyword.PRF_ASM -> KEYWORD3,
+ Keyword.PRF_ASM_GOAL -> KEYWORD3
+ ).withDefaultValue(KEYWORD1)
+ }
+
+ private val token_style: Map[String, Byte] =
+ {
+ import Token._
+ Map[String, Byte](
+ // logical entities
+ Markup.TCLASS -> NULL,
+ Markup.TYCON -> NULL,
+ Markup.FIXED_DECL -> FUNCTION,
+ Markup.FIXED -> NULL,
+ Markup.CONST_DECL -> FUNCTION,
+ Markup.CONST -> NULL,
+ Markup.FACT_DECL -> FUNCTION,
+ Markup.FACT -> NULL,
+ Markup.DYNAMIC_FACT -> LABEL,
+ Markup.LOCAL_FACT_DECL -> FUNCTION,
+ Markup.LOCAL_FACT -> NULL,
+ // inner syntax
+ Markup.TFREE -> NULL,
+ Markup.FREE -> NULL,
+ Markup.TVAR -> NULL,
+ Markup.SKOLEM -> NULL,
+ Markup.BOUND -> NULL,
+ Markup.VAR -> NULL,
+ Markup.NUM -> DIGIT,
+ Markup.FLOAT -> DIGIT,
+ Markup.XNUM -> DIGIT,
+ Markup.XSTR -> LITERAL4,
+ Markup.LITERAL -> OPERATOR,
+ Markup.INNER_COMMENT -> COMMENT1,
+ Markup.SORT -> NULL,
+ Markup.TYP -> NULL,
+ Markup.TERM -> NULL,
+ Markup.PROP -> NULL,
+ Markup.ATTRIBUTE -> NULL,
+ Markup.METHOD -> NULL,
+ // ML syntax
+ Markup.ML_KEYWORD -> KEYWORD1,
+ Markup.ML_DELIMITER -> OPERATOR,
+ Markup.ML_IDENT -> NULL,
+ Markup.ML_TVAR -> NULL,
+ Markup.ML_NUMERAL -> DIGIT,
+ Markup.ML_CHAR -> LITERAL1,
+ Markup.ML_STRING -> LITERAL1,
+ Markup.ML_COMMENT -> COMMENT1,
+ Markup.ML_MALFORMED -> INVALID,
+ // embedded source text
+ Markup.ML_SOURCE -> COMMENT3,
+ Markup.DOC_SOURCE -> COMMENT3,
+ Markup.ANTIQ -> COMMENT4,
+ Markup.ML_ANTIQ -> COMMENT4,
+ Markup.DOC_ANTIQ -> COMMENT4,
+ // outer syntax
+ Markup.KEYWORD -> KEYWORD2,
+ Markup.OPERATOR -> OPERATOR,
+ Markup.COMMAND -> KEYWORD1,
+ Markup.IDENT -> NULL,
+ Markup.VERBATIM -> COMMENT3,
+ Markup.COMMENT -> COMMENT1,
+ Markup.CONTROL -> COMMENT3,
+ Markup.MALFORMED -> INVALID,
+ Markup.STRING -> LITERAL3,
+ Markup.ALTSTRING -> LITERAL1
+ ).withDefaultValue(NULL)
+ }
+
+ def tokens(syntax: Outer_Syntax): Markup_Tree.Select[Byte] =
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
+ if syntax.keyword_kind(name).isDefined => command_style(syntax.keyword_kind(name).get)
+
+ case Text.Info(_, XML.Elem(Markup(name, _), _))
+ if token_style(name) != Token.NULL => token_style(name)
+ }
+}
--- a/src/Tools/jEdit/src/jedit/plugin.scala Wed Sep 08 19:21:46 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala Wed Sep 08 19:23:23 2010 +0200
@@ -286,10 +286,9 @@
Isabelle.setup_tooltips()
}
- override def stop()
+ override def stop() // FIXME fragile
{
Isabelle.session.stop() // FIXME dialog!?
Isabelle.session = null
- Isabelle.system = null
}
}