more markup <expression kind="item"> in Isabelle/Scala, with pro-forma Markup_Kind.setup in Isabelle/ML;
--- a/src/Pure/General/pretty.scala Tue Sep 24 17:57:42 2024 +0200
+++ b/src/Pure/General/pretty.scala Tue Sep 24 18:17:39 2024 +0200
@@ -166,7 +166,8 @@
case Markup.Break(width, indent) =>
List(Break(false, force_nat(width), force_nat(indent)))
case Markup(Markup.ITEM, _) =>
- List(make_block(make_tree(bullet ::: body), indent = 2))
+ List(make_block(make_tree(bullet ::: body),
+ markup = Markup.Expression.item, indent = 2))
case _ =>
List(make_block(make_tree(body), markup = markup))
}
--- a/src/Pure/PIDE/markup.scala Tue Sep 24 17:57:42 2024 +0200
+++ b/src/Pure/PIDE/markup.scala Tue Sep 24 18:17:39 2024 +0200
@@ -184,6 +184,8 @@
case Markup(EXPRESSION, props) => Some(Kind.get(props))
case _ => None
}
+
+ val item: Markup = Markup(EXPRESSION, Kind(ITEM))
}
--- a/src/Pure/PIDE/markup_kind.ML Tue Sep 24 17:57:42 2024 +0200
+++ b/src/Pure/PIDE/markup_kind.ML Tue Sep 24 18:17:39 2024 +0200
@@ -16,6 +16,7 @@
val setup_expression_kind: binding -> theory -> string * theory
val check_expression: Proof.context -> xstring * Position.T -> Markup.T
val setup_expression: binding -> Markup.T
+ val markup_item: Markup.T
val markup_mixfix: Markup.T
val markup_prefix: Markup.T
val markup_postfix: Markup.T
@@ -92,6 +93,8 @@
(* concrete markup *)
+val markup_item = setup_expression (Binding.make ("item", \<^here>));
+
val markup_mixfix = setup_notation (Binding.make ("mixfix", \<^here>));
val markup_prefix = setup_notation (Binding.make ("prefix", \<^here>));
val markup_postfix = setup_notation (Binding.make ("postfix", \<^here>));