Changes

Summary

proper Font_Subst.cache for paintScreenLineRange;
more predictable result, avoid slightly odd "lastSubstFont" by jEdit;
tuned;
tuned signature;
tuned;
discontinue i21of4 (old Apple hardware);
avoid deprecated operation;
tuned;
support for jEdit font substitution;
more ambitious use of AttributedString (despite be825a69fc67, which was for much older Java); more direct TextAttribute.RUN_DIRECTION_LTR (see also ce22e5c3d4ce);
updated to flatlaf-1.2;
proper directories after reinstallation of lxbroy10;
more visual emphasis on node status;
more word cleanup
merged
more default simp rules
some word streamlining
avoid legacy domain informatik.tu-muenchen.de;

Changeset 73884:0a12ca4f3e8d by wenzelm: proper Font_Subst.cache for paintScreenLineRange;
The file was modified	`src/Tools/jEdit/src/rich_text_area.scala`
Changeset 73883:994c9dacd2f9 by wenzelm: more predictable result, avoid slightly odd "lastSubstFont" by jEdit;
The file was modified	`src/Tools/jEdit/src/rich_text_area.scala`
Changeset 73882:01efb7cbf365 by wenzelm: tuned;
The file was modified	`src/Tools/jEdit/src/token_markup.scala`
Changeset 73881:b1272ec71568 by wenzelm: tuned signature;
The file was modified	`src/Tools/jEdit/src/rich_text_area.scala`
Changeset 73880:9ce206f6e8c6 by wenzelm: tuned;
The file was modified	`src/Tools/jEdit/src/rich_text_area.scala`
Changeset 73879:0db0cd462163 by wenzelm: discontinue i21of4 (old Apple hardware);
The file was modified	`src/Pure/Admin/isabelle_cronjob.scala`
Changeset 73878:291597140695 by wenzelm: avoid deprecated operation;
The file was modified	`src/Pure/GUI/gui.scala`
Changeset 73877:d9ebbfe099a8 by wenzelm: tuned;
The file was modified	`src/Tools/jEdit/src/rich_text_area.scala`
Changeset 73876:e6c9c1c3f580 by wenzelm: support for jEdit font substitution;
The file was modified	`NEWS`
The file was modified	`src/Tools/jEdit/src/rich_text_area.scala`
Changeset 73875:6e43936f2111 by wenzelm: more ambitious use of AttributedString (despite be825a69fc67, which was for much older Java);<br>more direct TextAttribute.RUN_DIRECTION_LTR (see also ce22e5c3d4ce);
The file was modified	`src/Tools/jEdit/src/rich_text_area.scala`
Changeset 73874:7730b882f14a by wenzelm: updated to flatlaf-1.2;
The file was modified	`Admin/components/components.sha1`
The file was modified	`Admin/components/main`
Changeset 73873:2d42e52152b1 by wenzelm: proper directories after reinstallation of lxbroy10;
The file was modified	`Admin/etc/options`
Changeset 73872:ced6e3c03425 by wenzelm: more visual emphasis on node status;
The file was modified	`src/Tools/jEdit/etc/options`
The file was modified	`src/Tools/jEdit/src/theories_dockable.scala`
Changeset 73871:f46e9f75b7d5 by haftmann: more word cleanup
The file was modified	`src/HOL/Library/Bit_Operations.thy`
The file was modified	`src/HOL/Parity.thy`
Changeset 73870:d156b141fe2f by haftmann: merged
Changeset 73869:7181130f5872 by haftmann: more default simp rules
The file was modified	`NEWS`
The file was modified	`src/HOL/Analysis/Bochner_Integration.thy`
The file was modified	`src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy`
The file was modified	`src/HOL/Decision_Procs/Ferrack.thy`
The file was modified	`src/HOL/HOLCF/Universal.thy`
The file was modified	`src/HOL/Homology/Simplices.thy`
The file was modified	`src/HOL/Import/HOL_Light_Maps.thy`
The file was modified	`src/HOL/Lattices.thy`
The file was modified	`src/HOL/Library/Bit_Operations.thy`
The file was modified	`src/HOL/Library/Extended_Nonnegative_Real.thy`
The file was modified	`src/HOL/Power.thy`
Changeset 73868:465846b611d5 by haftmann: some word streamlining
The file was modified	`src/HOL/Library/Bit_Operations.thy`
Changeset 73867:3d3c60a90af5 by wenzelm: avoid legacy domain informatik.tu-muenchen.de;
The file was modified	`src/Pure/General/mailman.scala`

Summary

proved conditional completeness of compilation
fixed typos
more word cleanup
more default simp rules
some word streamlining
made consistent again
Fixed entry name for theories in sub-directory
Stone_Relation_Algebras, Aggregation_Algebras: added history to metadata

