Thu, 18 May 2023 23:50:59 +0200 wenzelm more careful reset/set_context for stored declarations;
Thu, 18 May 2023 23:21:05 +0200 wenzelm tuned;
Thu, 18 May 2023 23:20:41 +0200 wenzelm tuned;
Thu, 18 May 2023 17:21:29 +0200 wenzelm clarified signature: more explicit types;
Thu, 18 May 2023 15:34:01 +0200 wenzelm clarified data: avoid pointless Morphism.transform;
Thu, 18 May 2023 14:06:35 +0200 wenzelm proper Token.Declaration for internal_declaration;
Tue, 16 May 2023 20:26:09 +0200 wenzelm more standard treatment of morphism context;
Tue, 16 May 2023 19:52:50 +0200 wenzelm tuned: avoid duplication;
Tue, 16 May 2023 19:43:42 +0200 wenzelm more standard treatment of morphism context, but hardly relevant here;
Tue, 16 May 2023 19:42:19 +0200 wenzelm tuned;
Tue, 16 May 2023 19:20:18 +0200 wenzelm more careful treatment of set_context / reset_context for persistent morphisms;
Tue, 16 May 2023 17:08:31 +0200 wenzelm clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
(0) -30000 -10000 -3000 -1000 -300 -100 -12 +12 +100 +300 +1000 +3000 tip