# HG changeset patch
# User wenzelm
# Date 1727008894 -7200
# Node ID 1a52cc1c327440a6b8d1c50eb09bf73d7e1eb3fa
# Parent  e87d96ac5277c3a5507ab46e3401dc902dd799c3
clarified modules and signature;

diff -r e87d96ac5277 -r 1a52cc1c3274 src/Pure/PIDE/markup_expression.ML
--- a/src/Pure/PIDE/markup_expression.ML	Sun Sep 22 14:33:03 2024 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-(*  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 check: Proof.context -> xstring * Position.T -> Markup.T
-  val setup: binding -> Markup.T
-  val markup_type: Markup.T
-  val markup_type_application: Markup.T
-  val markup_term: Markup.T
-  val markup_term_application: Markup.T
-  val markup_term_abstraction: Markup.T
-  val markup_prop: Markup.T
-  val markup_prop_application: Markup.T
-  val markup_prop_abstraction: 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;
-);
-
-
-(* kind *)
-
-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;
-
-
-(* markup *)
-
-fun check ctxt = check_kind ctxt #> Markup.expression;
-
-fun setup binding =
-  Context.>>> (Context.map_theory_result (setup_kind binding #>> Markup.expression));
-
-
-(* concrete markup *)
-
-val markup_type = setup (Binding.make ("type", \<^here>));
-val markup_type_application = setup (Binding.make ("type_application", \<^here>));
-
-val markup_term = setup (Binding.make ("term", \<^here>));
-val markup_term_application = setup (Binding.make ("term_application", \<^here>));
-val markup_term_abstraction = setup (Binding.make ("term_abstraction", \<^here>));
-
-val markup_prop = setup (Binding.make ("prop", \<^here>));
-val markup_prop_application = setup (Binding.make ("prop_application", \<^here>));
-val markup_prop_abstraction = setup (Binding.make ("prop_abstraction", \<^here>));
-
-end;
diff -r e87d96ac5277 -r 1a52cc1c3274 src/Pure/PIDE/markup_kind.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/markup_kind.ML	Sun Sep 22 14:41:34 2024 +0200
@@ -0,0 +1,69 @@
+(*  Title:      Pure/markup_kind.ML
+    Author:     Makarius
+
+Formally defined kind for Markup.expression.
+*)
+
+signature MARKUP_KIND =
+sig
+  val check_expression_kind: Proof.context -> xstring * Position.T -> string
+  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_type: Markup.T
+  val markup_type_application: Markup.T
+  val markup_term: Markup.T
+  val markup_term_application: Markup.T
+  val markup_term_abstraction: Markup.T
+  val markup_prop: Markup.T
+  val markup_prop_application: Markup.T
+  val markup_prop_abstraction: Markup.T
+end;
+
+structure Markup_Kind: MARKUP_KIND =
+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;
+);
+
+
+(* kind *)
+
+fun check_expression_kind ctxt =
+  Name_Space.check (Context.Proof ctxt) (Data.get (Proof_Context.theory_of ctxt)) #> #1;
+
+fun setup_expression_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;
+
+
+(* markup *)
+
+fun check_expression ctxt = check_expression_kind ctxt #> Markup.expression;
+
+fun setup_expression binding =
+  Context.>>> (Context.map_theory_result (setup_expression_kind binding #>> Markup.expression));
+
+
+(* concrete markup *)
+
+val markup_type = setup_expression (Binding.make ("type", \<^here>));
+val markup_type_application = setup_expression (Binding.make ("type_application", \<^here>));
+
+val markup_term = setup_expression (Binding.make ("term", \<^here>));
+val markup_term_application = setup_expression (Binding.make ("term_application", \<^here>));
+val markup_term_abstraction = setup_expression (Binding.make ("term_abstraction", \<^here>));
+
+val markup_prop = setup_expression (Binding.make ("prop", \<^here>));
+val markup_prop_application = setup_expression (Binding.make ("prop_application", \<^here>));
+val markup_prop_abstraction = setup_expression (Binding.make ("prop_abstraction", \<^here>));
+
+end;
diff -r e87d96ac5277 -r 1a52cc1c3274 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sun Sep 22 14:33:03 2024 +0200
+++ b/src/Pure/ROOT.ML	Sun Sep 22 14:41:34 2024 +0200
@@ -116,7 +116,7 @@
 ML_file "context_position.ML";
 ML_file "General/completion.ML";
 ML_file "General/name_space.ML";
-ML_file "PIDE/markup_expression.ML";
+ML_file "PIDE/markup_kind.ML";
 ML_file "soft_type_system.ML";
 
 
diff -r e87d96ac5277 -r 1a52cc1c3274 src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Sun Sep 22 14:33:03 2024 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Sun Sep 22 14:41:34 2024 +0200
@@ -194,7 +194,7 @@
   get_property NONE (SOME Markup.notation0) (SOME o parse_notation) Markup.notationN;
 
 fun get_expression_markup ctxt =
-  get_property NONE (SOME Markup.expression0) (SOME o Markup_Expression.check ctxt)
+  get_property NONE (SOME Markup.expression0) (SOME o Markup_Kind.check_expression ctxt)
     Markup.expressionN;
 
 end;
@@ -204,12 +204,12 @@
 
 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>));
+val markup_block_begin = Markup_Kind.setup_expression (Binding.make ("mixfix_block_begin", \<^here>));
+val markup_block_end = Markup_Kind.setup_expression (Binding.make ("mixfix_block_end", \<^here>));
+val markup_delimiter = Markup_Kind.setup_expression (Binding.make ("mixfix_delimiter", \<^here>));
+val markup_argument = Markup_Kind.setup_expression (Binding.make ("mixfix_argument", \<^here>));
+val markup_space = Markup_Kind.setup_expression (Binding.make ("mixfix_space", \<^here>));
+val markup_break = Markup_Kind.setup_expression (Binding.make ("mixfix_break", \<^here>));
 
 open Basic_Symbol_Pos;
 
diff -r e87d96ac5277 -r 1a52cc1c3274 src/Pure/Tools/rail.ML
--- a/src/Pure/Tools/rail.ML	Sun Sep 22 14:33:03 2024 +0200
+++ b/src/Pure/Tools/rail.ML	Sun Sep 22 14:41:34 2024 +0200
@@ -182,17 +182,17 @@
 fun null_trees (CAT ([], _)) = true
   | null_trees _ = false;
 
-val markup_concat = Markup_Expression.setup \<^binding>\<open>rail_concat\<close>;
-val markup_union = Markup_Expression.setup \<^binding>\<open>rail_union\<close>;
-val markup_repeat = Markup_Expression.setup \<^binding>\<open>rail_repeat\<close>;
-val markup_repeat1 = Markup_Expression.setup \<^binding>\<open>rail_repeat1\<close>;
-val markup_enum = Markup_Expression.setup \<^binding>\<open>rail_enum\<close>;
-val markup_enum1 = Markup_Expression.setup \<^binding>\<open>rail_enum1\<close>;
-val markup_maybe = Markup_Expression.setup \<^binding>\<open>rail_maybe\<close>;
-val markup_newline = Markup_Expression.setup \<^binding>\<open>rail_newline\<close>;
-val markup_nonterminal = Markup_Expression.setup \<^binding>\<open>rail_nonterminal\<close>;
-val markup_terminal = Markup_Expression.setup \<^binding>\<open>rail_terminal\<close>;
-val markup_antiquote = Markup_Expression.setup \<^binding>\<open>rail_antiquote\<close>;
+val markup_concat = Markup_Kind.setup_expression \<^binding>\<open>rail_concat\<close>;
+val markup_union = Markup_Kind.setup_expression \<^binding>\<open>rail_union\<close>;
+val markup_repeat = Markup_Kind.setup_expression \<^binding>\<open>rail_repeat\<close>;
+val markup_repeat1 = Markup_Kind.setup_expression \<^binding>\<open>rail_repeat1\<close>;
+val markup_enum = Markup_Kind.setup_expression \<^binding>\<open>rail_enum\<close>;
+val markup_enum1 = Markup_Kind.setup_expression \<^binding>\<open>rail_enum1\<close>;
+val markup_maybe = Markup_Kind.setup_expression \<^binding>\<open>rail_maybe\<close>;
+val markup_newline = Markup_Kind.setup_expression \<^binding>\<open>rail_newline\<close>;
+val markup_nonterminal = Markup_Kind.setup_expression \<^binding>\<open>rail_nonterminal\<close>;
+val markup_terminal = Markup_Kind.setup_expression \<^binding>\<open>rail_terminal\<close>;
+val markup_antiquote = Markup_Kind.setup_expression \<^binding>\<open>rail_antiquote\<close>;
 
 fun reports_of_tree ctxt =
   if Context_Position.reports_enabled ctxt then