# HG changeset patch
# User wenzelm
# Date 1726509508 -7200
# Node ID 510f6cb6721edce1c06c341ae96fa3722c2a1ac0
# Parent  c5ea0cb4dd914838ee40b8ce48766061b66194db
more formal Markup.expression;

diff -r c5ea0cb4dd91 -r 510f6cb6721e src/Pure/PIDE/markup_expression.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/markup_expression.ML	Mon Sep 16 19:58:28 2024 +0200
@@ -0,0 +1,38 @@
+(*  Title:      Pure/markup_expression.ML
+    Author:     Makarius
+
+Formally defined kind for Markup.expression.
+*)
+
+signature MARKUP_EXPRESSION =
+sig
+  val check_kind: Proof.context -> xstring * Position.T -> string
+  val setup_kind: binding -> theory -> string * theory
+  val setup: binding -> Markup.T
+end;
+
+structure Markup_Expression: MARKUP_EXPRESSION =
+struct
+
+(* theory data *)
+
+structure Data = Theory_Data
+(
+  type T = unit Name_Space.table;
+  val empty : T = Name_Space.empty_table "markup_expression_kind";
+  fun merge data : T = Name_Space.merge_tables data;
+);
+
+fun check_kind ctxt =
+  Name_Space.check (Context.Proof ctxt) (Data.get (Proof_Context.theory_of ctxt)) #> #1;
+
+fun setup_kind binding thy =
+  let
+    val context = Name_Space.map_naming (K Name_Space.global_naming) (Context.Theory thy);
+    val (name, data') = Name_Space.define context true (binding, ()) (Data.get thy);
+  in (name, Data.put data' thy) end;
+
+fun setup binding =
+  Context.>>> (Context.map_theory_result (setup_kind binding #>> Markup.expression));
+
+end;
diff -r c5ea0cb4dd91 -r 510f6cb6721e src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Mon Sep 16 19:36:20 2024 +0200
+++ b/src/Pure/PIDE/rendering.scala	Mon Sep 16 19:58:28 2024 +0200
@@ -664,8 +664,10 @@
             Some(info + (r0, true, XML.Text("language: " + lang.description)))
 
           case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind), _))) =>
-            val descr = if (kind == "") "expression" else "expression: " + kind
-            Some(info + (r0, true, XML.Text(descr)))
+            val description =
+              if (kind.isEmpty) "expression"
+              else "expression: " + Word.implode(Word.explode('_', kind))
+            Some(info + (r0, true, XML.Text(description)))
 
           case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
             Some(info + (r0, true, XML.Text("Markdown: paragraph")))
diff -r c5ea0cb4dd91 -r 510f6cb6721e src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Sep 16 19:36:20 2024 +0200
+++ b/src/Pure/ROOT.ML	Mon Sep 16 19:58:28 2024 +0200
@@ -114,6 +114,9 @@
 ML_file "context.ML";
 ML_file "config.ML";
 ML_file "context_position.ML";
+ML_file "General/completion.ML";
+ML_file "General/name_space.ML";
+ML_file "PIDE/markup_expression.ML";
 ML_file "soft_type_system.ML";
 
 
@@ -158,8 +161,6 @@
 ML_file "term_ord.ML";
 ML_file "term_items.ML";
 ML_file "term_subst.ML";
-ML_file "General/completion.ML";
-ML_file "General/name_space.ML";
 ML_file "sorts.ML";
 ML_file "type.ML";
 ML_file "logic.ML";
diff -r c5ea0cb4dd91 -r 510f6cb6721e src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Mon Sep 16 19:36:20 2024 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Mon Sep 16 19:58:28 2024 +0200
@@ -188,6 +188,13 @@
 
 local
 
+val markup_block_begin = Markup_Expression.setup (Binding.make ("mixfix_block_begin", \<^here>));
+val markup_block_end = Markup_Expression.setup (Binding.make ("mixfix_block_end", \<^here>));
+val markup_delimiter = Markup_Expression.setup (Binding.make ("mixfix_delimiter", \<^here>));
+val markup_argument = Markup_Expression.setup (Binding.make ("mixfix_argument", \<^here>));
+val markup_space = Markup_Expression.setup (Binding.make ("mixfix_space", \<^here>));
+val markup_break = Markup_Expression.setup (Binding.make ("mixfix_break", \<^here>));
+
 open Basic_Symbol_Pos;
 
 val err_prefix = "Error in mixfix annotation: ";
@@ -196,17 +203,16 @@
 fun scan_many pred = Scan.many (pred o Symbol_Pos.symbol);
 fun scan_many1 pred = Scan.many1 (pred o Symbol_Pos.symbol);
 
-fun reports_of_block pos =
-  [(pos, Markup.expression "mixfix block begin"), (pos, Markup.keyword3)];
+fun reports_of_block pos = [(pos, markup_block_begin), (pos, Markup.keyword3)];
 
 fun reports_of (xsym, pos) =
   (case xsym of
-    Delim _ => [(pos, Markup.expression "mixfix delimiter"), (pos, Markup.literal)]
-  | Argument _ => [(pos, Markup.expression "mixfix argument")]
-  | Space _ => [(pos, Markup.expression "mixfix space")]
+    Delim _ => [(pos, markup_delimiter), (pos, Markup.literal)]
+  | Argument _ => [(pos, markup_argument)]
+  | Space _ => [(pos, markup_space)]
   | Bg _ => reports_of_block pos
-  | Brk _ => [(pos, Markup.expression "mixfix break"), (pos, Markup.keyword3)]
-  | En => [(pos, Markup.expression "mixfix block end"), (pos, Markup.keyword3)]);
+  | Brk _ => [(pos, markup_break), (pos, Markup.keyword3)]
+  | En => [(pos, markup_block_end), (pos, Markup.keyword3)]);
 
 fun reports_text_of (xsym, pos) =
   (case xsym of