Changeset 11891:5695f90acdbf by desharna: proved conditional completeness of compilation
The file was added	`thys/Interpreter_Optimizations/Inca_Verification.thy`
The file was modified	`metadata/metadata`
The file was modified	`thys/Interpreter_Optimizations/Global.thy`
The file was modified	`thys/Interpreter_Optimizations/Inca.thy`
The file was modified	`thys/Interpreter_Optimizations/Inca_to_Ubx_compiler.thy`
The file was modified	`thys/Interpreter_Optimizations/List_util.thy`
The file was modified	`thys/Interpreter_Optimizations/Map_Extra.thy`
The file was modified	`thys/Interpreter_Optimizations/Op_example.thy`
The file was modified	`thys/Interpreter_Optimizations/Std.thy`
The file was modified	`thys/Interpreter_Optimizations/Std_to_Inca_compiler.thy`
The file was modified	`thys/Interpreter_Optimizations/Ubx.thy`
Changeset 11890:e8af416c2e70 by nipkow: fixed typos
The file was modified	`thys/Amortized_Complexity/Amortized_Framework0.thy`
Changeset 11889:1a99ac2d4342 by haftmann: more word cleanup
The file was modified	`thys/Native_Word/Code_Symbolic_Bits_Int.thy`
The file was modified	`thys/Native_Word/More_Bits_Int.thy`
The file was modified	`thys/Word_Lib/Bits_Int.thy`
The file was modified	`thys/Word_Lib/Generic_set_bit.thy`
The file was modified	`thys/Word_Lib/More_Arithmetic.thy`
The file was modified	`thys/Word_Lib/Most_significant_bit.thy`
The file was modified	`thys/Word_Lib/Norm_Words.thy`
The file was modified	`thys/Word_Lib/Signed_Division_Word.thy`
The file was modified	`thys/Word_Lib/Word_Lemmas.thy`
Changeset 11888:f1195cc96e85 by haftmann: more default simp rules
The file was modified	`thys/AVL-Trees/AVL.thy`
The file was modified	`thys/Akra_Bazzi/Akra_Bazzi_Asymptotics.thy`
The file was modified	`thys/BTree/BTree_ImpSet.thy`
The file was modified	`thys/BenOr_Kozen_Reif/BKR_Proofs.thy`
The file was modified	`thys/Berlekamp_Zassenhaus/Mahler_Measure.thy`
The file was modified	`thys/Bertrands_Postulate/Bertrand.thy`
The file was modified	`thys/Chandy_Lamport/Co_Snapshot.thy`
The file was modified	`thys/Closest_Pair_Points/Common.thy`
The file was modified	`thys/Coinductive/Coinductive_Nat.thy`
The file was modified	`thys/Dirichlet_Series/Dirichlet_Series_Analysis.thy`
The file was modified	`thys/Ergodic_Theory/Kingman.thy`
The file was modified	`thys/Extended_Finite_State_Machines/GExp.thy`
The file was modified	`thys/Gromov_Hyperbolicity/Gromov_Hyperbolicity.thy`
The file was modified	`thys/Group-Ring-Module/Algebra5.thy`
The file was modified	`thys/Group-Ring-Module/Algebra6.thy`
The file was modified	`thys/HereditarilyFinite/HF.thy`
The file was modified	`thys/IP_Addresses/IPv6.thy`
The file was modified	`thys/Inductive_Inference/Universal.thy`
The file was modified	`thys/JinjaThreads/MM/SC_Completion.thy`
The file was modified	`thys/List-Infinite/ListInf/List2.thy`
The file was modified	`thys/List_Update/Move_to_Front.thy`
The file was modified	`thys/Locally-Nameless-Sigma/preliminary/ListPre.thy`
The file was modified	`thys/Lp/Lp.thy`
The file was modified	`thys/Noninterference_CSP/ClassicalNoninterference.thy`
The file was modified	`thys/Ordinal_Partitions/Erdos_Milner.thy`
The file was modified	`thys/Prime_Distribution_Elementary/More_Dirichlet_Misc.thy`
The file was modified	`thys/Prime_Number_Theorem/Mertens_Theorems.thy`
The file was modified	`thys/Probabilistic_Noninterference/Language_Semantics.thy`
The file was modified	`thys/RSAPSS/Word.thy`
The file was modified	`thys/Recursion-Theory-I/PRecFinSet.thy`
The file was modified	`thys/Simple_Firewall/Primitives/Iface.thy`
The file was modified	`thys/Taylor_Models/Polynomial_Expression_Additional.thy`
The file was modified	`thys/Timed_Automata/Approx_Beta.thy`
The file was modified	`thys/Timed_Automata/Paths_Cycles.thy`
The file was modified	`thys/Universal_Turing_Machine/Recursive.thy`
The file was modified	`thys/Word_Lib/More_Arithmetic.thy`
The file was modified	`thys/Zeta_Function/Zeta_Library.thy`
The file was modified	`thys/pGCL/Tutorial/Primitives.thy`
Changeset 11887:9e42e0c5f9f9 by haftmann: some word streamlining
The file was modified	`thys/Word_Lib/Bits_Int.thy`
Changeset 11886:55af834ad1b8 by haftmann: made consistent again
The file was modified	`thys/Group-Ring-Module/Algebra5.thy`
Changeset 11885:291a8d8961b4 by fabian huch _huch@in.tum.de_: Fixed entry name for theories in sub-directory
The file was modified	`admin/jenkins/ci_build_all.scala`
The file was modified	`admin/jenkins/ci_build_testboard.scala`
Changeset 11884:d6c66721438d by walter guttmann _walter.guttmann@canterbury.ac.nz_: Stone_Relation_Algebras, Aggregation_Algebras: added history to metadata
The file was modified	`metadata/metadata`