wenzelm [Thu, 19 Sep 2024 20:38:19 +0200] rev 80902
more operations;
wenzelm [Thu, 19 Sep 2024 12:41:02 +0200] rev 80901
minor performance tuning: avoid vacuous update of context;
wenzelm [Thu, 19 Sep 2024 12:10:17 +0200] rev 80900
tuned;
wenzelm [Thu, 19 Sep 2024 12:08:56 +0200] rev 80899
proper Context_Position.report, following 5328d67ec647;
wenzelm [Tue, 17 Sep 2024 18:49:46 +0200] rev 80898
more operations;
wenzelm [Tue, 17 Sep 2024 17:51:55 +0200] rev 80897
more explicit context for syn_ext/mixfix operations, but it often degenerates to background theory;
wenzelm [Tue, 17 Sep 2024 17:05:37 +0200] rev 80896
obsolete --- superseded by Local_Theory.syntax_cmd;
wenzelm [Tue, 17 Sep 2024 11:32:11 +0200] rev 80895
tuned;
wenzelm [Tue, 17 Sep 2024 11:14:25 +0200] rev 80894
unused (see 39261908e12f);
wenzelm [Tue, 17 Sep 2024 11:06:11 +0200] rev 80893
clarified signature;
tuned comments;
wenzelm [Tue, 17 Sep 2024 11:00:03 +0200] rev 80892
tuned comments;
wenzelm [Tue, 17 Sep 2024 10:47:08 +0200] rev 80891
tuned;
wenzelm [Mon, 16 Sep 2024 20:44:46 +0200] rev 80890
more detailed markup;
wenzelm [Mon, 16 Sep 2024 19:58:28 +0200] rev 80889
more formal Markup.expression;