remove specific support for "expression" block markup: prefer "notation";
authorwenzelm
Sun, 22 Sep 2024 16:04:44 +0200
changeset 80922 e0b958719301
parent 80921 a37ed1aeb163
child 80923 6c9628a116cc
remove specific support for "expression" block markup: prefer "notation";
src/Pure/PIDE/markup.ML
src/Pure/Syntax/syntax_ext.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";
 
--- 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) =>