# HG changeset patch # User haftmann # Date 1283966603 -7200 # Node ID 3a15ee47c6106f48a2dd883ff7604ba9dfc0f2f9 # Parent 5a3bd2b7d0eec16525b3b86d257a92183d1525a9# Parent 9e58f0499f57f8cfd73ccaf46cbe533202fceb1d merged diff -r 9e58f0499f57 -r 3a15ee47c610 doc-src/manual.bib --- 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}, diff -r 9e58f0499f57 -r 3a15ee47c610 src/HOL/Auth/Guard/Analz.thy --- 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 diff -r 9e58f0499f57 -r 3a15ee47c610 src/HOL/Auth/Guard/Guard_Yahalom.thy --- 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*} diff -r 9e58f0499f57 -r 3a15ee47c610 src/HOL/Auth/Guard/P1.thy --- 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*} diff -r 9e58f0499f57 -r 3a15ee47c610 src/HOL/Auth/Message.thy --- 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 \ synth H" -inductive_cases Key_synth [elim!]: "Key K \ synth H" -inductive_cases Hash_synth [elim!]: "Hash X \ synth H" -inductive_cases MPair_synth [elim!]: "{|X,Y|} \ synth H" -inductive_cases Crypt_synth [elim!]: "Crypt K X \ synth H" +inductive_simps synth_simps [iff]: + "Nonce n \ synth H" + "Key K \ synth H" + "Hash X \ synth H" + "{|X,Y|} \ synth H" + "Crypt K X \ synth H" lemma synth_increasing: "H \ synth(H)" by blast @@ -605,7 +606,7 @@ subsubsection{*Idempotence and transitivity *} lemma synth_synthD [dest!]: "X\ synth (synth H) ==> X\ 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 \ synth (analz H) ==> (Hash[X] Y \ synth (analz H)) = (Hash {|X, Y|} \ analz H & Y \ 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!!*} diff -r 9e58f0499f57 -r 3a15ee47c610 src/HOL/Auth/Shared.thy --- 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 \ keysFor (parts (insert X G)); X \ synth (analz H) |] - ==> K \ keysFor (parts (G \ H)) | Key K \ parts H"; + ==> K \ keysFor (parts (G \ H)) | Key K \ parts H" by (force dest: Event.keysFor_parts_insert) lemma Crypt_imp_keysFor: "Crypt K X \ H ==> K \ keysFor H" diff -r 9e58f0499f57 -r 3a15ee47c610 src/HOL/IsaMakefile --- 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 diff -r 9e58f0499f57 -r 3a15ee47c610 src/HOL/Nitpick.thy --- 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 *} diff -r 9e58f0499f57 -r 3a15ee47c610 src/HOL/Nitpick_Examples/Core_Nits.thy --- 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\12, expect = none] by auto -lemma "(split o curry) f = f" -nitpick [card = 1\12, expect = none] -by auto - -lemma "(curry o split) f = f" -nitpick [card = 1\12, expect = none] -by auto - -lemma "(split o curry) f = (\x. x) f" -nitpick [card = 1\12, expect = none] -by auto - -lemma "(curry o split) f = (\x. x) f" -nitpick [card = 1\12, expect = none] -by auto - -lemma "((split o curry) f) p = ((\x. x) f) p" -nitpick [card = 1\12, expect = none] -by auto - -lemma "((curry o split) f) x = ((\x. x) f) x" -nitpick [card = 1\12, expect = none] -by auto - -lemma "((curry o split) f) x y = ((\x. x) f) x y" -nitpick [card = 1\12, expect = none] -by auto - -lemma "split o curry = (\x. x)" -nitpick [card = 1\12, expect = none] -apply (rule ext)+ -by auto - -lemma "curry o split = (\x. x)" -nitpick [card = 1\12, expect = none] -apply (rule ext)+ -by auto - lemma "split (\x y. f (x, y)) = f" nitpick [card = 1\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\'a\'a, a\'a\'a) \ 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\'a\'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\'a) = (\a. \b. \c. if c then a else b) x x True" -nitpick [card = 1\12, expect = none] +nitpick [card = 1\10, expect = none] by auto lemma "\F. F a b = G a b" @@ -187,7 +149,7 @@ oops lemma "(A\'a\'a, B\'a\'a) \ R \ (A, B) \ R" -nitpick [card = 20, expect = none] +nitpick [card = 15, expect = none] by auto lemma "(A, B) \ R \ (\C. (A, C) \ R \ (C, B) \ R) \ @@ -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 "\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 "\x\'a \ bool. x = y" nitpick [card 'a = 1, expect = genuine] -nitpick [card 'a = 200, expect = genuine] +nitpick [card 'a = 100, expect = genuine] oops lemma "\x\'a \ bool. x = y" -nitpick [card 'a = 1\20, expect = none] +nitpick [card 'a = 1\15, expect = none] by auto lemma "\x y\'a \ bool. x = y" -nitpick [card = 1\20, expect = none] +nitpick [card = 1\15, expect = none] by auto lemma "\x. \y. f x y = f x (g x)" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\4, expect = none] by auto lemma "\u. \v. \w. \x. f u v w x = f u (g u) w (h u w)" @@ -241,7 +203,6 @@ lemma "\u. \v. \w. \x. \y. \z. f u v w x y z = f u (g u) w (h u w) y (k u w y)" nitpick [card = 1\2, expect = none] -nitpick [card = 3, expect = none] sorry lemma "\u. \v. \w. \x. \y. \z. @@ -288,18 +249,6 @@ nitpick [expect = none] sorry -lemma "\x\'a\'b. if (\y. x = y) then True else False" -nitpick [expect = none] -sorry - -lemma "(\ (\x. P x)) \ (\x. \ P x)" -nitpick [expect = none] -by auto - -lemma "(\ \ (\x. P x)) \ (\ (\x. \ P x))" -nitpick [expect = none] -by auto - lemma "(\x\'a. \y. P x y) \ (\x\'a \ 'a. \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 = (\x. x) \ (op \ x) \ (\y. (x \ I y))" -nitpick [expect = none] -by auto - lemma "P x \ P x" nitpick [card = 1\10, expect = none] by auto @@ -456,14 +401,12 @@ oops lemma "\!x. x = undefined" -nitpick [card = 30, expect = none] +nitpick [card = 15, expect = none] by auto lemma "x = All \ 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 "\x. f x y = f x y" @@ -482,15 +425,9 @@ nitpick [expect = genuine] oops -lemma "I = (\x. x) \ All P = All (\x. P (I x))" -nitpick [expect = none] -by auto - lemma "x = Ex \ 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 "\x. f x y = f x y" @@ -513,10 +450,6 @@ nitpick [expect = genuine] oops -lemma "Ex (\x. f x y = f y x) = False" -nitpick [expect = genuine] -oops - lemma "Ex (\x. f x y \ f x y) = False" nitpick [expect = none] by auto @@ -525,11 +458,6 @@ nitpick [expect = none] by auto -lemma "I = (\x. x) \ (op =) = (\x. (op= (I x)))" - "I = (\x. x) \ (op =) = (\x y. x = (I y))" -nitpick [expect = none] -by auto - lemma "x = y \ y = x" nitpick [expect = none] by auto @@ -555,35 +483,10 @@ nitpick [expect = none] by auto -lemma "\ a \ \ (a \ b)" "\ b \ \ (a \ b)" -nitpick [expect = none] -by auto - -lemma "I = (\x. x) \ (op \) = (\x. op \ (I x))" - "I = (\x. x) \ (op \) = (\x y. x \ (I y))" -nitpick [expect = none] -by auto - -lemma "a \ a \ b" "b \ a \ b" -nitpick [expect = none] -by auto - -lemma "\ (a \ b) \ \ a" "\ (a \ b) \ \ b" -nitpick [expect = none] -by auto - lemma "(op \) = (\x. op\ x)" "(op\ ) = (\x y. x \ y)" nitpick [expect = none] by auto -lemma "\a \ a \ b" "b \ a \ b" -nitpick [expect = none] -by auto - -lemma "\a; \ b\ \ \ (a \ b)" -nitpick [expect = none] -by auto - lemma "((if a then b else c) = d) = ((a \ (b = d)) \ (\ a \ (c = d)))" nitpick [expect = none] by auto @@ -592,12 +495,6 @@ nitpick [expect = none] by auto -lemma "I = (\x. x) \ If = (\x. If (I x))" - "J = (\x. x) \ If = (\x y. If x (J y))" - "K = (\x. x) \ If = (\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 = (\x. x) \ snd = (\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 = (\x. x) \ curry Id = (\x y. Id (x, I y))" -nitpick [expect = none] -by (simp add: curry_def) - lemma "{} = (\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 = (\x. x) \ insert = (\x. insert (I x))" -nitpick [expect = none] -by simp - lemma "insert = (\x y. insert x (y \ y))" nitpick [expect = none] by simp @@ -743,10 +628,6 @@ nitpick [expect = none] by auto -lemma "I = (\x. x) \ rtrancl = (\x. rtrancl (I x))" -nitpick [card = 1\2, expect = none] -by auto - lemma "((x, x), (x, x)) \ rtrancl {}" nitpick [card = 1\5, expect = none] by auto @@ -755,42 +636,18 @@ nitpick [card = 1\5, expect = none] by auto -lemma "I = (\x. x) \ op \ = (\x y. op \ x (I y))" -nitpick [card = 1\5, expect = none] -by auto - lemma "a \ A \ a \ (A \ B)" "b \ B \ b \ (A \ B)" nitpick [expect = none] by auto -lemma "a \ (A \ B) \ a \ A \ a \ B" -nitpick [expect = none] -by auto - lemma "I = (\x. x) \ op \ = (\x. op \ (I x))" nitpick [card = 1\5, expect = none] by auto -lemma "I = (\x. x) \ op \ = (\x y. op \ x (I y))" -nitpick [card = 1\5, expect = none] -by auto - lemma "a \ A \ a \ (A \ B)" "b \ B \ b \ (A \ B)" nitpick [card = 1\5, expect = none] by auto -lemma "a \ (A \ B) \ a \ A \ a \ B" -nitpick [expect = none] -by auto - -lemma "I = (\x. x) \ op - = (\x\'a set. op - (I x))" -nitpick [card = 1\5, expect = none] -by auto - -lemma "I = (\x. x) \ op - = (\x y\'a set. op - x (I y))" -nitpick [card = 1\5, expect = none] -by auto - lemma "x \ ((A\'a set) - B) \ x \ A \ x \ B" nitpick [card = 1\5, expect = none] by auto @@ -799,22 +656,10 @@ nitpick [card = 1\5, expect = none] by auto -lemma "I = (\x. x) \ op \ = (\x y. op \ x (I y))" -nitpick [card = 1\5, expect = none] -by auto - lemma "A \ B \ (\a \ A. a \ B) \ (\b \ B. b \ A)" nitpick [card = 1\5, expect = none] by auto -lemma "I = (\x. x) \ op \ = (\x. op \ (I x))" -nitpick [card = 1\5, expect = none] -by auto - -lemma "I = (\x. x) \ op \ = (\x y. op \ x (I y))" -nitpick [card = 1\5, expect = none] -by auto - lemma "A \ B \ \a \ A. a \ B" nitpick [card = 1\5, expect = none] by auto @@ -843,10 +688,6 @@ nitpick [card 'a = 10, expect = genuine] oops -lemma "I = (\x. x) \ finite = (\x. finite (I x))" -nitpick [card = 1\7, expect = none] -oops - lemma "finite A" nitpick [expect = none] oops diff -r 9e58f0499f57 -r 3a15ee47c610 src/HOL/Nitpick_Examples/Nitpick_Examples.thy --- 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 diff -r 9e58f0499f57 -r 3a15ee47c610 src/HOL/Predicate_Compile_Examples/ROOT.ML --- 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"]) diff -r 9e58f0499f57 -r 3a15ee47c610 src/HOL/Tools/Nitpick/kodkod_sat.ML --- 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) diff -r 9e58f0499f57 -r 3a15ee47c610 src/HOL/Tools/Nitpick/minipick.ML --- 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; diff -r 9e58f0499f57 -r 3a15ee47c610 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- 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 diff -r 9e58f0499f57 -r 3a15ee47c610 src/HOL/Tools/try.ML --- 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 diff -r 9e58f0499f57 -r 3a15ee47c610 src/HOL/Unix/Unix.thy --- 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 \ 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\file') \ empty" by simp ultimately show ?thesis .. diff -r 9e58f0499f57 -r 3a15ee47c610 src/Pure/General/markup.ML --- 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 **) diff -r 9e58f0499f57 -r 3a15ee47c610 src/Pure/General/markup.scala --- 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) diff -r 9e58f0499f57 -r 3a15ee47c610 src/Pure/Isar/proof_context.ML --- 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; diff -r 9e58f0499f57 -r 3a15ee47c610 src/Pure/PIDE/command.scala --- 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 } } diff -r 9e58f0499f57 -r 3a15ee47c610 src/Pure/PIDE/document.scala --- 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) diff -r 9e58f0499f57 -r 3a15ee47c610 src/Pure/PIDE/isar_document.scala --- 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 } } diff -r 9e58f0499f57 -r 3a15ee47c610 src/Pure/PIDE/markup_tree.scala --- 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) diff -r 9e58f0499f57 -r 3a15ee47c610 src/Pure/Syntax/lexicon.ML --- 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 *) diff -r 9e58f0499f57 -r 3a15ee47c610 src/Pure/Syntax/syntax.ML --- 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; diff -r 9e58f0499f57 -r 3a15ee47c610 src/Tools/jEdit/dist-template/properties/jedit.props --- 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 diff -r 9e58f0499f57 -r 3a15ee47c610 src/Tools/jEdit/src/jedit/document_model.scala --- 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) diff -r 9e58f0499f57 -r 3a15ee47c610 src/Tools/jEdit/src/jedit/document_view.scala --- 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) "TODO:
Tooltip" - 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 diff -r 9e58f0499f57 -r 3a15ee47c610 src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala --- 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 } } diff -r 9e58f0499f57 -r 3a15ee47c610 src/Tools/jEdit/src/jedit/isabelle_markup.scala --- /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) + } +} diff -r 9e58f0499f57 -r 3a15ee47c610 src/Tools/jEdit/src/jedit/plugin.scala --- 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 } }