wenzelm [Thu, 26 Sep 2024 21:55:46 +0200] rev 80966
proper 'no_syntax' declarations (amending 8e72f55295fd);
wenzelm [Thu, 26 Sep 2024 11:41:51 +0200] rev 80965
tuned, following make_symbs in src/Pure/Syntax/printer.ML;
wenzelm [Thu, 26 Sep 2024 11:31:43 +0200] rev 80964
clarified use of Lexicon.dummy;
tuned signature;
wenzelm [Thu, 26 Sep 2024 11:01:41 +0200] rev 80963
unused (see 584828fa7a97);
wenzelm [Thu, 26 Sep 2024 10:51:36 +0200] rev 80962
tuned;
wenzelm [Thu, 26 Sep 2024 00:06:00 +0200] rev 80961
tuned;
wenzelm [Wed, 25 Sep 2024 23:34:31 +0200] rev 80960
tuned: prefer ML over prose;
wenzelm [Wed, 25 Sep 2024 17:45:15 +0200] rev 80959
eliminated redundant nt_count: rely on Symtab.size;
tuned signature: more standard argument order;
wenzelm [Wed, 25 Sep 2024 15:06:12 +0200] rev 80958
eliminate unused prod_count (see also 7afca3218b65);
wenzelm [Wed, 25 Sep 2024 14:45:19 +0200] rev 80957
tuned;
wenzelm [Wed, 25 Sep 2024 13:32:52 +0200] rev 80956
more markup;
wenzelm [Wed, 25 Sep 2024 13:30:04 +0200] rev 80955
minor performance tuning: prefer static values;
wenzelm [Wed, 25 Sep 2024 13:20:36 +0200] rev 80954
tuned;
wenzelm [Wed, 25 Sep 2024 13:20:24 +0200] rev 80953
more markup;
wenzelm [Wed, 25 Sep 2024 12:59:43 +0200] rev 80952
clarified persistent datatype: more direct literal_markup, which also serves as a flag;
wenzelm [Wed, 25 Sep 2024 10:48:16 +0200] rev 80951
tuned signature;
wenzelm [Wed, 25 Sep 2024 10:38:46 +0200] rev 80950
clarified signature;
Fabian Huch <huch@in.tum.de> [Fri, 23 Aug 2024 15:30:09 +0200] rev 80949
add comments to rendering, e.g. to collect them from build database;
paulson <lp15@cam.ac.uk> [Thu, 26 Sep 2024 14:44:37 +0100] rev 80948
To tiny but maybe useful lemmas (moved in from the AFP, Word_Lib)
wenzelm [Tue, 24 Sep 2024 21:41:01 +0200] rev 80947
tuned;
wenzelm [Tue, 24 Sep 2024 21:31:20 +0200] rev 80946
tuned;
wenzelm [Tue, 24 Sep 2024 21:24:44 +0200] rev 80945
tuned;
wenzelm [Tue, 24 Sep 2024 20:10:11 +0200] rev 80944
tuned;
wenzelm [Tue, 24 Sep 2024 19:58:24 +0200] rev 80943
tuned;
wenzelm [Tue, 24 Sep 2024 18:25:36 +0200] rev 80942
minor performance tuning for blocks without markup;
wenzelm [Tue, 24 Sep 2024 18:17:39 +0200] rev 80941
more markup <expression kind="item"> in Isabelle/Scala, with pro-forma Markup_Kind.setup in Isabelle/ML;
wenzelm [Tue, 24 Sep 2024 17:57:42 +0200] rev 80940
clarified signature;
wenzelm [Tue, 24 Sep 2024 17:41:05 +0200] rev 80939
tuned;
wenzelm [Tue, 24 Sep 2024 17:35:24 +0200] rev 80938
minor performance tuning: more direct blocks without markup;
tuned signature;
wenzelm [Tue, 24 Sep 2024 17:31:12 +0200] rev 80937
tuned;
wenzelm [Tue, 24 Sep 2024 17:27:56 +0200] rev 80936
tuned signature;
wenzelm [Mon, 23 Sep 2024 22:33:37 +0200] rev 80935
proper 'no_syntax' (amending 8e72f55295fd);
wenzelm [Mon, 23 Sep 2024 21:09:23 +0200] rev 80934
more inner syntax markup: HOL;
wenzelm [Mon, 23 Sep 2024 15:01:10 +0200] rev 80933
misc tuning and clarification;
wenzelm [Mon, 23 Sep 2024 13:32:38 +0200] rev 80932
standardize mixfix annotations via "isabelle update -u mixfix_cartouches -l Pure HOL" --- to simplify systematic editing;
wenzelm [Mon, 23 Sep 2024 12:59:10 +0200] rev 80931
tuned;
wenzelm [Mon, 23 Sep 2024 11:36:03 +0200] rev 80930
minor performance tuning: more concise tuples;
wenzelm [Mon, 23 Sep 2024 11:08:30 +0200] rev 80929
tuned;
wenzelm [Mon, 23 Sep 2024 10:56:25 +0200] rev 80928
tuned;
wenzelm [Mon, 23 Sep 2024 10:45:05 +0200] rev 80927
tuned;
wenzelm [Sun, 22 Sep 2024 18:47:43 +0200] rev 80926
misc tuning and clarification;
wenzelm [Sun, 22 Sep 2024 17:40:28 +0200] rev 80925
more antiquotations;
wenzelm [Sun, 22 Sep 2024 16:18:49 +0200] rev 80924
tuned comments;
wenzelm [Sun, 22 Sep 2024 16:12:15 +0200] rev 80923
more specific markup for "judgment";
wenzelm [Sun, 22 Sep 2024 16:04:44 +0200] rev 80922
remove specific support for "expression" block markup: prefer "notation";
wenzelm [Sun, 22 Sep 2024 15:58:55 +0200] rev 80921
clarified inner syntax markup: use "notation" uniformly;
wenzelm [Sun, 22 Sep 2024 15:46:19 +0200] rev 80920
more uniform treatment of Markup.notation and Markup.expression: manage kinds via context;
wenzelm [Sun, 22 Sep 2024 14:41:34 +0200] rev 80919
clarified modules and signature;
wenzelm [Sun, 22 Sep 2024 14:33:03 +0200] rev 80918
proper fbreaks (amending 53f12ab896e6);
wenzelm [Fri, 20 Sep 2024 23:37:00 +0200] rev 80917
more inner syntax markup: minor object-logics;
wenzelm [Fri, 20 Sep 2024 23:36:33 +0200] rev 80916
more inner syntax markup: Pure;
wenzelm [Fri, 20 Sep 2024 21:34:09 +0200] rev 80915
more markup elements;
wenzelm [Fri, 20 Sep 2024 19:51:08 +0200] rev 80914
standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing;
wenzelm [Fri, 20 Sep 2024 19:07:10 +0200] rev 80913
proper Haskell setup, following 406a85a25189;
wenzelm [Fri, 20 Sep 2024 18:09:04 +0200] rev 80912
support more markup elements;
wenzelm [Fri, 20 Sep 2024 15:35:16 +0200] rev 80911
block markup for specific notation, notably infix and binder;
tuned;
wenzelm [Fri, 20 Sep 2024 14:28:13 +0200] rev 80910
clarified signature: more explicit operations;
wenzelm [Fri, 20 Sep 2024 13:30:55 +0200] rev 80909
tuned;
wenzelm [Fri, 20 Sep 2024 11:19:23 +0200] rev 80908
tuned;
wenzelm [Fri, 20 Sep 2024 11:10:04 +0200] rev 80907
no need to suppress positions (see ff3b8e4079bd) thanks to Context_Position.set_visible false (see 5328d67ec647);