Sun, 29 Jun 2025 16:16:22 +0200 |
wenzelm |
clarified signature: more explicit operations;
|
file |
diff |
annotate
|
Fri, 21 Mar 2025 18:37:05 +0100 |
wenzelm |
support for writeln_urgent, which is shown in Output before state messages (reminiscent of old Output.urgent_message before 521cea5fa777);
|
file |
diff |
annotate
|
Mon, 23 Dec 2024 14:09:43 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 18 Dec 2024 16:03:07 +0100 |
wenzelm |
more uniform Markup.notation vs. Markup.expression;
|
file |
diff |
annotate
|
Sun, 08 Dec 2024 20:09:14 +0100 |
wenzelm |
more markup (without rendering): class, type constructor, term constant --- similar to free, bound, etc.;
|
file |
diff |
annotate
|
Sat, 07 Dec 2024 23:50:18 +0100 |
wenzelm |
clarified term positions and markup: syntax = true means this is via concrete syntax;
|
file |
diff |
annotate
|
Mon, 28 Oct 2024 08:48:31 +0100 |
wenzelm |
removed obsolete markup for "open_block" (see also d5ad89fda714): Isabelle/Scala directly supports XML.Elem pretty-printing;
|
file |
diff |
annotate
|
Sun, 06 Oct 2024 18:34:35 +0200 |
wenzelm |
support for pretty blocks that are "open" and thus have no impact on formatting, only on markup;
|
file |
diff |
annotate
|
Sun, 06 Oct 2024 13:02:33 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Tue, 24 Sep 2024 18:17:39 +0200 |
wenzelm |
more markup <expression kind="item"> in Isabelle/Scala, with pro-forma Markup_Kind.setup in Isabelle/ML;
|
file |
diff |
annotate
|
Fri, 20 Sep 2024 15:35:16 +0200 |
wenzelm |
block markup for specific notation, notably infix and binder;
|
file |
diff |
annotate
|
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);
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Wed, 10 May 2023 20:30:46 +0200 |
wenzelm |
more informative position information;
|
file |
diff |
annotate
|