--- a/src/Pure/PIDE/markup.ML Sun Sep 22 15:58:55 2024 +0200
+++ b/src/Pure/PIDE/markup.ML Sun Sep 22 16:04:44 2024 +0200
@@ -473,7 +473,7 @@
val unbreakableN = "unbreakable";
val indentN = "indent";
-val block_properties = [notationN, expressionN, markupN, consistentN, unbreakableN, indentN];
+val block_properties = [notationN, markupN, consistentN, unbreakableN, indentN];
val widthN = "width";
--- a/src/Pure/Syntax/syntax_ext.ML Sun Sep 22 15:58:55 2024 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML Sun Sep 22 16:04:44 2024 +0200
@@ -202,10 +202,6 @@
fun get_notation_markup ctxt =
get_property NONE (SOME Markup.notation0) (SOME o parse_notation ctxt) Markup.notationN;
-fun get_expression_markup ctxt =
- get_property NONE (SOME Markup.expression0) (SOME o Markup_Kind.check_expression ctxt)
- Markup.expressionN;
-
end;
@@ -250,9 +246,7 @@
let
val props = read_properties ss;
- val more_markups =
- the_list (get_notation_markup ctxt props) @
- the_list (get_expression_markup ctxt props);
+ val more_markups = the_list (get_notation_markup ctxt props);
val markup_name = get_string Markup.markupN props;
val markup_props = props |> map_filter (fn (a, opt_b) =>