src/Pure/PIDE/markup.scala
Fri, 20 Sep 2024 15:35:16 +0200 wenzelm block markup for specific notation, notably infix and binder;
Tue, 26 Mar 2024 21:34:08 +0100 wenzelm more robust: untyped/unscoped markup elements need to reside in module Markup for minimal static checking (see also 11a1f4d7af51);
Sun, 09 Jul 2023 17:39:46 +0200 wenzelm more markup for command_span: this allows to reconstruct Thy_Element structure without knowing the outer syntax;
less more (0) -100 -30 -10 -3 tip