--- a/Admin/components/components.sha1 Wed Dec 18 10:50:59 2024 +0100
+++ b/Admin/components/components.sha1 Sat Dec 28 16:38:57 2024 +0100
@@ -153,6 +153,7 @@
9467ad54a9ac10a6e7e8db5458d8d2a5516eba96 isabelle_fonts-20210321.tar.gz
1f7a0b9829ecac6552b21e995ad0f0ac168634f3 isabelle_fonts-20210322.tar.gz
667000ce6dd6ea3c2d11601a41c206060468807d isabelle_fonts-20211004.tar.gz
+1d16542fa847c65ae137adb723da3afbbe252abf isabelle_fonts-20241227.tar.gz
916adccd2f40c55116b68b92ce1eccb24d4dd9a2 isabelle_setup-20210630.tar.gz
c611e363287fcc9bdd93c33bef85fa4e66cd3f37 isabelle_setup-20210701.tar.gz
a0e7527448ef0f7ce164a38a50dc26e98de3cad6 isabelle_setup-20210709.tar.gz
--- a/Admin/components/main Wed Dec 18 10:50:59 2024 +0100
+++ b/Admin/components/main Sat Dec 28 16:38:57 2024 +0100
@@ -10,7 +10,7 @@
flatlaf-2.6
foiltex-2.1.4b
idea-icons-20210508
-isabelle_fonts-20211004
+isabelle_fonts-20241227
isabelle_setup-20240327
javamail-20240109
jdk-21.0.5
--- a/NEWS Wed Dec 18 10:50:59 2024 +0100
+++ b/NEWS Sat Dec 28 16:38:57 2024 +0100
@@ -209,6 +209,16 @@
\renewcommand{\isatconst}[1]{{\color{darkgray}#1}}
\renewcommand{\isaconst}[1]{\textsl{\color{darkgray}#1}}
+* LaTeX presentation of outer syntax keywords now distinguishes
+keyword1, keyword2, keyword3 more carefully. This allows to imitate
+Isabelle/jEdit rendering like this:
+
+ \renewcommand{\isacommand}[1]{\isakeywordONE{#1}}
+ \renewcommand{\isakeywordONE}[1]{\isakeyword{\color[RGB]{0,102,153}#1}}
+ \renewcommand{\isakeywordTWO}[1]{\isakeyword{\color[RGB]{0,153,102}#1}}
+ \renewcommand{\isakeywordTHREE}[1]{\isakeyword{\color[RGB]{0,153,255}#1}}
+
+
*** HOL ***
--- a/lib/texinputs/isabelle.sty Wed Dec 18 10:50:59 2024 +0100
+++ b/lib/texinputs/isabelle.sty Sat Dec 28 16:38:57 2024 +0100
@@ -151,6 +151,9 @@
{\emph{\normalfont\bfseries\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
\newcommand{\isacommand}[1]{\isakeyword{#1}}
+\newcommand{\isakeywordONE}[1]{\isakeyword{#1}}
+\newcommand{\isakeywordTWO}[1]{\isakeyword{#1}}
+\newcommand{\isakeywordTHREE}[1]{\isakeyword{#1}}
\newcommand{\isatclass}[1]{#1}
\newcommand{\isatconst}[1]{#1}
\newcommand{\isatfree}[1]{#1}
--- a/src/Doc/Sledgehammer/document/root.tex Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Sat Dec 28 16:38:57 2024 +0100
@@ -825,6 +825,12 @@
\opnodefault{prover}{string}
Alias for \textit{provers}.
+\opdefault{cache\_dir}{string}{""}
+Specifies whether Sledgehammer should cache the result of the external provers or not and, if yes, where.
+If the option is set to the empty string (i.e., ""), then no caching takes place.
+Otherwise, the string is interpreted as a path to a directory where the cached result will be saved.
+The content of the cache directory can be deleted at any time to reset the cache.
+
\opsmartfalse{falsify}{dont\_falsify}
Specifies whether Sledgehammer should look for falsifications or for proofs. If
the option is set to \textit{smart}, it looks for both.
--- a/src/HOL/Bit_Operations.thy Wed Dec 18 10:50:59 2024 +0100
+++ b/src/HOL/Bit_Operations.thy Sat Dec 28 16:38:57 2024 +0100
@@ -1237,14 +1237,6 @@
\<open>take_bit n (flip_bit m a) = (if n \<le> m then take_bit n a else flip_bit m (take_bit n a))\<close>
by (rule bit_eqI) (auto simp: bit_take_bit_iff bit_flip_bit_iff)
-lemma bit_1_0 [simp]:
- \<open>bit 1 0\<close>
- by (simp add: bit_0)
-
-lemma not_bit_1_Suc [simp]:
- \<open>\<not> bit 1 (Suc n)\<close>
- by (simp add: bit_Suc)
-
lemma push_bit_Suc_numeral [simp]:
\<open>push_bit (Suc n) (numeral k) = push_bit n (numeral (Num.Bit0 k))\<close>
by (simp add: numeral_eq_Suc mult_2_right) (simp add: numeral_Bit0)
@@ -1387,7 +1379,7 @@
lemma not_one_eq [simp]:
\<open>NOT 1 = - 2\<close>
- by (simp add: bit_eq_iff bit_not_iff) (simp add: bit_1_iff)
+ by (rule bit_eqI, simp add: bit_simps)
sublocale "and": semilattice_neutr \<open>(AND)\<close> \<open>- 1\<close>
by standard (rule bit_eqI, simp add: bit_and_iff)
@@ -2695,6 +2687,18 @@
context semiring_bits
begin
+lemma bit_1_0 [simp]:
+ \<open>bit 1 0\<close>
+ by (simp add: bit_0)
+
+lemma not_bit_1_Suc [simp]:
+ \<open>\<not> bit 1 (Suc n)\<close>
+ by (simp add: bit_Suc)
+
+lemma not_bit_1_numeral [simp]:
+ \<open>\<not> bit 1 (numeral m)\<close>
+ by (simp add: numeral_eq_Suc)
+
lemma not_bit_numeral_Bit0_0 [simp]:
\<open>\<not> bit (numeral (Num.Bit0 m)) 0\<close>
by (simp add: bit_0)
@@ -2770,7 +2774,6 @@
by (cases n; simp add: bit_0)+
lemma bit_numeral_simps [simp]:
- \<open>\<not> bit 1 (numeral n)\<close>
\<open>bit (numeral (Num.Bit0 w)) (numeral n) \<longleftrightarrow> bit (numeral w) (pred_numeral n)\<close>
\<open>bit (numeral (Num.Bit1 w)) (numeral n) \<longleftrightarrow> bit (numeral w) (pred_numeral n)\<close>
by (simp_all add: bit_1_iff numeral_eq_Suc)
@@ -2923,7 +2926,8 @@
\<open>numeral (Num.Bit1 m) AND NOT (1 :: int) = numeral (Num.Bit0 m)\<close>
\<open>numeral (Num.Bit1 m) AND NOT (numeral (Num.Bit0 n)) = 1 + (2 :: int) * (numeral m AND NOT (numeral n))\<close>
\<open>numeral (Num.Bit1 m) AND NOT (numeral (Num.Bit1 n)) = (2 :: int) * (numeral m AND NOT (numeral n))\<close>
- by (simp_all add: bit_eq_iff) (auto simp: bit_0 bit_simps bit_Suc bit_numeral_rec BitM_inc_eq sub_inc_One_eq split: nat.split)
+ by (simp_all add: bit_eq_iff)
+ (auto simp: bit_0 bit_simps bit_Suc bit_numeral_rec BitM_inc_eq sub_inc_One_eq split: nat.split)
fun and_not_num :: \<open>num \<Rightarrow> num \<Rightarrow> num option\<close> \<^marker>\<open>contributor \<open>Andreas Lochbihler\<close>\<close>
where
--- a/src/HOL/Code_Numeral.thy Wed Dec 18 10:50:59 2024 +0100
+++ b/src/HOL/Code_Numeral.thy Sat Dec 28 16:38:57 2024 +0100
@@ -136,6 +136,18 @@
is Int.nat
.
+lemma nat_of_integer_0 [simp]:
+ \<open>nat_of_integer 0 = 0\<close>
+ by transfer simp
+
+lemma nat_of_integer_1 [simp]:
+ \<open>nat_of_integer 1 = 1\<close>
+ by transfer simp
+
+lemma nat_of_integer_numeral [simp]:
+ \<open>nat_of_integer (numeral n) = numeral n\<close>
+ by transfer simp
+
lemma nat_of_integer_of_nat [simp]:
"nat_of_integer (of_nat n) = n"
by transfer simp
@@ -860,6 +872,26 @@
and (Haskell) "Prelude.abs"
and (Scala) "_.abs"
and (Eval) "abs"
+| constant "Bit_Operations.and :: integer \<Rightarrow> integer \<Rightarrow> integer" \<rightharpoonup>
+ (SML) "IntInf.andb ((_),/ (_))"
+ and (OCaml) "Z.logand"
+ and (Haskell) infixl 7 ".&."
+ and (Scala) infixl 3 "&"
+| constant "Bit_Operations.or :: integer \<Rightarrow> integer \<Rightarrow> integer" \<rightharpoonup>
+ (SML) "IntInf.orb ((_),/ (_))"
+ and (OCaml) "Z.logor"
+ and (Haskell) infixl 5 ".|."
+ and (Scala) infixl 1 "|"
+| constant "Bit_Operations.xor :: integer \<Rightarrow> integer \<Rightarrow> integer" \<rightharpoonup>
+ (SML) "IntInf.xorb ((_),/ (_))"
+ and (OCaml) "Z.logxor"
+ and (Haskell) infixl 6 ".^."
+ and (Scala) infixl 2 "^"
+| constant "Bit_Operations.not :: integer \<Rightarrow> integer" \<rightharpoonup>
+ (SML) "IntInf.notb"
+ and (OCaml) "Z.lognot"
+ and (Haskell) "Data.Bits.complement"
+ and (Scala) "_.unary'_~"
code_identifier
code_module Code_Numeral \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
@@ -1249,7 +1281,7 @@
lemma [code]:
\<open>integer_of_natural (mask n) = mask n\<close>
- by transfer (simp add: mask_eq_exp_minus_1 of_nat_diff)
+ by transfer (simp add: mask_eq_exp_minus_1)
lemma [code_abbrev]:
"natural_of_integer (Code_Numeral.Pos k) = numeral k"
--- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy Wed Dec 18 10:50:59 2024 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy Sat Dec 28 16:38:57 2024 +0100
@@ -1,10 +1,15 @@
(* Title: HOL/Codegenerator_Test/Code_Test_GHC.thy
Author: Andreas Lochbihler, ETH Zurich
-
-Test case for test_code on GHC
+ Author: Florian Haftmann, TU Muenchen
*)
-theory Code_Test_GHC imports "HOL-Library.Code_Test" Code_Lazy_Test begin
+theory Code_Test_GHC
+imports
+ "HOL-Library.Code_Test"
+ Code_Lazy_Test
+begin
+
+text \<open>Test cases for \<^text>\<open>test_code\<close>\<close>
test_code "(14 + 7 * -12 :: integer) = 140 div -2" in GHC
@@ -22,4 +27,163 @@
test_code "stake 10 (cycle ''ab'') = ''ababababab''" in GHC
+text \<open>Test cases for bit operations on target language numerals\<close>
+
+unbundle bit_operations_syntax
+
+lemma \<open>bit (473514 :: integer) 5\<close>
+ by normalization
+
+test_code \<open>bit (473514 :: integer) 5\<close> in GHC
+
+lemma \<open>bit (- 805167 :: integer) 7\<close>
+ by normalization
+
+test_code \<open>bit (- 805167 :: integer) 7\<close> in GHC
+
+lemma \<open>473514 AND (767063 :: integer) = 208898\<close>
+ by normalization
+
+test_code \<open>473514 AND (767063 :: integer) = 208898\<close> in GHC
+
+lemma \<open>- 805167 AND (767063 :: integer) = 242769\<close>
+ by normalization
+
+test_code \<open>- 805167 AND (767063 :: integer) = 242769\<close> in GHC
+
+lemma \<open>473514 AND (- 314527 :: integer) = 209184\<close>
+ by normalization
+
+test_code \<open>473514 AND (- 314527 :: integer) = 209184\<close> in GHC
+
+lemma \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close>
+ by normalization
+
+test_code \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close> in GHC
+
+lemma \<open>473514 OR (767063 :: integer) = 1031679\<close>
+ by normalization
+
+test_code \<open>473514 OR (767063 :: integer) = 1031679\<close> in GHC
+
+lemma \<open>- 805167 OR (767063 :: integer) = - 280873\<close>
+ by normalization
+
+test_code \<open>- 805167 OR (767063 :: integer) = - 280873\<close> in GHC
+
+lemma \<open>473514 OR (- 314527 :: integer) = - 50197\<close>
+ by normalization
+
+test_code \<open>473514 OR (- 314527 :: integer) = - 50197\<close> in GHC
+
+lemma \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close>
+ by normalization
+
+test_code \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close> in GHC
+
+lemma \<open>473514 XOR (767063 :: integer) = 822781\<close>
+ by normalization
+
+test_code \<open>473514 XOR (767063 :: integer) = 822781\<close> in GHC
+
+lemma \<open>- 805167 XOR (767063 :: integer) = - 523642\<close>
+ by normalization
+
+test_code \<open>- 805167 XOR (767063 :: integer) = - 523642\<close> in GHC
+
+lemma \<open>473514 XOR (- 314527 :: integer) = - 259381\<close>
+ by normalization
+
+test_code \<open>473514 XOR (- 314527 :: integer) = - 259381\<close> in GHC
+
+lemma \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close>
+ by normalization
+
+test_code \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close> in GHC
+
+lemma \<open>NOT (473513 :: integer) = - 473514\<close>
+ by normalization
+
+test_code \<open>NOT (473513 :: integer) = - 473514\<close> in GHC
+
+lemma \<open>NOT (- 805167 :: integer) = 805166\<close>
+ by normalization
+
+test_code \<open>NOT (- 805167 :: integer) = 805166\<close> in GHC
+
+lemma \<open>(mask 39 :: integer) = 549755813887\<close>
+ by normalization
+
+test_code \<open>(mask 39 :: integer) = 549755813887\<close> in GHC
+
+lemma \<open>set_bit 15 (473514 :: integer) = 506282\<close>
+ by normalization
+
+test_code \<open>set_bit 15 (473514 :: integer) = 506282\<close> in GHC
+
+lemma \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close>
+ by normalization
+
+test_code \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close> in GHC
+
+lemma \<open>unset_bit 13 (473514 :: integer) = 465322\<close>
+ by normalization
+
+test_code \<open>unset_bit 13 (473514 :: integer) = 465322\<close> in GHC
+
+lemma \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close>
+ by normalization
+
+test_code \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close> in GHC
+
+lemma \<open>flip_bit 15 (473514 :: integer) = 506282\<close>
+ by normalization
+
+test_code \<open>flip_bit 15 (473514 :: integer) = 506282\<close> in GHC
+
+lemma \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close>
+ by normalization
+
+test_code \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close> in GHC
+
+lemma \<open>push_bit 12 (473514 :: integer) = 1939513344\<close>
+ by normalization
+
+test_code \<open>push_bit 12 (473514 :: integer) = 1939513344\<close> in GHC
+
+lemma \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close>
+ by normalization
+
+test_code \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close> in GHC
+
+lemma \<open>drop_bit 12 (473514 :: integer) = 115\<close>
+ by normalization
+
+test_code \<open>drop_bit 12 (473514 :: integer) = 115\<close> in GHC
+
+lemma \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close>
+ by normalization
+
+test_code \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close> in GHC
+
+lemma \<open>take_bit 12 (473514 :: integer) = 2474\<close>
+ by normalization
+
+test_code \<open>take_bit 12 (473514 :: integer) = 2474\<close> in GHC
+
+lemma \<open>take_bit 12 (- 805167 :: integer) = 1745\<close>
+ by normalization
+
+test_code \<open>take_bit 12 (- 805167 :: integer) = 1745\<close> in GHC
+
+lemma \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close>
+ by normalization
+
+test_code \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close> in GHC
+
+lemma \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close>
+ by normalization
+
+test_code \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close> in GHC
+
end
--- a/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy Wed Dec 18 10:50:59 2024 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy Sat Dec 28 16:38:57 2024 +0100
@@ -1,10 +1,15 @@
(* Title: HOL/Codegenerator_Test/Code_Test_OCaml.thy
Author: Andreas Lochbihler, ETH Zurich
-
-Test case for test_code on OCaml
+ Author: Florian Haftmann, TU Muenchen
*)
-theory Code_Test_OCaml imports "HOL-Library.Code_Test" Code_Lazy_Test begin
+theory Code_Test_OCaml
+imports
+ "HOL-Library.Code_Test"
+ Code_Lazy_Test
+begin
+
+text \<open>Test cases for \<^text>\<open>test_code\<close>\<close>
test_code "14 + 7 * -12 = (140 div -2 :: integer)" in OCaml
@@ -22,4 +27,163 @@
test_code "stake 10 (cycle ''ab'') = ''ababababab''" in OCaml
+text \<open>Test cases for bit operations on target language numerals\<close>
+
+unbundle bit_operations_syntax
+
+lemma \<open>bit (473514 :: integer) 5\<close>
+ by normalization
+
+test_code \<open>bit (473514 :: integer) 5\<close> in OCaml
+
+lemma \<open>bit (- 805167 :: integer) 7\<close>
+ by normalization
+
+test_code \<open>bit (- 805167 :: integer) 7\<close> in OCaml
+
+lemma \<open>473514 AND (767063 :: integer) = 208898\<close>
+ by normalization
+
+test_code \<open>473514 AND (767063 :: integer) = 208898\<close> in OCaml
+
+lemma \<open>- 805167 AND (767063 :: integer) = 242769\<close>
+ by normalization
+
+test_code \<open>- 805167 AND (767063 :: integer) = 242769\<close> in OCaml
+
+lemma \<open>473514 AND (- 314527 :: integer) = 209184\<close>
+ by normalization
+
+test_code \<open>473514 AND (- 314527 :: integer) = 209184\<close> in OCaml
+
+lemma \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close>
+ by normalization
+
+test_code \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close> in OCaml
+
+lemma \<open>473514 OR (767063 :: integer) = 1031679\<close>
+ by normalization
+
+test_code \<open>473514 OR (767063 :: integer) = 1031679\<close> in OCaml
+
+lemma \<open>- 805167 OR (767063 :: integer) = - 280873\<close>
+ by normalization
+
+test_code \<open>- 805167 OR (767063 :: integer) = - 280873\<close> in OCaml
+
+lemma \<open>473514 OR (- 314527 :: integer) = - 50197\<close>
+ by normalization
+
+test_code \<open>473514 OR (- 314527 :: integer) = - 50197\<close> in OCaml
+
+lemma \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close>
+ by normalization
+
+test_code \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close> in OCaml
+
+lemma \<open>473514 XOR (767063 :: integer) = 822781\<close>
+ by normalization
+
+test_code \<open>473514 XOR (767063 :: integer) = 822781\<close> in OCaml
+
+lemma \<open>- 805167 XOR (767063 :: integer) = - 523642\<close>
+ by normalization
+
+test_code \<open>- 805167 XOR (767063 :: integer) = - 523642\<close> in OCaml
+
+lemma \<open>473514 XOR (- 314527 :: integer) = - 259381\<close>
+ by normalization
+
+test_code \<open>473514 XOR (- 314527 :: integer) = - 259381\<close> in OCaml
+
+lemma \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close>
+ by normalization
+
+test_code \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close> in OCaml
+
+lemma \<open>NOT (473513 :: integer) = - 473514\<close>
+ by normalization
+
+test_code \<open>NOT (473513 :: integer) = - 473514\<close> in OCaml
+
+lemma \<open>NOT (- 805167 :: integer) = 805166\<close>
+ by normalization
+
+test_code \<open>NOT (- 805167 :: integer) = 805166\<close> in OCaml
+
+lemma \<open>(mask 39 :: integer) = 549755813887\<close>
+ by normalization
+
+test_code \<open>(mask 39 :: integer) = 549755813887\<close> in OCaml
+
+lemma \<open>set_bit 15 (473514 :: integer) = 506282\<close>
+ by normalization
+
+test_code \<open>set_bit 15 (473514 :: integer) = 506282\<close> in OCaml
+
+lemma \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close>
+ by normalization
+
+test_code \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close> in OCaml
+
+lemma \<open>unset_bit 13 (473514 :: integer) = 465322\<close>
+ by normalization
+
+test_code \<open>unset_bit 13 (473514 :: integer) = 465322\<close> in OCaml
+
+lemma \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close>
+ by normalization
+
+test_code \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close> in OCaml
+
+lemma \<open>flip_bit 15 (473514 :: integer) = 506282\<close>
+ by normalization
+
+test_code \<open>flip_bit 15 (473514 :: integer) = 506282\<close> in OCaml
+
+lemma \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close>
+ by normalization
+
+test_code \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close> in OCaml
+
+lemma \<open>push_bit 12 (473514 :: integer) = 1939513344\<close>
+ by normalization
+
+test_code \<open>push_bit 12 (473514 :: integer) = 1939513344\<close> in OCaml
+
+lemma \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close>
+ by normalization
+
+test_code \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close> in OCaml
+
+lemma \<open>drop_bit 12 (473514 :: integer) = 115\<close>
+ by normalization
+
+test_code \<open>drop_bit 12 (473514 :: integer) = 115\<close> in OCaml
+
+lemma \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close>
+ by normalization
+
+test_code \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close> in OCaml
+
+lemma \<open>take_bit 12 (473514 :: integer) = 2474\<close>
+ by normalization
+
+test_code \<open>take_bit 12 (473514 :: integer) = 2474\<close> in OCaml
+
+lemma \<open>take_bit 12 (- 805167 :: integer) = 1745\<close>
+ by normalization
+
+test_code \<open>take_bit 12 (- 805167 :: integer) = 1745\<close> in OCaml
+
+lemma \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close>
+ by normalization
+
+test_code \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close> in OCaml
+
+lemma \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close>
+ by normalization
+
+test_code \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close> in OCaml
+
end
--- a/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy Wed Dec 18 10:50:59 2024 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy Sat Dec 28 16:38:57 2024 +0100
@@ -1,10 +1,15 @@
(* Title: HOL/Codegenerator_Test/Code_Test_PolyML.thy
Author: Andreas Lochbihler, ETH Zurich
-
-Test case for test_code on PolyML
+ Author: Florian Haftmann, TU Muenchen
*)
-theory Code_Test_PolyML imports "HOL-Library.Code_Test" Code_Lazy_Test begin
+theory Code_Test_PolyML
+imports
+ "HOL-Library.Code_Test"
+ Code_Lazy_Test
+begin
+
+text \<open>Test cases for \<^text>\<open>test_code\<close>\<close>
test_code "14 + 7 * -12 = (140 div -2 :: integer)" in PolyML
@@ -12,4 +17,163 @@
test_code "stake 10 (cycle ''ab'') = ''ababababab''" in PolyML
+text \<open>Test cases for bit operations on target language numerals\<close>
+
+unbundle bit_operations_syntax
+
+lemma \<open>bit (473514 :: integer) 5\<close>
+ by normalization
+
+test_code \<open>bit (473514 :: integer) 5\<close> in PolyML
+
+lemma \<open>bit (- 805167 :: integer) 7\<close>
+ by normalization
+
+test_code \<open>bit (- 805167 :: integer) 7\<close> in PolyML
+
+lemma \<open>473514 AND (767063 :: integer) = 208898\<close>
+ by normalization
+
+test_code \<open>473514 AND (767063 :: integer) = 208898\<close> in PolyML
+
+lemma \<open>- 805167 AND (767063 :: integer) = 242769\<close>
+ by normalization
+
+test_code \<open>- 805167 AND (767063 :: integer) = 242769\<close> in PolyML
+
+lemma \<open>473514 AND (- 314527 :: integer) = 209184\<close>
+ by normalization
+
+test_code \<open>473514 AND (- 314527 :: integer) = 209184\<close> in PolyML
+
+lemma \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close>
+ by normalization
+
+test_code \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close> in PolyML
+
+lemma \<open>473514 OR (767063 :: integer) = 1031679\<close>
+ by normalization
+
+test_code \<open>473514 OR (767063 :: integer) = 1031679\<close> in PolyML
+
+lemma \<open>- 805167 OR (767063 :: integer) = - 280873\<close>
+ by normalization
+
+test_code \<open>- 805167 OR (767063 :: integer) = - 280873\<close> in PolyML
+
+lemma \<open>473514 OR (- 314527 :: integer) = - 50197\<close>
+ by normalization
+
+test_code \<open>473514 OR (- 314527 :: integer) = - 50197\<close> in PolyML
+
+lemma \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close>
+ by normalization
+
+test_code \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close> in PolyML
+
+lemma \<open>473514 XOR (767063 :: integer) = 822781\<close>
+ by normalization
+
+test_code \<open>473514 XOR (767063 :: integer) = 822781\<close> in PolyML
+
+lemma \<open>- 805167 XOR (767063 :: integer) = - 523642\<close>
+ by normalization
+
+test_code \<open>- 805167 XOR (767063 :: integer) = - 523642\<close> in PolyML
+
+lemma \<open>473514 XOR (- 314527 :: integer) = - 259381\<close>
+ by normalization
+
+test_code \<open>473514 XOR (- 314527 :: integer) = - 259381\<close> in PolyML
+
+lemma \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close>
+ by normalization
+
+test_code \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close> in PolyML
+
+lemma \<open>NOT (473513 :: integer) = - 473514\<close>
+ by normalization
+
+test_code \<open>NOT (473513 :: integer) = - 473514\<close> in PolyML
+
+lemma \<open>NOT (- 805167 :: integer) = 805166\<close>
+ by normalization
+
+test_code \<open>NOT (- 805167 :: integer) = 805166\<close> in PolyML
+
+lemma \<open>(mask 39 :: integer) = 549755813887\<close>
+ by normalization
+
+test_code \<open>(mask 39 :: integer) = 549755813887\<close> in PolyML
+
+lemma \<open>set_bit 15 (473514 :: integer) = 506282\<close>
+ by normalization
+
+test_code \<open>set_bit 15 (473514 :: integer) = 506282\<close> in PolyML
+
+lemma \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close>
+ by normalization
+
+test_code \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close> in PolyML
+
+lemma \<open>unset_bit 13 (473514 :: integer) = 465322\<close>
+ by normalization
+
+test_code \<open>unset_bit 13 (473514 :: integer) = 465322\<close> in PolyML
+
+lemma \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close>
+ by normalization
+
+test_code \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close> in PolyML
+
+lemma \<open>flip_bit 15 (473514 :: integer) = 506282\<close>
+ by normalization
+
+test_code \<open>flip_bit 15 (473514 :: integer) = 506282\<close> in PolyML
+
+lemma \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close>
+ by normalization
+
+test_code \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close> in PolyML
+
+lemma \<open>push_bit 12 (473514 :: integer) = 1939513344\<close>
+ by normalization
+
+test_code \<open>push_bit 12 (473514 :: integer) = 1939513344\<close> in PolyML
+
+lemma \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close>
+ by normalization
+
+test_code \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close> in PolyML
+
+lemma \<open>drop_bit 12 (473514 :: integer) = 115\<close>
+ by normalization
+
+test_code \<open>drop_bit 12 (473514 :: integer) = 115\<close> in PolyML
+
+lemma \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close>
+ by normalization
+
+test_code \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close> in PolyML
+
+lemma \<open>take_bit 12 (473514 :: integer) = 2474\<close>
+ by normalization
+
+test_code \<open>take_bit 12 (473514 :: integer) = 2474\<close> in PolyML
+
+lemma \<open>take_bit 12 (- 805167 :: integer) = 1745\<close>
+ by normalization
+
+test_code \<open>take_bit 12 (- 805167 :: integer) = 1745\<close> in PolyML
+
+lemma \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close>
+ by normalization
+
+test_code \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close> in PolyML
+
+lemma \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close>
+ by normalization
+
+test_code \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close> in PolyML
+
end
--- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy Wed Dec 18 10:50:59 2024 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy Sat Dec 28 16:38:57 2024 +0100
@@ -1,10 +1,14 @@
(* Title: HOL/Codegenerator_Test/Code_Test_Scala.thy
Author: Andreas Lochbihler, ETH Zurich
-
-Test case for test_code on Scala
+ Author: Florian Haftmann, TU Muenchen
*)
-theory Code_Test_Scala imports "HOL-Library.Code_Test" Code_Lazy_Test begin
+theory Code_Test_Scala imports
+ "HOL-Library.Code_Test"
+ Code_Lazy_Test
+begin
+
+text \<open>Test cases for \<^text>\<open>test_code\<close>\<close>
test_code "14 + 7 * -12 = (140 div -2 :: integer)" in Scala
@@ -22,4 +26,163 @@
test_code "stake 10 (cycle ''ab'') = ''ababababab''" in Scala
+text \<open>Test cases for bit operations on target language numerals\<close>
+
+unbundle bit_operations_syntax
+
+lemma \<open>bit (473514 :: integer) 5\<close>
+ by normalization
+
+test_code \<open>bit (473514 :: integer) 5\<close> in Scala
+
+lemma \<open>bit (- 805167 :: integer) 7\<close>
+ by normalization
+
+test_code \<open>bit (- 805167 :: integer) 7\<close> in Scala
+
+lemma \<open>473514 AND (767063 :: integer) = 208898\<close>
+ by normalization
+
+test_code \<open>473514 AND (767063 :: integer) = 208898\<close> in Scala
+
+lemma \<open>- 805167 AND (767063 :: integer) = 242769\<close>
+ by normalization
+
+test_code \<open>- 805167 AND (767063 :: integer) = 242769\<close> in Scala
+
+lemma \<open>473514 AND (- 314527 :: integer) = 209184\<close>
+ by normalization
+
+test_code \<open>473514 AND (- 314527 :: integer) = 209184\<close> in Scala
+
+lemma \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close>
+ by normalization
+
+test_code \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close> in Scala
+
+lemma \<open>473514 OR (767063 :: integer) = 1031679\<close>
+ by normalization
+
+test_code \<open>473514 OR (767063 :: integer) = 1031679\<close> in Scala
+
+lemma \<open>- 805167 OR (767063 :: integer) = - 280873\<close>
+ by normalization
+
+test_code \<open>- 805167 OR (767063 :: integer) = - 280873\<close> in Scala
+
+lemma \<open>473514 OR (- 314527 :: integer) = - 50197\<close>
+ by normalization
+
+test_code \<open>473514 OR (- 314527 :: integer) = - 50197\<close> in Scala
+
+lemma \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close>
+ by normalization
+
+test_code \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close> in Scala
+
+lemma \<open>473514 XOR (767063 :: integer) = 822781\<close>
+ by normalization
+
+test_code \<open>473514 XOR (767063 :: integer) = 822781\<close> in Scala
+
+lemma \<open>- 805167 XOR (767063 :: integer) = - 523642\<close>
+ by normalization
+
+test_code \<open>- 805167 XOR (767063 :: integer) = - 523642\<close> in Scala
+
+lemma \<open>473514 XOR (- 314527 :: integer) = - 259381\<close>
+ by normalization
+
+test_code \<open>473514 XOR (- 314527 :: integer) = - 259381\<close> in Scala
+
+lemma \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close>
+ by normalization
+
+test_code \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close> in Scala
+
+lemma \<open>NOT (473513 :: integer) = - 473514\<close>
+ by normalization
+
+test_code \<open>NOT (473513 :: integer) = - 473514\<close> in Scala
+
+lemma \<open>NOT (- 805167 :: integer) = 805166\<close>
+ by normalization
+
+test_code \<open>NOT (- 805167 :: integer) = 805166\<close> in Scala
+
+lemma \<open>(mask 39 :: integer) = 549755813887\<close>
+ by normalization
+
+test_code \<open>(mask 39 :: integer) = 549755813887\<close> in Scala
+
+lemma \<open>set_bit 15 (473514 :: integer) = 506282\<close>
+ by normalization
+
+test_code \<open>set_bit 15 (473514 :: integer) = 506282\<close> in Scala
+
+lemma \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close>
+ by normalization
+
+test_code \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close> in Scala
+
+lemma \<open>unset_bit 13 (473514 :: integer) = 465322\<close>
+ by normalization
+
+test_code \<open>unset_bit 13 (473514 :: integer) = 465322\<close> in Scala
+
+lemma \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close>
+ by normalization
+
+test_code \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close> in Scala
+
+lemma \<open>flip_bit 15 (473514 :: integer) = 506282\<close>
+ by normalization
+
+test_code \<open>flip_bit 15 (473514 :: integer) = 506282\<close> in Scala
+
+lemma \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close>
+ by normalization
+
+test_code \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close> in Scala
+
+lemma \<open>push_bit 12 (473514 :: integer) = 1939513344\<close>
+ by normalization
+
+test_code \<open>push_bit 12 (473514 :: integer) = 1939513344\<close> in Scala
+
+lemma \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close>
+ by normalization
+
+test_code \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close> in Scala
+
+lemma \<open>drop_bit 12 (473514 :: integer) = 115\<close>
+ by normalization
+
+test_code \<open>drop_bit 12 (473514 :: integer) = 115\<close> in Scala
+
+lemma \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close>
+ by normalization
+
+test_code \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close> in Scala
+
+lemma \<open>take_bit 12 (473514 :: integer) = 2474\<close>
+ by normalization
+
+test_code \<open>take_bit 12 (473514 :: integer) = 2474\<close> in Scala
+
+lemma \<open>take_bit 12 (- 805167 :: integer) = 1745\<close>
+ by normalization
+
+test_code \<open>take_bit 12 (- 805167 :: integer) = 1745\<close> in Scala
+
+lemma \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close>
+ by normalization
+
+test_code \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close> in Scala
+
+lemma \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close>
+ by normalization
+
+test_code \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close> in Scala
+
end
--- a/src/HOL/HOLCF/Algebraic.thy Wed Dec 18 10:50:59 2024 +0100
+++ b/src/HOL/HOLCF/Algebraic.thy Sat Dec 28 16:38:57 2024 +0100
@@ -47,11 +47,11 @@
by (rule Rep_fin_defl.belowD)
lemma fin_defl_eqI:
- "(\<And>x. Rep_fin_defl a\<cdot>x = x \<longleftrightarrow> Rep_fin_defl b\<cdot>x = x) \<Longrightarrow> a = b"
-apply (rule below_antisym)
-apply (rule fin_defl_belowI, simp)
-apply (rule fin_defl_belowI, simp)
-done
+ "a = b" if "(\<And>x. Rep_fin_defl a\<cdot>x = x \<longleftrightarrow> Rep_fin_defl b\<cdot>x = x)"
+proof (rule below_antisym)
+ show "a \<sqsubseteq> b" by (rule fin_defl_belowI) (simp add: that)
+ show "b \<sqsubseteq> a" by (rule fin_defl_belowI) (simp add: that)
+qed
lemma Rep_fin_defl_mono: "a \<sqsubseteq> b \<Longrightarrow> Rep_fin_defl a \<sqsubseteq> Rep_fin_defl b"
unfolding below_fin_defl_def .
@@ -63,8 +63,8 @@
by (simp add: Abs_fin_defl_inverse)
lemma (in finite_deflation) compact_belowI:
- assumes "\<And>x. compact x \<Longrightarrow> d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x" shows "d \<sqsubseteq> f"
-by (rule belowI, rule assms, erule subst, rule compact)
+ "d \<sqsubseteq> f" if "\<And>x. compact x \<Longrightarrow> d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x"
+ by (rule belowI, rule that, erule subst, rule compact)
lemma compact_Rep_fin_defl [simp]: "compact (Rep_fin_defl a)"
using finite_deflation_Rep_fin_defl
@@ -79,10 +79,10 @@
instantiation defl :: (bifinite) below
begin
-definition
- "x \<sqsubseteq> y \<longleftrightarrow> Rep_defl x \<subseteq> Rep_defl y"
+definition "x \<sqsubseteq> y \<longleftrightarrow> Rep_defl x \<subseteq> Rep_defl y"
instance ..
+
end
instance defl :: (bifinite) po
@@ -93,9 +93,8 @@
using type_definition_defl below_defl_def
by (rule below.typedef_ideal_cpo)
-definition
- defl_principal :: "'a::bifinite fin_defl \<Rightarrow> 'a defl" where
- "defl_principal t = Abs_defl {u. u \<sqsubseteq> t}"
+definition defl_principal :: "'a::bifinite fin_defl \<Rightarrow> 'a defl"
+ where "defl_principal t = Abs_defl {u. u \<sqsubseteq> t}"
lemma fin_defl_countable: "\<exists>f::'a::bifinite fin_defl \<Rightarrow> nat. inj f"
proof -
@@ -134,11 +133,13 @@
text \<open>Algebraic deflations are pointed\<close>
lemma defl_minimal: "defl_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> x"
-apply (induct x rule: defl.principal_induct, simp)
-apply (rule defl.principal_mono)
-apply (simp add: below_fin_defl_def)
-apply (simp add: Abs_fin_defl_inverse finite_deflation_bottom)
-done
+proof (induct x rule: defl.principal_induct)
+ fix a :: "'a fin_defl"
+ have "Abs_fin_defl \<bottom> \<sqsubseteq> a"
+ by (simp add: below_fin_defl_def Abs_fin_defl_inverse finite_deflation_bottom)
+ then show "defl_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> defl_principal a"
+ by (rule defl.principal_mono)
+qed simp
instance defl :: (bifinite) pcpo
by intro_classes (fast intro: defl_minimal)
@@ -149,17 +150,12 @@
subsection \<open>Applying algebraic deflations\<close>
-definition
- cast :: "'a::bifinite defl \<rightarrow> 'a \<rightarrow> 'a"
-where
- "cast = defl.extension Rep_fin_defl"
+definition cast :: "'a::bifinite defl \<rightarrow> 'a \<rightarrow> 'a"
+ where "cast = defl.extension Rep_fin_defl"
-lemma cast_defl_principal:
- "cast\<cdot>(defl_principal a) = Rep_fin_defl a"
-unfolding cast_def
-apply (rule defl.extension_principal)
-apply (simp only: below_fin_defl_def)
-done
+lemma cast_defl_principal: "cast\<cdot>(defl_principal a) = Rep_fin_defl a"
+ unfolding cast_def
+ by (rule defl.extension_principal) (simp only: below_fin_defl_def)
lemma deflation_cast: "deflation (cast\<cdot>d)"
apply (induct d rule: defl.principal_induct)
@@ -169,22 +165,20 @@
apply (rule finite_deflation_Rep_fin_defl)
done
-lemma finite_deflation_cast:
- "compact d \<Longrightarrow> finite_deflation (cast\<cdot>d)"
-apply (drule defl.compact_imp_principal, clarify)
-apply (simp add: cast_defl_principal)
-apply (rule finite_deflation_Rep_fin_defl)
-done
+lemma finite_deflation_cast: "compact d \<Longrightarrow> finite_deflation (cast\<cdot>d)"
+ apply (drule defl.compact_imp_principal)
+ apply clarify
+ apply (simp add: cast_defl_principal)
+ apply (rule finite_deflation_Rep_fin_defl)
+ done
interpretation cast: deflation "cast\<cdot>d"
by (rule deflation_cast)
declare cast.idem [simp]
-lemma compact_cast [simp]: "compact d \<Longrightarrow> compact (cast\<cdot>d)"
-apply (rule finite_deflation_imp_compact)
-apply (erule finite_deflation_cast)
-done
+lemma compact_cast [simp]: "compact (cast\<cdot>d)" if "compact d"
+ by (rule finite_deflation_imp_compact) (use that in \<open>rule finite_deflation_cast\<close>)
lemma cast_below_cast: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<longleftrightarrow> A \<sqsubseteq> B"
apply (induct A rule: defl.principal_induct, simp)
@@ -236,10 +230,13 @@
assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)"
shows "cast\<cdot>(defl_fun1 e p f\<cdot>A) = e oo f\<cdot>(cast\<cdot>A) oo p"
proof -
- have 1: "\<And>a. finite_deflation (e oo f\<cdot>(Rep_fin_defl a) oo p)"
- apply (rule ep_pair.finite_deflation_e_d_p [OF ep])
- apply (rule f, rule finite_deflation_Rep_fin_defl)
- done
+ have 1: "finite_deflation (e oo f\<cdot>(Rep_fin_defl a) oo p)" for a
+ proof -
+ have "finite_deflation (f\<cdot>(Rep_fin_defl a))"
+ using finite_deflation_Rep_fin_defl by (rule f)
+ with ep show ?thesis
+ by (rule ep_pair.finite_deflation_e_d_p)
+ qed
show ?thesis
by (induct A rule: defl.principal_induct, simp)
(simp only: defl_fun1_def
@@ -259,11 +256,13 @@
finite_deflation (f\<cdot>a\<cdot>b)"
shows "cast\<cdot>(defl_fun2 e p f\<cdot>A\<cdot>B) = e oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo p"
proof -
- have 1: "\<And>a b. finite_deflation
- (e oo f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo p)"
- apply (rule ep_pair.finite_deflation_e_d_p [OF ep])
- apply (rule f, (rule finite_deflation_Rep_fin_defl)+)
- done
+ have 1: "finite_deflation (e oo f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo p)" for a b
+ proof -
+ have "finite_deflation (f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b))"
+ using finite_deflation_Rep_fin_defl finite_deflation_Rep_fin_defl by (rule f)
+ with ep show ?thesis
+ by (rule ep_pair.finite_deflation_e_d_p)
+ qed
show ?thesis
apply (induct A rule: defl.principal_induct, simp)
apply (induct B rule: defl.principal_induct, simp)
--- a/src/HOL/HOLCF/Compact_Basis.thy Wed Dec 18 10:50:59 2024 +0100
+++ b/src/HOL/HOLCF/Compact_Basis.thy Sat Dec 28 16:38:57 2024 +0100
@@ -13,29 +13,28 @@
definition "pd_basis = {S::'a::bifinite compact_basis set. finite S \<and> S \<noteq> {}}"
typedef 'a::bifinite pd_basis = "pd_basis :: 'a compact_basis set set"
- unfolding pd_basis_def
- apply (rule_tac x="{_}" in exI)
- apply simp
- done
+proof
+ show "{a} \<in> ?pd_basis" for a
+ by (simp add: pd_basis_def)
+qed
lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)"
-by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
+using Rep_pd_basis [of u, unfolded pd_basis_def] by simp
lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}"
-by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
+using Rep_pd_basis [of u, unfolded pd_basis_def] by simp
text \<open>The powerdomain basis type is countable.\<close>
-lemma pd_basis_countable: "\<exists>f::'a::bifinite pd_basis \<Rightarrow> nat. inj f"
+lemma pd_basis_countable: "\<exists>f::'a::bifinite pd_basis \<Rightarrow> nat. inj f" (is "Ex ?P")
proof -
obtain g :: "'a compact_basis \<Rightarrow> nat" where "inj g"
using compact_basis.countable ..
- hence image_g_eq: "\<And>A B. g ` A = g ` B \<longleftrightarrow> A = B"
+ hence image_g_eq: "g ` A = g ` B \<longleftrightarrow> A = B" for A B
by (rule inj_image_eq_iff)
have "inj (\<lambda>t. set_encode (g ` Rep_pd_basis t))"
by (simp add: inj_on_def set_encode_eq image_g_eq Rep_pd_basis_inject)
- thus ?thesis by - (rule exI)
- (* FIXME: why doesn't ".." or "by (rule exI)" work? *)
+ thus ?thesis by (rule exI [of ?P])
qed
@@ -69,26 +68,30 @@
lemma PDPlus_absorb: "PDPlus t t = t"
unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_absorb)
-lemma pd_basis_induct1:
+lemma pd_basis_induct1 [case_names PDUnit PDPlus]:
assumes PDUnit: "\<And>a. P (PDUnit a)"
assumes PDPlus: "\<And>a t. P t \<Longrightarrow> P (PDPlus (PDUnit a) t)"
shows "P x"
-apply (induct x, unfold pd_basis_def, clarify)
-apply (erule (1) finite_ne_induct)
-apply (cut_tac a=x in PDUnit)
-apply (simp add: PDUnit_def)
-apply (drule_tac a=x in PDPlus)
-apply (simp add: PDUnit_def PDPlus_def
- Abs_pd_basis_inverse [unfolded pd_basis_def])
-done
+proof (induct x)
+ case (Abs_pd_basis y)
+ then have "finite y" and "y \<noteq> {}" by (simp_all add: pd_basis_def)
+ then show ?case
+ proof (induct rule: finite_ne_induct)
+ case (singleton x)
+ show ?case by (rule PDUnit [unfolded PDUnit_def])
+ next
+ case (insert x F)
+ from insert(4) have "P (PDPlus (PDUnit x) (Abs_pd_basis F))" by (rule PDPlus)
+ with insert(1,2) show ?case
+ by (simp add: PDUnit_def PDPlus_def Abs_pd_basis_inverse [unfolded pd_basis_def])
+ qed
+qed
-lemma pd_basis_induct:
+lemma pd_basis_induct [case_names PDUnit PDPlus]:
assumes PDUnit: "\<And>a. P (PDUnit a)"
assumes PDPlus: "\<And>t u. \<lbrakk>P t; P u\<rbrakk> \<Longrightarrow> P (PDPlus t u)"
shows "P x"
-apply (induct x rule: pd_basis_induct1)
-apply (rule PDUnit, erule PDPlus [OF PDUnit])
-done
+ by (induct x rule: pd_basis_induct1) (fact PDUnit, fact PDPlus [OF PDUnit])
subsection \<open>Fold operator\<close>
--- a/src/HOL/HOLCF/ConvexPD.thy Wed Dec 18 10:50:59 2024 +0100
+++ b/src/HOL/HOLCF/ConvexPD.thy Sat Dec 28 16:38:57 2024 +0100
@@ -92,10 +92,7 @@
apply fast
done
show "t \<le>\<natural> ?v" "u \<le>\<natural> ?w"
- apply (insert z)
- apply (simp_all add: convex_le_def upper_le_def lower_le_def Rep_PDPlus Rep_v Rep_w)
- apply fast+
- done
+ using z by (simp_all add: convex_le_def upper_le_def lower_le_def Rep_PDPlus Rep_v Rep_w) fast+
qed
lemma convex_le_induct [induct set: convex_le]:
@@ -104,17 +101,24 @@
assumes 3: "\<And>a b. a \<sqsubseteq> b \<Longrightarrow> P (PDUnit a) (PDUnit b)"
assumes 4: "\<And>t u v w. \<lbrakk>P t v; P u w\<rbrakk> \<Longrightarrow> P (PDPlus t u) (PDPlus v w)"
shows "P t u"
-using le apply (induct t arbitrary: u rule: pd_basis_induct)
-apply (erule rev_mp)
-apply (induct_tac u rule: pd_basis_induct1)
-apply (simp add: 3)
-apply (simp, clarify, rename_tac a b t)
-apply (subgoal_tac "P (PDPlus (PDUnit a) (PDUnit a)) (PDPlus (PDUnit b) t)")
-apply (simp add: PDPlus_absorb)
-apply (erule (1) 4 [OF 3])
-apply (drule convex_le_PDPlus_lemma, clarify)
-apply (simp add: 4)
-done
+ using le
+proof (induct t arbitrary: u rule: pd_basis_induct)
+ case (PDUnit a)
+ then show ?case
+ proof (induct u rule: pd_basis_induct1)
+ case (PDUnit b)
+ then show ?case by (simp add: 3)
+ next
+ case (PDPlus b t)
+ have "P (PDPlus (PDUnit a) (PDUnit a)) (PDPlus (PDUnit b) t)"
+ by (rule 4 [OF 3]) (use PDPlus in simp_all)
+ then show ?case by (simp add: PDPlus_absorb)
+ qed
+next
+ case PDPlus
+ from PDPlus(1,2) show ?case
+ using convex_le_PDPlus_lemma [OF PDPlus(3)] by (auto simp add: 4)
+qed
subsection \<open>Type definition\<close>
@@ -281,26 +285,34 @@
assumes unit: "\<And>x. P {x}\<natural>"
assumes insert: "\<And>x ys. \<lbrakk>P {x}\<natural>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<natural> \<union>\<natural> ys)"
shows "P (xs::'a::bifinite convex_pd)"
-apply (induct xs rule: convex_pd.principal_induct, rule P)
-apply (induct_tac a rule: pd_basis_induct1)
-apply (simp only: convex_unit_Rep_compact_basis [symmetric])
-apply (rule unit)
-apply (simp only: convex_unit_Rep_compact_basis [symmetric]
- convex_plus_principal [symmetric])
-apply (erule insert [OF unit])
-done
+proof (induct xs rule: convex_pd.principal_induct)
+ show "P (convex_principal a)" for a
+ proof (induct a rule: pd_basis_induct1)
+ case PDUnit
+ show ?case by (simp only: convex_unit_Rep_compact_basis [symmetric]) (rule unit)
+ next
+ case PDPlus
+ show ?case
+ by (simp only: convex_unit_Rep_compact_basis [symmetric] convex_plus_principal [symmetric])
+ (rule insert [OF unit PDPlus])
+ qed
+qed (rule P)
-lemma convex_pd_induct
- [case_names adm convex_unit convex_plus, induct type: convex_pd]:
+lemma convex_pd_induct [case_names adm convex_unit convex_plus, induct type: convex_pd]:
assumes P: "adm P"
assumes unit: "\<And>x. P {x}\<natural>"
assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs \<union>\<natural> ys)"
shows "P (xs::'a::bifinite convex_pd)"
-apply (induct xs rule: convex_pd.principal_induct, rule P)
-apply (induct_tac a rule: pd_basis_induct)
-apply (simp only: convex_unit_Rep_compact_basis [symmetric] unit)
-apply (simp only: convex_plus_principal [symmetric] plus)
-done
+proof (induct xs rule: convex_pd.principal_induct)
+ show "P (convex_principal a)" for a
+ proof (induct a rule: pd_basis_induct)
+ case PDUnit
+ then show ?case by (simp only: convex_unit_Rep_compact_basis [symmetric] unit)
+ next
+ case PDPlus
+ then show ?case by (simp only: convex_plus_principal [symmetric] plus)
+ qed
+qed (rule P)
subsection \<open>Monadic bind\<close>
--- a/src/HOL/HOLCF/LowerPD.thy Wed Dec 18 10:50:59 2024 +0100
+++ b/src/HOL/HOLCF/LowerPD.thy Sat Dec 28 16:38:57 2024 +0100
@@ -59,17 +59,33 @@
assumes 2: "\<And>t u a. P (PDUnit a) t \<Longrightarrow> P (PDUnit a) (PDPlus t u)"
assumes 3: "\<And>t u v. \<lbrakk>P t v; P u v\<rbrakk> \<Longrightarrow> P (PDPlus t u) v"
shows "P t u"
-using le
-apply (induct t arbitrary: u rule: pd_basis_induct)
-apply (erule rev_mp)
-apply (induct_tac u rule: pd_basis_induct)
-apply (simp add: 1)
-apply (simp add: lower_le_PDUnit_PDPlus_iff)
-apply (simp add: 2)
-apply (subst PDPlus_commute)
-apply (simp add: 2)
-apply (simp add: lower_le_PDPlus_iff 3)
-done
+ using le
+proof (induct t arbitrary: u rule: pd_basis_induct)
+ case (PDUnit a)
+ then show ?case
+ proof (induct u rule: pd_basis_induct)
+ case PDUnit
+ then show ?case by (simp add: 1)
+ next
+ case (PDPlus t u)
+ from PDPlus(3) consider (t) "PDUnit a \<le>\<flat> t" | (u) "PDUnit a \<le>\<flat> u"
+ by (auto simp: lower_le_PDUnit_PDPlus_iff)
+ then show ?case
+ proof cases
+ case t
+ then have "P (PDUnit a) t" by (rule PDPlus(1))
+ then show ?thesis by (rule 2)
+ next
+ case u
+ then have "P (PDUnit a) u" by (rule PDPlus(2))
+ then have "P (PDUnit a) (PDPlus u t)" by (rule 2)
+ then show ?thesis by (simp only: PDPlus_commute)
+ qed
+ qed
+next
+ case (PDPlus t t')
+ then show ?case by (simp add: lower_le_PDPlus_iff 3)
+qed
subsection \<open>Type definition\<close>
@@ -271,29 +287,42 @@
lemma lower_pd_induct1:
assumes P: "adm P"
assumes unit: "\<And>x. P {x}\<flat>"
- assumes insert:
- "\<And>x ys. \<lbrakk>P {x}\<flat>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<flat> \<union>\<flat> ys)"
+ assumes insert: "\<And>x ys. \<lbrakk>P {x}\<flat>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<flat> \<union>\<flat> ys)"
shows "P (xs::'a::bifinite lower_pd)"
-apply (induct xs rule: lower_pd.principal_induct, rule P)
-apply (induct_tac a rule: pd_basis_induct1)
-apply (simp only: lower_unit_Rep_compact_basis [symmetric])
-apply (rule unit)
-apply (simp only: lower_unit_Rep_compact_basis [symmetric]
- lower_plus_principal [symmetric])
-apply (erule insert [OF unit])
-done
+proof (induct xs rule: lower_pd.principal_induct)
+ have *: "P {Rep_compact_basis a}\<flat>" for a
+ by (rule unit)
+ show "P (lower_principal a)" for a
+ proof (induct a rule: pd_basis_induct1)
+ case PDUnit
+ from * show ?case
+ by (simp only: lower_unit_Rep_compact_basis [symmetric])
+ next
+ case (PDPlus a t)
+ with * have "P ({Rep_compact_basis a}\<flat> \<union>\<flat> lower_principal t)"
+ by (rule insert)
+ then show ?case
+ by (simp only: lower_unit_Rep_compact_basis [symmetric] lower_plus_principal [symmetric])
+ qed
+qed (rule P)
-lemma lower_pd_induct
- [case_names adm lower_unit lower_plus, induct type: lower_pd]:
+lemma lower_pd_induct [case_names adm lower_unit lower_plus, induct type: lower_pd]:
assumes P: "adm P"
assumes unit: "\<And>x. P {x}\<flat>"
assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs \<union>\<flat> ys)"
shows "P (xs::'a::bifinite lower_pd)"
-apply (induct xs rule: lower_pd.principal_induct, rule P)
-apply (induct_tac a rule: pd_basis_induct)
-apply (simp only: lower_unit_Rep_compact_basis [symmetric] unit)
-apply (simp only: lower_plus_principal [symmetric] plus)
-done
+proof (induct xs rule: lower_pd.principal_induct)
+ show "P (lower_principal a)" for a
+ proof (induct a rule: pd_basis_induct)
+ case PDUnit
+ then show ?case
+ by (simp only: lower_unit_Rep_compact_basis [symmetric] unit)
+ next
+ case PDPlus
+ then show ?case
+ by (simp only: lower_plus_principal [symmetric] plus)
+ qed
+qed (rule P)
subsection \<open>Monadic bind\<close>
--- a/src/HOL/HOLCF/UpperPD.thy Wed Dec 18 10:50:59 2024 +0100
+++ b/src/HOL/HOLCF/UpperPD.thy Sat Dec 28 16:38:57 2024 +0100
@@ -58,16 +58,33 @@
assumes 2: "\<And>t u a. P t (PDUnit a) \<Longrightarrow> P (PDPlus t u) (PDUnit a)"
assumes 3: "\<And>t u v. \<lbrakk>P t u; P t v\<rbrakk> \<Longrightarrow> P t (PDPlus u v)"
shows "P t u"
-using le apply (induct u arbitrary: t rule: pd_basis_induct)
-apply (erule rev_mp)
-apply (induct_tac t rule: pd_basis_induct)
-apply (simp add: 1)
-apply (simp add: upper_le_PDPlus_PDUnit_iff)
-apply (simp add: 2)
-apply (subst PDPlus_commute)
-apply (simp add: 2)
-apply (simp add: upper_le_PDPlus_iff 3)
-done
+ using le
+proof (induct u arbitrary: t rule: pd_basis_induct)
+ case (PDUnit a)
+ then show ?case
+ proof (induct t rule: pd_basis_induct)
+ case PDUnit
+ then show ?case by (simp add: 1)
+ next
+ case (PDPlus t u)
+ from PDPlus(3) consider (t) "t \<le>\<sharp> PDUnit a" | (u) "u \<le>\<sharp> PDUnit a"
+ by (auto simp: upper_le_PDPlus_PDUnit_iff)
+ then show ?case
+ proof cases
+ case t
+ then have "P t (PDUnit a)" by (rule PDPlus(1))
+ then show ?thesis by (rule 2)
+ next
+ case u
+ then have "P u (PDUnit a)" by (rule PDPlus(2))
+ then have "P (PDPlus u t) (PDUnit a)" by (rule 2)
+ then show ?thesis by (simp only: PDPlus_commute)
+ qed
+ qed
+next
+ case (PDPlus t t' u)
+ then show ?case by (simp add: upper_le_PDPlus_iff 3)
+qed
subsection \<open>Type definition\<close>
@@ -267,26 +284,41 @@
assumes unit: "\<And>x. P {x}\<sharp>"
assumes insert: "\<And>x ys. \<lbrakk>P {x}\<sharp>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<sharp> \<union>\<sharp> ys)"
shows "P (xs::'a::bifinite upper_pd)"
-apply (induct xs rule: upper_pd.principal_induct, rule P)
-apply (induct_tac a rule: pd_basis_induct1)
-apply (simp only: upper_unit_Rep_compact_basis [symmetric])
-apply (rule unit)
-apply (simp only: upper_unit_Rep_compact_basis [symmetric]
- upper_plus_principal [symmetric])
-apply (erule insert [OF unit])
-done
+proof (induct xs rule: upper_pd.principal_induct)
+ have *: "P {Rep_compact_basis a}\<sharp>" for a
+ by (rule unit)
+ show "P (upper_principal a)" for a
+ proof (induct a rule: pd_basis_induct1)
+ case (PDUnit a)
+ with * show ?case
+ by (simp only: upper_unit_Rep_compact_basis [symmetric])
+ next
+ case (PDPlus a t)
+ with * have "P ({Rep_compact_basis a}\<sharp> \<union>\<sharp> upper_principal t)"
+ by (rule insert)
+ then show ?case
+ by (simp only: upper_unit_Rep_compact_basis [symmetric]
+ upper_plus_principal [symmetric])
+ qed
+qed (rule P)
-lemma upper_pd_induct
- [case_names adm upper_unit upper_plus, induct type: upper_pd]:
+lemma upper_pd_induct [case_names adm upper_unit upper_plus, induct type: upper_pd]:
assumes P: "adm P"
assumes unit: "\<And>x. P {x}\<sharp>"
assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs \<union>\<sharp> ys)"
shows "P (xs::'a::bifinite upper_pd)"
-apply (induct xs rule: upper_pd.principal_induct, rule P)
-apply (induct_tac a rule: pd_basis_induct)
-apply (simp only: upper_unit_Rep_compact_basis [symmetric] unit)
-apply (simp only: upper_plus_principal [symmetric] plus)
-done
+proof (induct xs rule: upper_pd.principal_induct)
+ show "P (upper_principal a)" for a
+ proof (induct a rule: pd_basis_induct)
+ case PDUnit
+ then show ?case
+ by (simp only: upper_unit_Rep_compact_basis [symmetric] unit)
+ next
+ case PDPlus
+ then show ?case
+ by (simp only: upper_plus_principal [symmetric] plus)
+ qed
+qed (rule P)
subsection \<open>Monadic bind\<close>
--- a/src/HOL/Nat.thy Wed Dec 18 10:50:59 2024 +0100
+++ b/src/HOL/Nat.thy Sat Dec 28 16:38:57 2024 +0100
@@ -119,14 +119,6 @@
declare nat.sel[code del]
hide_const (open) Nat.pred \<comment> \<open>hide everything related to the selector\<close>
-hide_fact
- nat.case_eq_if
- nat.collapse
- nat.expand
- nat.sel
- nat.exhaust_sel
- nat.split_sel
- nat.split_sel_asm
lemma nat_exhaust [case_names 0 Suc, cases type: nat]:
"(y = 0 \<Longrightarrow> P) \<Longrightarrow> (\<And>nat. y = Suc nat \<Longrightarrow> P) \<Longrightarrow> P"
--- a/src/HOL/Tools/ATP/atp_problem.ML Wed Dec 18 10:50:59 2024 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML Sat Dec 28 16:38:57 2024 +0100
@@ -801,8 +801,8 @@
end
fun lines_of_atp_problem format ord_info problem =
- "% This file was generated by Isabelle (most likely Sledgehammer)\n\
- \% " ^ timestamp () ^ "\n" ::
+ "% This file was generated by Isabelle (most likely Sledgehammer)" ::
+ timestamp () ::
(case format of
DFG poly => dfg_lines poly ord_info
| _ => tptp_lines format) problem
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Dec 18 10:50:59 2024 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sat Dec 28 16:38:57 2024 +0100
@@ -494,23 +494,20 @@
val hash = SHA1.rep (SHA1.digest arg)
val file = cache_dir + Path.explode hash
in
- if File.is_file file then
+ (case try File.read file of
+ NONE =>
+ let val result = f arg in
+ File.write file result;
+ result
+ end
+ | SOME s =>
let
val () =
if verbose then
writeln ("Found problem with key " ^ hash ^ " in cache.")
else
()
- in
- File.read file
- end
- else
- let
- val result = f arg
- in
- File.write file result;
- result
- end
+ in s end)
end
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Wed Dec 18 10:50:59 2024 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Sat Dec 28 16:38:57 2024 +0100
@@ -145,10 +145,13 @@
val prob_path =
if problem_dest_dir = "" then
File.tmp_path problem_file_name
- else if File.exists (Path.explode problem_dest_dir) then
- Path.explode problem_dest_dir + problem_file_name
else
- error ("No such directory: " ^ quote problem_dest_dir)
+ let val problem_dest_dir_path = Path.explode problem_dest_dir in
+ if File.is_dir problem_dest_dir_path then
+ problem_dest_dir_path + problem_file_name
+ else
+ error ("No such directory: " ^ quote problem_dest_dir)
+ end
val executable =
(case find_first (fn var => getenv var <> "") (fst exec) of
@@ -233,9 +236,9 @@
else
let val res = Isabelle_System.bash_process (Bash.script command |> Bash.redirect)
in Process_Result.out res end
- (* Hackish: This removes the two first lines that contain call-specific information
- such as timestamp. *)
- val arg = cat_lines (drop 2 lines_of_atp_problem)
+ (* Hackish: This removes the first two lines that contain call-specific information
+ such as a timestamp. *)
+ val arg = cat_lines (command :: drop 2 lines_of_atp_problem)
in
Timing.timing (memoize_fun_call f) arg
end
@@ -286,14 +289,15 @@
too. *)
fun clean_up () = if problem_dest_dir = "" then (try File.rm prob_path; ()) else ()
fun export (_, (output, _, _, _, _, _, _, _), _) =
- let val proof_dest_dir_path = Path.explode proof_dest_dir in
- if proof_dest_dir = "" then
- Output.system_message "don't export proof"
- else if File.exists proof_dest_dir_path then
- File.write (proof_dest_dir_path + proof_file_name) output
- else
- error ("No such directory: " ^ quote proof_dest_dir)
- end
+ if proof_dest_dir = "" then
+ Output.system_message "don't export proof"
+ else
+ let val proof_dest_dir_path = Path.explode proof_dest_dir in
+ if File.is_dir proof_dest_dir_path then
+ File.write (proof_dest_dir_path + proof_file_name) output
+ else
+ error ("No such directory: " ^ quote proof_dest_dir)
+ end
val ((_, pool, lifted, sym_tab),
(_, run_time, used_from, atp_problem, tstplike_proof, atp_proof,
--- a/src/Pure/Admin/component_fonts.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Pure/Admin/component_fonts.scala Sat Dec 28 16:38:57 2024 +0100
@@ -24,6 +24,8 @@
0x201c, // double quote
0x201d, // double quote
0x201e, // double quote
+ 0x2022, // regular bullet
+ 0x2023, // triangular bullet
0x2039, // single guillemet
0x203a, // single guillemet
0x204b, // FOOTNOTE
@@ -58,7 +60,6 @@
0x2016, // big parallel
0x2020, // dagger
0x2021, // double dagger
- 0x2022, // bullet
0x2026, // ellipsis
0x2030, // perthousand
0x2032, // minute
--- a/src/Pure/Admin/component_llncs.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Pure/Admin/component_llncs.scala Sat Dec 28 16:38:57 2024 +0100
@@ -59,7 +59,7 @@
/* README */
- File.change(component_dir.path + README_md)(_.replace(" ", "\u00a0"))
+ File.change(component_dir.path + README_md)(_.replace(" ", HTML.space))
File.write(component_dir.README,
"""This is the Springer LaTeX LNCS style for authors from
--- a/src/Pure/Concurrent/delay.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Pure/Concurrent/delay.scala Sat Dec 28 16:38:57 2024 +0100
@@ -20,7 +20,7 @@
final class Delay private(first: Boolean, delay: => Time, log: Logger, event: => Unit) {
private var running: Option[Event_Timer.Request] = None
- private def run: Unit = {
+ private def run(): Unit = {
val do_run = synchronized {
if (running.isDefined) { running = None; true } else false
}
@@ -37,8 +37,9 @@
case Some(request) => if (first) false else { request.cancel(); true }
case None => true
}
- if (new_run)
- running = Some(Event_Timer.request(Time.now() + delay)(run))
+ if (new_run) {
+ running = Some(Event_Timer.request(Time.now() + delay)(run()))
+ }
}
def revoke(msg: String = ""): Unit = synchronized {
@@ -55,7 +56,7 @@
case Some(request) =>
val alt_time = Time.now() + alt_delay
if (request.time < alt_time && request.cancel()) {
- running = Some(Event_Timer.request(alt_time)(run))
+ running = Some(Event_Timer.request(alt_time)(run()))
}
case None =>
}
--- a/src/Pure/Concurrent/event_timer.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Pure/Concurrent/event_timer.scala Sat Dec 28 16:38:57 2024 +0100
@@ -25,7 +25,7 @@
}
def request(time: Time, repeat: Option[Time] = None)(event: => Unit): Request = {
- val task = new TimerTask { def run: Unit = event }
+ val task = new TimerTask { def run(): Unit = event }
repeat match {
case None => event_timer.schedule(task, new JDate(time.ms))
case Some(rep) => event_timer.schedule(task, new JDate(time.ms), rep.ms)
--- a/src/Pure/GUI/gui.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Pure/GUI/gui.scala Sat Dec 28 16:38:57 2024 +0100
@@ -67,6 +67,89 @@
}
+ /* style */
+
+ class Style {
+ def enclose(body: String): String = body
+ def make_text(str: String): String = str
+ def make_bold(str: String): String = str
+ def enclose_text(str: String): String = enclose(make_text(str))
+ def enclose_bold(str: String): String = enclose(make_bold(str))
+ def spaces(n: Int): String = Symbol.spaces(n)
+ }
+
+ class Style_HTML extends Style {
+ override def enclose(body: String): String = enclose_style("", body)
+ override def make_text(str: String): String = HTML.output(str)
+ override def make_bold(str: String): String = "<b>" + make_text(str) + "</b>"
+ override def spaces(n: Int): String = HTML.spaces(n)
+
+ def enclose_style(style: String, body: String): String =
+ if (style.isEmpty) {
+ Library.string_builder(body.length + 13) { s =>
+ s ++= "<html>"
+ s ++= body
+ s ++= "</html>"
+ }
+ }
+ else {
+ Library.string_builder(style.length + body.length + 35) { s =>
+ s ++= "<html><span style=\""
+ s ++= style
+ s ++= "\">"
+ s ++= body
+ s ++= "</span></html>"
+ }
+ }
+
+ def regular_bullet: String = "\u2022"
+ def triangular_bullet: String = "\u2023"
+ }
+
+ abstract class Style_Symbol extends Style {
+ def bold: String
+ override def make_bold(str: String): String =
+ Symbol.iterator(str)
+ .flatMap(s => if (Symbol.is_controllable(s)) List(bold, s) else List(s))
+ .mkString
+ }
+
+ object Style_Plain extends Style { override def toString: String = "plain" }
+
+ object Style_HTML extends Style_HTML { override def toString: String = "html" }
+
+ object Style_Symbol_Encoded extends Style_Symbol {
+ override def toString: String = "symbol_encoded"
+ override def bold: String = Symbol.bold
+ }
+
+ object Style_Symbol_Decoded extends Style_Symbol {
+ override def toString: String = "symbol_decoded"
+ override def bold: String = Symbol.bold_decoded
+ }
+
+
+ /* named items */
+
+ sealed case class Name(
+ name: String,
+ kind: String = "",
+ prefix: String = "",
+ style: Style = Style_Plain
+ ) {
+ def set_style(new_style: Style): Name = copy(style = new_style)
+
+ override def toString: String = {
+ val a = kind.nonEmpty
+ val b = name.nonEmpty
+ style.make_text(prefix) +
+ if_proper(a || b,
+ if_proper(prefix, ": ") + if_proper(kind, style.make_bold(kind)) +
+ if_proper(a && b, " ") + if_proper(b, style.make_text(quote(name))))
+ }
+ }
+
+
/* simple dialogs */
def scrollable_text(
@@ -263,7 +346,7 @@
def tooltip_lines(text: String): String =
if (text == null || text == "") null
- else "<html>" + HTML.output(text) + "</html>"
+ else Style_HTML.enclose_text(text)
/* icon */
--- a/src/Pure/General/completion.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Pure/General/completion.scala Sat Dec 28 16:38:57 2024 +0100
@@ -198,8 +198,7 @@
if (kind == "") (name, quote(decode(name)))
else
(Long_Name.qualify(kind, name),
- Word.implode(Word.explode('_', kind)) +
- (if (xname == name) "" else " " + quote(decode(name))))
+ Word.informal(kind) + (if (xname == name) "" else " " + quote(decode(name))))
} yield {
val description = List(xname1, "(" + descr_name + ")")
val replacement =
--- a/src/Pure/General/html.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Pure/General/html.scala Sat Dec 28 16:38:57 2024 +0100
@@ -7,11 +7,28 @@
package isabelle
+import java.awt.Color
+import java.util.Locale
+
import org.jsoup.nodes.{Entities => Jsoup_Entities, Document => Jsoup_Document}
import org.jsoup.Jsoup
object HTML {
+ /* spaces (non-breaking) */
+
+ val space = "\u00a0"
+
+ private val static_spaces = space * 100
+
+ def spaces(n: Int): String = {
+ require(n >= 0, "negative spaces")
+ if (n == 0) ""
+ else if (n < static_spaces.length) static_spaces.substring(0, n)
+ else space * n
+ }
+
+
/* attributes */
class Attribute(val name: String, value: String) {
@@ -97,6 +114,21 @@
def script_file(href: String): XML.Elem = XML.Elem(Markup("script", List("src" -> href)), Nil)
def script_file(path: Path): XML.Elem = script_file(Url.print_file(path.file))
+ def color(c: Color): String = {
+ val r = Integer.valueOf(c.getRed)
+ val g = Integer.valueOf(c.getGreen)
+ val b = Integer.valueOf(c.getBlue)
+ c.getAlpha match {
+ case 255 => String.format(Locale.ROOT, "rgb(%d,%d,%d)", r, g, b)
+ case a =>
+ String.format(Locale.ROOT, "rgba(%d,%d,%d,%.2f)", r, g, b,
+ java.lang.Double.valueOf(a.toDouble / 255))
+ }
+ }
+
+ def color_property(c: Color): String = "color: " + color(c)
+ def background_property(c: Color): String = "background: " + color(c)
+
/* href */
--- a/src/Pure/General/latex.ML Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Pure/General/latex.ML Sat Dec 28 16:38:57 2024 +0100
@@ -247,10 +247,10 @@
val markup_indent = markup_macro "isaindent";
val markup_latex =
Symtab.make
- [(Markup.commandN, markup_macro "isacommand"),
- (Markup.keyword1N, markup_macro "isacommand"),
- (Markup.keyword2N, markup_macro "isakeyword"),
- (Markup.keyword3N, markup_macro "isacommand"),
+ [(Markup.commandN, markup_macro "isakeywordONE"),
+ (Markup.keyword1N, markup_macro "isakeywordONE"),
+ (Markup.keyword2N, markup_macro "isakeywordTWO"),
+ (Markup.keyword3N, markup_macro "isakeywordTHREE"),
(Markup.tclassN, markup_macro "isatclass"),
(Markup.tconstN, markup_macro "isatconst"),
(Markup.tfreeN, markup_macro "isatfree"),
--- a/src/Pure/General/mailman.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Pure/General/mailman.scala Sat Dec 28 16:38:57 2024 +0100
@@ -20,27 +20,27 @@
private val standard_name: Map[String, String] =
Map(
- "121171528@qq.com" -> "Guo Fan\n121171528@qq.com",
+ "121171528:qq/com" -> "Guo Fan\n121171528:qq/com",
"Aman Pohjola, Johannes (Data61, Kensington NSW)" -> "Johannes Aman Pohjola",
"Andrei de AraÃjo Formiga" -> "Andrei de Araujo Formiga",
- "Benedikt.AHRENS@unice.fr" -> "Benedikt Ahrens\nBenedikt.AHRENS@unice.fr",
+ "Benedikt/AHRENS:unice/fr" -> "Benedikt Ahrens\nBenedikt/AHRENS:unice/fr",
"Berg, Nils Erik" -> "Nils Erik Berg",
- "Berger U." -> "Ulrich Berger",
+ "Berger U/" -> "Ulrich Berger",
"Bisping, Benjamin" -> "Benjamin Bisping",
- "Blanchette, J.C." -> "Jasmin Christian Blanchette",
+ "Blanchette, J/C/" -> "Jasmin Christian Blanchette",
"Buday Gergely István" -> "Gergely Buday",
- "CALaF1UJ9Uy0vGCu4WkBmbfuPDxG7nFm8hfeCMP+O3g7_5CQ0Bw@mail.gmail.com" -> "",
- "CRACIUN F." -> "Florin Craciun",
+ "CALaF1UJ9Uy0vGCu4WkBmbfuPDxG7nFm8hfeCMP+O3g7_5CQ0Bw:mail/gmail/com" -> "",
+ "CRACIUN F/" -> "Florin Craciun",
"Carsten Schuermann" -> "Carsten Schürmann",
"Chris" -> "",
"Christoph Lueth" -> "Christoph Lüth",
"Claude Marche" -> "Claude Marché",
"Daniel StÃwe" -> "Daniel Stüwe",
- "Daniel.Matichuk@data61.csiro.au" -> "Daniel Matichuk\nDaniel.Matichuk@data61.csiro.au",
- "Daniel.Matichuk@nicta.com.au" -> "Daniel Matichuk\nDaniel.Matichuk@nicta.com.au",
+ "Daniel/Matichuk:data61/csiro/au" -> "Daniel Matichuk\nDaniel/Matichuk:data61/csiro/au",
+ "Daniel/Matichuk:nicta/com/au" -> "Daniel Matichuk\nDaniel/Matichuk:nicta/com/au",
"David MENTRE" -> "David MENTRÉ",
"Dey, Katie" -> "Katie Dey",
- "Dr. Brendan Patrick Mahony" -> "Brendan Mahony",
+ "Dr/ Brendan Patrick Mahony" -> "Brendan Mahony",
"Farn" -> "Farn Wang",
"Farquhar, Colin I" -> "Colin Farquhar",
"Fernandez, Matthew" -> "Matthew Fernandez",
@@ -50,7 +50,7 @@
"Francisco Jose CHAVES ALONSO" -> "Francisco Jose Chaves Alonso",
"Frederic Tuong (Dr)" -> "Frederic Tuong",
"Fulya" -> "Fulya Horozal",
- "George K." -> "George Karabotsos",
+ "George K/" -> "George Karabotsos",
"Gidon Ernst" -> "Gidon ERNST",
"Gransden, Thomas" -> "Thomas Gransden",
"Hans-JÃrg Schurr" -> "Hans-Jörg Schurr",
@@ -58,7 +58,7 @@
"Hitoshi Ohsaki (RTA publicity chair)" -> "Hitoshi Ohsaki",
"Häuselmann Rafael" -> "Rafael Häuselmann",
"Isabelle" -> "",
- "J. Juhas (TUM)" -> "Jonatan Juhas",
+ "J/ Juhas (TUM)" -> "Jonatan Juhas",
"Jackson, Vincent (Data61, Kensington NSW)" -> "Vincent Jackson",
"Janney, Mark-P26816" -> "Mark Janney",
"Jean François Molderez" -> "Jean-François Molderez",
@@ -70,7 +70,7 @@
"Klein, Gerwin (Data61, Kensington NSW)" -> "Gerwin Klein",
"Kobayashi, Hidetsune" -> "Hidetsune Kobayashi",
"Kylie Williams (IND)" -> "Kylie Williams",
- "Laarman, A.W." -> "A.W. Laarman",
+ "Laarman, A/W/" -> "A/W/ Laarman",
"Laurent Thery" -> "Laurent Théry",
"Li, Chanjuan" -> "Li Chanjuan",
"Lochbihler Andreas" -> "Andreas Lochbihler",
@@ -86,7 +86,7 @@
"Marmsoler, Diego" -> "Diego Marmsoler",
"Martin Klebermass" -> "Martin Klebermaß",
"Martyn Johnson via RT" -> "",
- "Mathias.Fleury@ens-rennes.fr" -> "Mathias Fleury\nmathias.fleury12@gmail.com",
+ "Mathias/Fleury:ens-rennes/fr" -> "Mathias Fleury\nmathias/fleury12:gmail/com",
"Matthew" -> "",
"Matthews, John R" -> "John Matthews",
"McCarthy, Jim (C3ID)" -> "Jim McCarthy",
@@ -94,10 +94,10 @@
"Michael FÃrber" -> "Michael Färber",
"Michel" -> "",
"Miranda, Brando" -> "Brando Miranda",
- "Moscato, Mariano M. \\(LARC-D320\\)\\[NATIONAL INSTITUTE OF AEROSPACE\\]" -> "Mariano M. Moscato",
+ "Moscato, Mariano M/ \\(LARC-D320\\)\\[NATIONAL INSTITUTE OF AEROSPACE\\]" -> "Mariano M/ Moscato",
"Mr Julian Fell" -> "Julian Fell",
"Mueller Peter" -> "Peter Müller",
- "Munoz, Cesar Augusto (LARC-D320)" -> "Cesar A. Munoz",
+ "Munoz, Cesar Augusto (LARC-D320)" -> "Cesar A/ Munoz",
"Nadel, Alexander" -> "Alexander Nadel",
"Nagashima, Yutaka" -> "Yutaka Nagashima",
"Norrish, Michael (Data61, Acton)" -> "Michael Norrish",
@@ -109,34 +109,34 @@
"PAQUI LUCIO" -> "Paqui Lucio",
"Pal, Abhik" -> "Abhik Pal",
"Pasupuleti, Vijay" -> "Vijay Pasupuleti",
- "Peter Vincent Homeier" -> "Peter V. Homeier",
+ "Peter Vincent Homeier" -> "Peter V/ Homeier",
"Peter" -> "",
"Philipp Ruemmer" -> "Philipp Rümmer",
"Philipp RÃmmer" -> "Philipp Rümmer",
"Piete Brooks via RT" -> "",
"RTA publicity chair" -> "",
- "Raamsdonk, F. van" -> "Femke van Raamsdonk",
+ "Raamsdonk, F/ van" -> "Femke van Raamsdonk",
"Raul Gutierrez" -> "Raúl Gutiérrez",
"Renà Thiemann" -> "René Thiemann",
- "Ridgway, John V. E." -> "John V. E. Ridgway",
- "Roggenbach M." -> "Markus Roggenbach",
+ "Ridgway, John V/ E/" -> "John V/ E/ Ridgway",
+ "Roggenbach M/" -> "Markus Roggenbach",
"Rosu, Grigore" -> "Grigore Rosu",
"Rozman, Mihaela" -> "Mihaela Rozman",
- "Schmaltz, J." -> "Julien Schmaltz",
- "Serguei A. Mokhov on behalf of PST-11" -> "Serguei A. Mokhov",
- "Serguei Mokhov" -> "Serguei A. Mokhov",
+ "Schmaltz, J/" -> "Julien Schmaltz",
+ "Serguei A/ Mokhov on behalf of PST-11" -> "Serguei A/ Mokhov",
+ "Serguei Mokhov" -> "Serguei A/ Mokhov",
"Shumeiko, Igor" -> "Igor Shumeiko",
"Siek, Jeremy" -> "Jeremy Siek",
- "Silvio.Ranise@loria.fr" -> "Silvio Ranise\nSilvio.Ranise@loria.fr",
+ "Silvio/Ranise:loria/fr" -> "Silvio Ranise\nSilvio/Ranise:loria/fr",
"Siu, Tony" -> "Tony Siu",
"Stüber, Sebastian" -> "Sebastian Stüber",
"Thiemann, Rene" -> "René Thiemann",
"Thiemann, René" -> "René Thiemann",
"Thomas Arthur Leck Sewell" -> "Thomas Sewell",
"Thomas Goethel" -> "Thomas Göthel",
- "Thomas.Sewell@data61.csiro.au" -> "Thomas Sewell\nThomas.Sewell@data61.csiro.au",
+ "Thomas/Sewell:data61/csiro/au" -> "Thomas Sewell\nThomas/Sewell:data61/csiro/au",
"Tjark Weber via RT" -> "Tjark Weber",
- "Toby.Murray@data61.csiro.au" -> "Toby Murray\nToby.Murray@data61.csiro.au",
+ "Toby/Murray:data61/csiro/au" -> "Toby Murray\nToby/Murray:data61/csiro/au",
"Urban, Christian" -> "Christian Urban",
"Ursula Eschbach" -> "",
"Van Staden Stephan" -> "Stephan van Staden",
@@ -154,57 +154,64 @@
"chen kun" -> "Chen Kun",
"chunhan wu" -> "Chunhan Wu",
"daniel de la concepción sáez" -> "Daniel de la Concepción Sáez",
- "daniel.luckhardt@mathematik.uni-goettingen.de" -> "Logiker@gmx.net",
+ "daniel/luckhardt:mathematik/uni-goettingen/de" -> "Logiker:gmx/net",
"david streader" -> "David Streader",
- "eschbach@in.tum.de" -> "",
- "f.rabe@jacobs-university.de" -> "florian.rabe@fau.de",
- "florian@haftmann-online.de" -> "haftmann@in.tum.de",
- "fredegar@haftmann-online.de" -> "haftmann@in.tum.de",
- "gallais @ ensl.org" -> "Guillaume Allais",
+ "eschbach:in/tum/de" -> "",
+ "f/rabe:jacobs-university/de" -> "florian/rabe:fau/de",
+ "florian:haftmann-online/de" -> "haftmann:in/tum/de",
+ "fredegar:haftmann-online/de" -> "haftmann:in/tum/de",
+ "gallais : ensl/org" -> "Guillaume Allais",
"geng chen" -> "Geng Chen",
- "henning.seidler" -> "Henning Seidler",
+ "henning/seidler" -> "Henning Seidler",
"hkb" -> "Hidetsune Kobayashi",
- "jobs-pm@inf.ethz.ch" -> "",
- "julien@RadboudUniversity" -> "",
+ "jobs-pm:inf/ethz/ch" -> "",
+ "julien:RadboudUniversity" -> "",
"jun sun" -> "Jun Sun",
- "jwang whu.edu.cn (jwang)" -> "jwang",
+ "jwang whu/edu/cn (jwang)" -> "jwang",
"kostas pouliasis" -> "Kostas Pouliasis",
- "kristof.teichel@ptb.de" -> "Kristof Teichel\nkristof.teichel@ptb.de",
+ "kristof/teichel:ptb/de" -> "Kristof Teichel\nkristof/teichel:ptb/de",
"lucas cavalcante" -> "Lucas Cavalcante",
"mahmoud abdelazim" -> "Mahmoud Abdelazim",
"manish surolia" -> "Manish Surolia",
"mantel" -> "Heiko Mantel",
"marco caminati" -> "Marco Caminati",
- "mathias.fleury@ens-rennes.fr" -> "Mathias Fleury\nmathias.fleury12@gmail.com",
- "merz@loria.fr" -> "stephan.merz@loria.fr",
+ "mathias/fleury:ens-rennes/fr" -> "Mathias Fleury\nmathias/fleury12:gmail/com",
+ "merz:loria/fr" -> "stephan/merz:loria/fr",
"michel levy" -> "Michel Levy",
- "michel.levy2009@laposte.net" -> "Michel Levy\nmichel.levy2009@laposte.net",
+ "michel/levy2009:laposte/net" -> "Michel Levy\nmichel/levy2009:laposte/net",
"nemouchi" -> "Yakoub Nemouchi",
"noam neer" -> "Noam Neer",
"olfa mraihi" -> "Olfa Mraihi",
- "pathsnottakenworkshop@gmail.com" -> "Leo Freitas\nleo.freitas@newcastle.ac.uk",
+ "pathsnottakenworkshop:gmail/com" -> "Leo Freitas\nleo/freitas:newcastle/ac/uk",
"patrick barlatier" -> "Patrick Barlatier",
"patrick dabou" -> "Patrick Dabou",
"paul zimmermann" -> "Paul Zimmermann",
- "popescu2@illinois.edu" -> "Andrei Popescu",
+ "popescu2:illinois/edu" -> "Andrei Popescu",
"recruiting" -> "",
- "recruiting@mais.informatik.tu-darmstadt.de" -> "",
+ "recruiting:mais/informatik/tu-darmstadt/de" -> "",
"roux cody" -> "Cody Roux",
"scott constable" -> "Scott Constable",
- "superuser@mattweidner.com" -> "Matthew Weidner\nsuperuser@mattweidner.com",
- "urban@math.lmu.de" -> "Christian Urban\nurban@math.lmu.de",
- "veronique.cortier@loria.fr" -> "Veronique.Cortier@loria.fr",
+ "superuser:mattweidner/com" -> "Matthew Weidner\nsuperuser:mattweidner/com",
+ "urban:math/lmu/de" -> "Christian Urban\nurban:math/lmu/de",
+ "veronique/cortier:loria/fr" -> "Veronique/Cortier:loria/fr",
"vikram singh" -> "Vikram Singh",
- "wenzelm@in.tum.de" -> "makarius@sketis.net",
- "werner@lix.polytechnique.fr" -> "Benjamin Werner\nwerner@lix.polytechnique.fr",
- "wmansky@cs.princeton.edu" -> "William Mansky\nwmansky@cs.princeton.edu",
- "y.nemouchi@ensbiotech.edu.dz" -> "Yakoub Nemouchi\ny.nemouchi@ensbiotech.edu.dz",
+ "wenzelm:in/tum/de" -> "makarius:sketis/net",
+ "werner:lix/polytechnique/fr" -> "Benjamin Werner\nwerner:lix/polytechnique/fr",
+ "wmansky:cs/princeton/edu" -> "William Mansky\nwmansky:cs/princeton/edu",
+ "y/nemouchi:ensbiotech/edu/dz" -> "Yakoub Nemouchi\ny/nemouchi:ensbiotech/edu/dz",
"ÐÑÐÐÐÑÐÐÐ ÐÐÐÐÐÐÐÑÐÐÐÑ ÐÐÐÑÐÐÐ" -> "",
- "∀X.Xπ - Tutorials about Proofs" -> "Bruno Woltzenlogel Paleo",
- ).withDefault(identity)
+ "∀X/Xπ - Tutorials about Proofs" -> "Bruno Woltzenlogel Paleo",
+ )
+
+ private def tune(s: String): String =
+ s.replace(64.toChar, 58.toChar).replace(46.toChar, 47.toChar)
+
+ private def untune(s: String): String =
+ s.replace(58.toChar, 64.toChar).replace(47.toChar, 46.toChar)
def standard_author_info(author_info: List[String]): List[String] =
- author_info.flatMap(s => split_lines(standard_name.getOrElse(s, s))).distinct
+ author_info.flatMap(s =>
+ split_lines(standard_name.get(tune(s)).map(untune).getOrElse(s))).distinct
sealed case class Message(
name: String,
--- a/src/Pure/General/symbol.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Pure/General/symbol.scala Sat Dec 28 16:38:57 2024 +0100
@@ -25,18 +25,17 @@
val space_char = ' '
val space = " "
- private val static_spaces_length = 4000
- private val static_spaces = space * static_spaces_length
+ private val static_spaces = space * 4000
def is_static_spaces(s: String): Boolean = {
val n = s.length
- n == 0 || n <= static_spaces_length && s(0) == space_char && s.forall(_ == space_char)
+ n == 0 || n <= static_spaces.length && s(0) == space_char && s.forall(_ == space_char)
}
def spaces(n: Int): String = {
require(n >= 0, "negative spaces")
if (n == 0) ""
- else if (n < static_spaces_length) static_spaces.substring(0, n)
+ else if (n < static_spaces.length) static_spaces.substring(0, n)
else space * n
}
--- a/src/Pure/General/word.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Pure/General/word.scala Sat Dec 28 16:38:57 2024 +0100
@@ -76,6 +76,8 @@
def explode(text: String): List[String] =
explode(Character.isWhitespace _, text)
+ def informal(text: String): String = implode(explode('_', text))
+
/* brackets */
--- a/src/Pure/Isar/keyword.ML Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Pure/Isar/keyword.ML Sat Dec 28 16:38:57 2024 +0100
@@ -80,6 +80,7 @@
val is_proof_open: keywords -> string -> bool
val is_proof_close: keywords -> string -> bool
val is_proof_asm: keywords -> string -> bool
+ val is_proof_asm_goal: keywords -> string -> bool
val is_improper: keywords -> string -> bool
val is_printed: keywords -> string -> bool
end;
@@ -289,6 +290,7 @@
val is_proof_close = command_category [qed, qed_script, qed_block, prf_close];
val is_proof_asm = command_category [prf_asm, prf_asm_goal];
+val is_proof_asm_goal = command_category [prf_asm_goal];
val is_improper = command_category [qed_script, prf_script, prf_script_goal, prf_script_asm_goal];
fun is_printed keywords = is_theory_goal keywords orf is_proof keywords;
--- a/src/Pure/PIDE/markup.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Pure/PIDE/markup.scala Sat Dec 28 16:38:57 2024 +0100
@@ -179,9 +179,9 @@
val EXPRESSION = "expression"
object Expression {
- def unapply(markup: Markup): Option[String] =
+ def unapply(markup: Markup): Option[(String, String)] =
markup match {
- case Markup(EXPRESSION, props) => Some(Kind.get(props))
+ case Markup(EXPRESSION, props) => Some((Kind.get(props), Name.get(props)))
case _ => None
}
@@ -238,7 +238,7 @@
def is_antiquotation: Boolean = name == Language.ANTIQUOTATION
def is_path: Boolean = name == Language.PATH
- def description: String = Word.implode(Word.explode('_', name))
+ def description: String = Word.informal(name)
}
--- a/src/Pure/PIDE/markup_kind.ML Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Pure/PIDE/markup_kind.ML Sat Dec 28 16:38:57 2024 +0100
@@ -17,6 +17,7 @@
val check_expression: Proof.context -> xstring * Position.T -> Markup.T
val setup_expression: binding -> Markup.T
val markup_item: Markup.T
+ val markup_syntax: Markup.T
val markup_mixfix: Markup.T
val markup_prefix: Markup.T
val markup_postfix: Markup.T
@@ -99,6 +100,8 @@
val markup_item = setup_expression (Binding.make ("item", \<^here>));
+val markup_syntax = setup_expression (Binding.make ("syntax", \<^here>));
+
val markup_mixfix = setup_notation (Binding.make ("mixfix", \<^here>));
val markup_prefix = setup_notation (Binding.make ("prefix", \<^here>));
val markup_postfix = setup_notation (Binding.make ("postfix", \<^here>));
--- a/src/Pure/PIDE/rendering.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Pure/PIDE/rendering.scala Sat Dec 28 16:38:57 2024 +0100
@@ -160,6 +160,10 @@
/* tooltips */
+ def gui_name(name: String, kind: String = "", prefix: String = ""): String =
+ GUI.Name(name, kind = Word.informal(kind), prefix = prefix,
+ style = GUI.Style_Symbol_Decoded).toString
+
def get_tooltip_description(name: String): Option[String] = tooltip_description.get(name)
private val tooltip_description =
@@ -670,30 +674,25 @@
case (info, Text.Info(r0, XML.Elem(Markup.Entity(kind, name), _)))
if kind != "" && kind != Markup.ML_DEF =>
- val kind1 = Word.implode(Word.explode('_', kind))
- val txt1 =
- if (name == "") kind1
- else if (kind1 == "") quote(name)
- else kind1 + " " + quote(name)
- val info1 = info.add_info_text(r0, txt1, ord = 2)
+ val txt = Rendering.gui_name(name, kind = kind)
+ val info1 = info.add_info_text(r0, txt, ord = 2)
Some(if (kind == Markup.COMMAND) info1.add_info(r0, XML.elem(Markup.TIMING)) else info1)
case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) =>
val file = perhaps_append_file(snapshot.node_name, name)
val info1 =
if (name == file) info
- else info.add_info_text(r0, "path " + quote(name))
- Some(info1.add_info_text(r0, "file " + quote(file)))
+ else info.add_info_text(r0, Rendering.gui_name(name, kind = "path"))
+ Some(info1.add_info_text(r0, Rendering.gui_name(file, kind = "file")))
case (info, Text.Info(r0, XML.Elem(Markup.Doc(name), _))) =>
- val text = "doc " + quote(name)
- Some(info.add_info_text(r0, text))
+ Some(info.add_info_text(r0, Rendering.gui_name(name, kind = "doc")))
case (info, Text.Info(r0, XML.Elem(Markup.Url(name), _))) =>
- Some(info.add_info_text(r0, "URL " + quote(name)))
+ Some(info.add_info_text(r0, Rendering.gui_name(name, kind = "URL")))
case (info, Text.Info(r0, XML.Elem(Markup.Command_Span(span), _))) =>
- Some(info.add_info_text(r0, "command span " + quote(span.name)))
+ Some(info.add_info_text(r0, Rendering.gui_name(span.name, kind = Markup.COMMAND_SPAN)))
case (info, Text.Info(r0, XML.Elem(Markup(name, _), body)))
if name == Markup.SORTING || name == Markup.TYPING =>
@@ -716,18 +715,11 @@
Some(info.add_info_text(r0, "language: " + lang.description))
case (info, Text.Info(r0, XML.Elem(Markup.Notation(kind, name), _))) =>
- val a = kind.nonEmpty
- val b = name.nonEmpty
- val k = Word.implode(Word.explode('_', kind))
- val description =
- if (!a && !b) "notation"
- else "notation: " + k + if_proper(a && b, " ") + if_proper(b, quote(name))
+ val description = Rendering.gui_name(name, kind = kind, prefix = Markup.NOTATION)
Some(info.add_info_text(r0, description, ord = 1))
- case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind), _))) =>
- val description =
- if (kind.isEmpty) "expression"
- else "expression: " + Word.implode(Word.explode('_', kind))
+ case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind, name), _))) =>
+ val description = Rendering.gui_name(name, kind = kind, prefix = Markup.EXPRESSION)
Some(info.add_info_text(r0, description, ord = 1))
case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
--- a/src/Pure/ROOT.ML Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Pure/ROOT.ML Sat Dec 28 16:38:57 2024 +0100
@@ -1,5 +1,6 @@
(* Title: Pure/ROOT.ML
Author: Makarius
+ UUID: b5c84e7e-c43b-4cf5-9644-a1f387b61ab4
Main entry point for the Isabelle/Pure bootstrap process.
--- a/src/Pure/ROOT.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Pure/ROOT.scala Sat Dec 28 16:38:57 2024 +0100
@@ -1,5 +1,6 @@
/* Title: Pure/ROOT.scala
Author: Makarius
+ UUID: b5c84e7e-c43b-4cf5-9644-a1f387b61ab4
Root of isabelle package.
*/
@@ -29,4 +30,3 @@
def if_proper[A](x: Iterable[A], body: => String): String = Library.if_proper(x, body)
def if_proper(b: Boolean, body: => String): String = Library.if_proper(b, body)
}
-
--- a/src/Pure/Syntax/parser.ML Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Pure/Syntax/parser.ML Sat Dec 28 16:38:57 2024 +0100
@@ -543,8 +543,15 @@
end;
fun pretty_tree (Markup (_, ts)) = maps pretty_tree ts
- | pretty_tree (Node ({const = c, ...}, ts)) =
- [Pretty.enclose "(" ")" (Pretty.breaks (Pretty.quote (Pretty.str c) :: maps pretty_tree ts))]
+ | pretty_tree (Node ({nonterm = nt, const = c, ...}, ts)) =
+ let
+ fun mark_const body =
+ if c = "" then body
+ else [Pretty.enclose "(" ")" (Pretty.breaks (Pretty.quote (Pretty.str c) :: body))];
+ fun mark_nonterm body =
+ if nt = "" then body
+ else [Pretty.markup_open (Markup.name nt Markup_Kind.markup_syntax) body];
+ in mark_nonterm (mark_const (maps pretty_tree ts)) end
| pretty_tree (Tip tok) =
if Lexicon.valued_token tok then [Pretty.str (Lexicon.str_of_token tok)] else [];
--- a/src/Pure/System/isabelle_system.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Pure/System/isabelle_system.scala Sat Dec 28 16:38:57 2024 +0100
@@ -390,7 +390,7 @@
/* JVM shutdown hook */
def create_shutdown_hook(body: => Unit): Thread = {
- val shutdown_hook = Isabelle_Thread.create(new Runnable { def run: Unit = body })
+ val shutdown_hook = Isabelle_Thread.create(new Runnable { def run(): Unit = body })
try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
catch { case _: IllegalStateException => }
--- a/src/Pure/Thy/document_antiquotations.ML Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML Sat Dec 28 16:38:57 2024 +0100
@@ -437,7 +437,7 @@
val _ =
Theory.setup
- (entity_antiquotation \<^binding>\<open>command\<close> Outer_Syntax.check_command "isacommand" #>
+ (entity_antiquotation \<^binding>\<open>command\<close> Outer_Syntax.check_command "isakeywordONE" #>
entity_antiquotation \<^binding>\<open>method\<close> Method.check_name "isa" #>
entity_antiquotation \<^binding>\<open>attribute\<close> Attrib.check_name "isa");
--- a/src/Pure/Thy/document_output.ML Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Pure/Thy/document_output.ML Sat Dec 28 16:38:57 2024 +0100
@@ -159,16 +159,27 @@
fun output_token ctxt tok =
let
+ val keywords = Thy_Header.get_keywords' ctxt;
+
fun output antiq bg en =
output_body ctxt antiq bg en (Input.source_explode (Token.input_of tok));
in
(case Token.kind_of tok of
Token.Comment NONE => []
| Token.Comment (SOME Comment.Marker) => []
- | Token.Command => output false "\\isacommand{" "}"
+ | Token.Command =>
+ let
+ val name = (Token.content_of tok);
+ val bg =
+ if Keyword.is_theory_end keywords name then "\\isakeywordTWO{"
+ else if Keyword.is_proof_asm keywords name orelse
+ Keyword.is_proof_asm_goal keywords name then "\\isakeywordTHREE{"
+ else if Keyword.is_proof_asm_goal keywords name then "\\isakeywordTHREE{"
+ else "\\isakeywordONE{";
+ in output false bg "}" end
| Token.Keyword =>
if Symbol.is_ascii_identifier (Token.content_of tok)
- then output false "\\isakeyword{" "}"
+ then output false "\\isakeywordTWO{" "}"
else output false "" ""
| Token.String => output false "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}"
| Token.Alt_String => output false "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}"
--- a/src/Pure/Tools/doc.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Pure/Tools/doc.scala Sat Dec 28 16:38:57 2024 +0100
@@ -18,7 +18,8 @@
def view(): Unit = Doc.view(path)
override def toString: String = // GUI label
if (title.nonEmpty) {
- "<html><b>" + HTML.output(name) + "</b>: " + HTML.output(title) + "</html>"
+ val style = GUI.Style_HTML
+ style.enclose(style.make_bold(name) + style.make_text(": " + title))
}
else name
}
--- a/src/Tools/Code/code_haskell.ML Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Tools/Code/code_haskell.ML Sat Dec 28 16:38:57 2024 +0100
@@ -330,6 +330,10 @@
("Maybe", ["Nothing", "Just"])
];
+val data_bits_import_operators = [
+ ".&.", ".|.", ".^."
+];
+
fun serialize_haskell module_prefix string_classes ctxt { module_name,
reserved_syms, identifiers, includes, class_syntax, tyco_syntax, const_syntax } program exports =
let
@@ -379,7 +383,10 @@
enclose "import Prelude (" ");" (commas (map str
(map (Library.enclose "(" ")") prelude_import_operators @ prelude_import_unqualified)
@ map (fn (tyco, constrs) => (enclose (tyco ^ "(") ")" o commas o map str) constrs) prelude_import_unqualified_constr))
+ :: enclose "import Data.Bits (" ");" (commas
+ (map (str o Library.enclose "(" ")") data_bits_import_operators))
:: print_qualified_import "Prelude"
+ :: print_qualified_import "Data.Bits"
:: map (print_qualified_import o fst) includes;
fun print_module module_name (gr, imports) =
let
--- a/src/Tools/Graphview/tree_panel.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Tools/Graphview/tree_panel.scala Sat Dec 28 16:38:57 2024 +0100
@@ -128,7 +128,7 @@
})
private val selection_apply = new Button {
- action = Action("<html><b>Apply</b></html>") { selection_action () }
+ action = Action(GUI.Style_HTML.enclose_bold("Apply")) { selection_action () }
tooltip = "Apply tree selection to graph"
}
--- a/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala Sat Dec 28 16:38:57 2024 +0100
@@ -32,6 +32,7 @@
}
class Keyword_Asset(keyword: String, text: String, range: Text.Range) extends IAsset {
+ private val style = GUI.Style_HTML
private val css = GUI.imitate_font_css(GUI.label_font())
protected var _name: String = text
@@ -43,12 +44,12 @@
val s =
_name.indexOf(keyword) match {
case i if i >= 0 && n > 0 =>
- HTML.output(_name.substring(0, i)) +
- "<b>" + HTML.output(keyword) + "</b>" +
- HTML.output(_name.substring(i + n))
- case _ => HTML.output(_name)
+ style.make_text(_name.substring(0, i)) +
+ style.make_bold(keyword) +
+ style.make_text(_name.substring(i + n))
+ case _ => style.make_text(_name)
}
- "<html><span style=\"" + css + "\">" + s + "</span></html>"
+ style.enclose_style(css, s)
}
override def getLongString: String = _name
override def getName: String = _name
@@ -272,6 +273,7 @@
val data = Isabelle_Sidekick.root_data(buffer)
try {
+ val style = GUI.Style_HTML
var offset = 0
for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) {
val kind = chunk.kind
@@ -279,9 +281,7 @@
val source = chunk.source
if (kind != "") {
val label = kind + if_proper(name, " " + name)
- val label_html =
- "<html><b>" + HTML.output(kind) + "</b>" +
- if_proper(name, " " + HTML.output(name)) + "</html>"
+ val label_html = style.enclose(GUI.Name(name, kind = kind, style = style).toString)
val range = Text.Range(offset, offset + source.length)
val asset = new Asset(label, label_html, range, source)
data.root.add(Tree_View.Node(asset))
--- a/src/Tools/jEdit/src/completion_popup.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Sat Dec 28 16:38:57 2024 +0100
@@ -30,8 +30,10 @@
private val html =
item.description match {
case a :: bs =>
- "<html><b>" + HTML.output(Symbol.print_newlines(a)) + "</b>" +
- HTML.output(bs.map(b => " " + Symbol.print_newlines(b)).mkString) + "</html>"
+ val style = GUI.Style_HTML
+ style.enclose(
+ style.make_bold(Symbol.print_newlines(a)) +
+ style.make_text(bs.map(b => " " + Symbol.print_newlines(b)).mkString))
case Nil => ""
}
override def toString: String = html
--- a/src/Tools/jEdit/src/debugger_dockable.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Sat Dec 28 16:38:57 2024 +0100
@@ -216,7 +216,7 @@
}
private val eval_button =
- new GUI.Button("<html><b>Eval</b></html>") {
+ new GUI.Button(GUI.Style_HTML.enclose_bold("Eval")) {
tooltip = "Evaluate ML expression within optional context"
override def clicked(): Unit = eval_expression()
}
--- a/src/Tools/jEdit/src/document_dockable.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala Sat Dec 28 16:38:57 2024 +0100
@@ -272,7 +272,7 @@
}
private val build_button =
- new GUI.Button("<html><b>Build</b></html>") {
+ new GUI.Button(GUI.Style_HTML.enclose_bold("Build")) {
tooltip = "Build document"
override def clicked(): Unit = pending_process()
}
--- a/src/Tools/jEdit/src/info_dockable.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala Sat Dec 28 16:38:57 2024 +0100
@@ -70,10 +70,17 @@
/* output text area */
- private val output: Output_Area = new Output_Area(view)
+ private val output: Output_Area =
+ new Output_Area(view) {
+ override def handle_shown(): Unit = split_pane_layout()
+ }
+
output.pretty_text_area.update(snapshot, results, info)
- private val controls = Wrap_Panel(output.pretty_text_area.search_zoom_components)
+ private val auto_hovering_button = new JEdit_Options.auto_hovering.GUI
+
+ private val controls =
+ Wrap_Panel(auto_hovering_button :: output.pretty_text_area.search_zoom_components)
add(controls.peer, BorderLayout.NORTH)
output.setup(dockable)
@@ -84,7 +91,11 @@
private val main =
Session.Consumer[Session.Global_Options](getClass.getName) {
- case _: Session.Global_Options => GUI_Thread.later { output.handle_resize() }
+ case _: Session.Global_Options =>
+ GUI_Thread.later {
+ output.handle_resize()
+ auto_hovering_button.load()
+ }
}
override def init(): Unit = {
--- a/src/Tools/jEdit/src/keymap_merge.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Tools/jEdit/src/keymap_merge.scala Sat Dec 28 16:38:57 2024 +0100
@@ -102,12 +102,14 @@
PIDE.options.color_value("error_color")
private sealed case class Table_Entry(shortcut: Shortcut, head: Option[Int], tail: List[Int]) {
- override def toString: String =
- if (head.isEmpty) "<html>" + HTML.output(shortcut.toString) + "</html>"
- else
- "<html><font style='color: #" + Color_Value.print(conflict_color) + ";'>" +
- HTML.output("--- " + shortcut.toString) +
- "</font></html>"
+ override def toString: String = {
+ val style = GUI.Style_HTML
+ if (head.isEmpty) style.enclose(style.make_text(shortcut.toString))
+ else {
+ style.enclose_style(HTML.color_property(conflict_color),
+ style.make_text("--- " + shortcut.toString))
+ }
+ }
}
private class Table_Model(entries: List[Table_Entry]) extends AbstractTableModel {
--- a/src/Tools/jEdit/src/output_area.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Tools/jEdit/src/output_area.scala Sat Dec 28 16:38:57 2024 +0100
@@ -11,9 +11,10 @@
import java.awt.Dimension
import java.awt.event.{ComponentEvent, ComponentAdapter, FocusAdapter, FocusEvent,
- MouseEvent, MouseAdapter}
-import javax.swing.JComponent
+ HierarchyListener, HierarchyEvent, MouseEvent, MouseAdapter}
+import javax.swing.{JComponent, JButton}
import javax.swing.event.{TreeSelectionListener, TreeSelectionEvent}
+import javax.swing.plaf.basic.BasicSplitPaneUI
import scala.util.matching.Regex
import scala.swing.{Component, ScrollPane, SplitPane, Orientation}
@@ -22,7 +23,7 @@
import org.gjt.sp.jedit.View
-class Output_Area(view: View, root_name: String = "Search results") {
+class Output_Area(view: View, root_name: String = Pretty_Text_Area.search_title()) {
output_area =>
GUI_Thread.require {}
@@ -35,8 +36,17 @@
val tree: Tree_View =
new Tree_View(root = Tree_View.Node(root_name), single_selection_mode = true)
+ private var search_activated = false
+
def handle_search(search: Pretty_Text_Area.Search_Results): Unit = {
- tree.init_model { for (result <- search.results) tree.root.add(Tree_View.Node(result)) }
+ if (!search_activated && search.pattern.isDefined) {
+ search_activated = true
+ delay_shown.invoke()
+ }
+ tree.init_model {
+ tree.root.setUserObject(Pretty_Text_Area.search_title(lines = search.length))
+ for (result <- search.results) tree.root.add(Tree_View.Node(result))
+ }
tree.revalidate()
}
@@ -65,6 +75,23 @@
/* handle events */
def handle_focus(): Unit = ()
+ def handle_shown(): Unit = ()
+
+ lazy val delay_shown: Delay =
+ Delay.first(PIDE.session.input_delay, gui = true) { handle_shown() }
+
+ private lazy val hierarchy_listener =
+ new HierarchyListener {
+ override def hierarchyChanged(e: HierarchyEvent): Unit = {
+ val displayed =
+ (e.getChangeFlags & HierarchyEvent.DISPLAYABILITY_CHANGED) != 0 &&
+ e.getComponent.isDisplayable
+ val shown =
+ (e.getChangeFlags & HierarchyEvent.SHOWING_CHANGED) != 0 &&
+ e.getComponent.isShowing
+ if (displayed || shown) delay_shown.invoke()
+ }
+ }
private lazy val component_listener =
new ComponentAdapter {
@@ -115,7 +142,47 @@
rightComponent = text_pane
}
+ def split_pane_layout(open: Boolean = search_activated): Unit = {
+ split_pane.peer.getUI match {
+ case ui: BasicSplitPaneUI =>
+ val div = ui.getDivider
+
+ val orientation = split_pane.orientation
+ val location = split_pane.dividerLocation
+ val insets = split_pane.peer.getInsets
+
+ val (left_collapsed, right_collapsed) =
+ if (orientation == Orientation.Vertical) {
+ (location == insets.left,
+ location == (split_pane.peer.getWidth - div.getWidth - insets.right))
+ }
+ else {
+ (location == insets.top,
+ location == (split_pane.peer.getHeight - div.getHeight - insets.bottom))
+ }
+
+ def click(i: Int): Unit = {
+ val comp =
+ try { div.getComponent(i) }
+ catch { case _: ArrayIndexOutOfBoundsException => null }
+ comp match {
+ case button: JButton => button.doClick()
+ case _ =>
+ }
+ }
+
+ if (open && left_collapsed) click(1)
+ else if (open && right_collapsed || !open && !left_collapsed) click(0)
+ else if (!open && right_collapsed) {
+ click(0)
+ GUI_Thread.later { click(0) } // FIXME!?
+ }
+ case _ =>
+ }
+ }
+
def setup(parent: JComponent): Unit = {
+ parent.addHierarchyListener(hierarchy_listener)
parent.addComponentListener(component_listener)
parent.addFocusListener(focus_listener)
tree.addMouseListener(mouse_listener)
@@ -128,5 +195,8 @@
handle_resize()
}
- def exit(): Unit = delay_resize.revoke()
+ def exit(): Unit = {
+ delay_resize.revoke()
+ delay_shown.revoke()
+ }
}
--- a/src/Tools/jEdit/src/output_dockable.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Sat Dec 28 16:38:57 2024 +0100
@@ -27,8 +27,11 @@
/* output area */
- private val output: Output_Area =
- new Output_Area(view) { override def handle_update(): Unit = dockable.handle_update(true) }
+ val output: Output_Area =
+ new Output_Area(view) {
+ override def handle_update(): Unit = dockable.handle_update(true)
+ override def handle_shown(): Unit = split_pane_layout()
+ }
override def detach_operation: Option[() => Unit] =
output.pretty_text_area.detach_operation
--- a/src/Tools/jEdit/src/pretty_text_area.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Sat Dec 28 16:38:57 2024 +0100
@@ -42,6 +42,7 @@
) {
lazy val line_text: String =
Library.trim_line(JEdit_Lib.get_text(buffer, line_range).getOrElse(""))
+ .replace('\t',' ')
lazy val gui_text: String = Library.string_builder(line_range.length * 2) { s =>
// see also HyperSearchResults.highlightString
@@ -50,8 +51,11 @@
s ++= ":</b> "
val line_start = line_range.start
- val search_range = Text.Range(line_start, line_start + line_text.length)
- var last = 0
+ val plain_start = line_text.length - line_text.stripLeading.length
+ val plain_stop = line_text.stripTrailing.length
+
+ val search_range = Text.Range(line_start + plain_start, line_start + plain_stop)
+ var last = plain_start
for (range <- JEdit_Lib.search_text(buffer, search_range, regex)) {
val next = range.start - line_start
if (last < next) s ++= line_text.substring(last, next)
@@ -62,12 +66,15 @@
s ++= "</span>"
last = range.stop - line_start
}
- if (last < line_text.length) s ++= line_text.substring(last)
+ if (last < plain_stop) s ++= line_text.substring(last)
s ++= "</html>"
}
override def toString: String = gui_text
}
+ def search_title(lines: Int = 0): String =
+ "Search result" + (if (lines <= 1) "" else " (" + lines + " lines)")
+
sealed case class Search_Results(
buffer: JEditBuffer,
highlight_style: String,
--- a/src/Tools/jEdit/src/query_dockable.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Tools/jEdit/src/query_dockable.scala Sat Dec 28 16:38:57 2024 +0100
@@ -10,9 +10,9 @@
import isabelle._
import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
-import javax.swing.{JComponent, JTextField}
+import javax.swing.JComponent
-import scala.swing.{Component, TextField, Label, ListView, TabbedPane, BorderPanel}
+import scala.swing.{Component, TextField, Label, TabbedPane, BorderPanel}
import scala.swing.event.{SelectionChanged, Key, KeyPressed}
import org.gjt.sp.jedit.View
@@ -108,7 +108,7 @@
override def clicked(): Unit = apply_query()
}
- private val apply_button = new GUI.Button("<html><b>Apply</b></html>") {
+ private val apply_button = new GUI.Button(GUI.Style_HTML.enclose_bold("Apply")) {
tooltip = "Find theorems meeting specified criteria"
override def clicked(): Unit = apply_query()
}
@@ -155,7 +155,7 @@
/* GUI page */
- private val apply_button = new GUI.Button("<html><b>Apply</b></html>") {
+ private val apply_button = new GUI.Button(GUI.Style_HTML.enclose_bold("Apply")) {
tooltip = "Find constants by name / type patterns"
override def clicked(): Unit = apply_query()
}
@@ -226,7 +226,7 @@
/* GUI page */
- private val apply_button = new GUI.Button("<html><b>Apply</b></html>") {
+ private val apply_button = new GUI.Button(GUI.Style_HTML.enclose_bold("Apply")) {
tooltip = "Apply to current context"
override def clicked(): Unit = apply_query()
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Sat Dec 28 16:38:57 2024 +0100
@@ -96,7 +96,7 @@
tooltip = "Try standard proof methods like \"auto\" and \"blast\" as alternatives to \"metis\""
}
- private val apply_query = new GUI.Button("<html><b>Apply</b></html>") {
+ private val apply_query = new GUI.Button(GUI.Style_HTML.enclose_bold("Apply")) {
tooltip = "Search for first-order proof using automatic theorem provers"
override def clicked(): Unit = hammer()
}
--- a/src/Tools/jEdit/src/state_dockable.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Tools/jEdit/src/state_dockable.scala Sat Dec 28 16:38:57 2024 +0100
@@ -23,7 +23,10 @@
/* output text area */
- private val output: Output_Area = new Output_Area(view)
+ private val output: Output_Area =
+ new Output_Area(view) {
+ override def handle_shown(): Unit = split_pane_layout()
+ }
override def detach_operation: Option[() => Unit] = output.pretty_text_area.detach_operation
@@ -71,7 +74,9 @@
}
}
- private val update_button = new GUI.Button("<html><b>Update</b></html>") {
+ private val auto_hovering_button = new JEdit_Options.auto_hovering.GUI
+
+ private val update_button = new GUI.Button(GUI.Style_HTML.enclose_bold("Update")) {
tooltip = "Update display according to the command at cursor position"
override def clicked(): Unit = update_request()
}
@@ -83,7 +88,7 @@
private val controls =
Wrap_Panel(
- List(auto_update_button, update_button, locate_button) :::
+ List(auto_hovering_button, auto_update_button, update_button, locate_button) :::
output.pretty_text_area.search_zoom_components)
add(controls.peer, BorderLayout.NORTH)
@@ -94,7 +99,10 @@
private val main =
Session.Consumer[Any](getClass.getName) {
case _: Session.Global_Options =>
- GUI_Thread.later { output.handle_resize() }
+ GUI_Thread.later {
+ output.handle_resize()
+ auto_hovering_button.load()
+ }
case changed: Session.Commands_Changed =>
if (changed.assignment) GUI_Thread.later { auto_update() }
--- a/src/Tools/jEdit/src/symbols_dockable.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Sat Dec 28 16:38:57 2024 +0100
@@ -32,7 +32,7 @@
def update_font(): Unit = { font = GUI.font(size = font_size) }
update_font()
- text = "<html>" + HTML.output(Symbol.decode(txt)) + "</html>"
+ text = GUI.Style_HTML.enclose_text(Symbol.decode(txt))
action =
Action(text) {
val text_area = view.getTextArea
--- a/src/Tools/jEdit/src/theories_dockable.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala Sat Dec 28 16:38:57 2024 +0100
@@ -9,9 +9,9 @@
import isabelle._
-import scala.swing.{Button, TextArea, Label, ListView, ScrollPane, Component}
+import scala.swing.{Button, Label, ScrollPane}
-import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension}
+import java.awt.BorderLayout
import javax.swing.border.{BevelBorder, SoftBevelBorder}
import org.gjt.sp.jedit.{View, jEdit}
--- a/src/Tools/jEdit/src/timing_dockable.scala Wed Dec 18 10:50:59 2024 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala Sat Dec 28 16:38:57 2024 +0100
@@ -28,68 +28,60 @@
entry2.timing compare entry1.timing
}
- object Renderer_Component extends Label {
- opaque = false
- xAlignment = Alignment.Leading
- border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
-
- var entry: Entry = null
- override def paintComponent(gfx: Graphics2D): Unit = {
- def paint_rectangle(color: Color): Unit = {
- val size = peer.getSize()
- val insets = border.getBorderInsets(peer)
- val x = insets.left
- val y = insets.top
- val w = size.width - x - insets.right
- val h = size.height - y - insets.bottom
- gfx.setColor(color)
- gfx.fillRect(x, y, w, h)
- }
-
- entry match {
- case theory_entry: Theory_Entry if theory_entry.current =>
- paint_rectangle(view.getTextArea.getPainter.getSelectionColor)
- case _: Command_Entry =>
- paint_rectangle(view.getTextArea.getPainter.getMultipleSelectionColor)
- case _ =>
- }
- super.paintComponent(gfx)
- }
- }
+ def make_gui_style(command: Boolean = false): String =
+ HTML.background_property(
+ if (command) view.getTextArea.getPainter.getMultipleSelectionColor
+ else view.getTextArea.getPainter.getSelectionColor)
class Renderer extends ListView.Renderer[Entry] {
+ private object component extends Label {
+ opaque = false
+ xAlignment = Alignment.Leading
+ border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
+ }
+
def componentFor(
list: ListView[_ <: Timing_Dockable.this.Entry],
isSelected: Boolean,
focused: Boolean,
- entry: Entry, index: Int
+ entry: Entry,
+ index: Int
): Component = {
- val component = Renderer_Component
- component.entry = entry
- component.text = entry.print
+ component.text = entry.gui_text
component
}
}
}
private abstract class Entry {
+ def depth: Int = 0
def timing: Double
- def print: String
+ def gui_style: String = ""
+ def gui_name: GUI.Name
+ def gui_text: String = {
+ val style = GUI.Style_HTML
+ val bullet = if (depth == 0) style.triangular_bullet else style.regular_bullet
+ style.enclose_style(gui_style,
+ style.spaces(4 * depth) + bullet + " " +
+ style.make_text(Time.print_seconds(timing) + "s ") +
+ gui_name.set_style(style).toString)
+ }
def follow(snapshot: Document.Snapshot): Unit
}
- private case class Theory_Entry(name: Document.Node.Name, timing: Double, current: Boolean)
+ private case class Theory_Entry(name: Document.Node.Name, timing: Double)
extends Entry {
- def print: String =
- Time.print_seconds(timing) + "s theory " + quote(name.theory)
+ def make_current: Theory_Entry =
+ new Theory_Entry(name, timing) { override val gui_style: String = Entry.make_gui_style() }
+ def gui_name: GUI.Name = GUI.Name(name.theory, kind = "theory")
def follow(snapshot: Document.Snapshot): Unit =
PIDE.editor.goto_file(true, view, name.node)
}
- private case class Command_Entry(command: Command, timing: Double)
- extends Entry {
- def print: String =
- " " + Time.print_seconds(timing) + "s command " + quote(command.span.name)
+ private case class Command_Entry(command: Command, timing: Double) extends Entry {
+ override def depth: Int = 1
+ override val gui_style: String = Entry.make_gui_style(command = true)
+ def gui_name: GUI.Name = GUI.Name(command.span.name, kind = "command")
def follow(snapshot: Document.Snapshot): Unit =
PIDE.editor.hyperlink_command(true, snapshot, command.id).foreach(_.follow(view))
}
@@ -133,8 +125,7 @@
handle_update()
}
tooltip = threshold_tooltip
- verifier = ((s: String) =>
- s match { case Value.Double(x) => x >= 0.0 case _ => false })
+ verifier = { case Value.Double(x) => x >= 0.0 case _ => false }
}
private val controls = Wrap_Panel(List(threshold_label, threshold_value))
@@ -158,13 +149,13 @@
val theories =
(for ((node_name, node_timing) <- nodes_timing.toList if node_timing.command_timings.nonEmpty)
- yield Theory_Entry(node_name, node_timing.total, false)).sorted(Entry.Ordering)
+ yield Theory_Entry(node_name, node_timing.total)).sorted(Entry.Ordering)
val commands =
(for ((command, command_timing) <- timing.command_timings.toList)
yield Command_Entry(command, command_timing)).sorted(Entry.Ordering)
theories.flatMap(entry =>
- if (entry.name == name) entry.copy(current = true) :: commands
+ if (entry.name == name) entry.make_current :: commands
else List(entry))
}