# HG changeset patch
# User wenzelm
# Date 1727013884 -7200
# Node ID e0b958719301e3b48bb4f4376ca64220a5de29cf
# Parent  a37ed1aeb1639787889b6485074815031d5d168e
remove specific support for "expression" block markup: prefer "notation";

diff -r a37ed1aeb163 -r e0b958719301 src/Pure/PIDE/markup.ML
--- 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";
 
diff -r a37ed1aeb163 -r e0b958719301 src/Pure/Syntax/syntax_ext.ML
--- 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) =>