# HG changeset patch
# User wenzelm
# Date 1726831855 -7200
# Node ID 6ddbfad8ca208cd1d5785006df5d32732fb046b0
# Parent  d794caea94a547716c077441fe56d1fdce09f7b9
tuned;

diff -r d794caea94a5 -r 6ddbfad8ca20 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Fri Sep 20 11:19:23 2024 +0200
+++ b/src/Pure/PIDE/markup.ML	Fri Sep 20 13:30:55 2024 +0200
@@ -68,6 +68,7 @@
   val position_property: Properties.entry -> bool
   val def_name: string -> string
   val expressionN: string val expression: string -> T
+  val expression0: T
   val citationN: string val citation: string -> T
   val pathN: string val path: string -> T
   val export_pathN: string val export_path: string -> T
@@ -438,6 +439,8 @@
 val expressionN = "expression";
 fun expression kind = (expressionN, kind_proper kind);
 
+val expression0 = (expressionN, []);
+
 
 (* citation *)
 
diff -r d794caea94a5 -r 6ddbfad8ca20 src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Fri Sep 20 11:19:23 2024 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Fri Sep 20 13:30:55 2024 +0200
@@ -172,7 +172,7 @@
 val get_nat = get_property 0 1 (Value.parse_nat o #1);
 
 fun get_expression_markup ctxt =
-  get_property NONE (SOME (Markup.expression "")) (SOME o Markup_Expression.check ctxt)
+  get_property NONE (SOME Markup.expression0) (SOME o Markup_Expression.check ctxt)
     Markup.expressionN;
 
 end;