--- 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 *)
--- 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;