# HG changeset patch
# User wenzelm
# Date 1727194659 -7200
# Node ID fd7a70babec1ce6153dfbe142a6049ec4fd2d1dc
# Parent  334625aec7a4f3d07cdf7e3dd14fc5248abad2d0
more markup <expression kind="item"> in Isabelle/Scala, with pro-forma Markup_Kind.setup in Isabelle/ML;

diff -r 334625aec7a4 -r fd7a70babec1 src/Pure/General/pretty.scala
--- 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))
           }
diff -r 334625aec7a4 -r fd7a70babec1 src/Pure/PIDE/markup.scala
--- 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))
   }
 
 
diff -r 334625aec7a4 -r fd7a70babec1 src/Pure/PIDE/markup_kind.ML
--- 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>));