more uniform treatment of Markup.notation and Markup.expression: manage kinds via context;

--- a/src/Pure/PIDE/markup.ML	Sun Sep 22 14:41:34 2024 +0200
+++ b/src/Pure/PIDE/markup.ML	Sun Sep 22 15:46:19 2024 +0200
@@ -67,13 +67,7 @@
   val position_properties: string list
   val position_property: Properties.entry -> bool
   val def_name: string -> string
-  val notation_mixfixN: string
-  val notation_prefixN: string
-  val notation_postfixN: string
-  val notation_infixN: string
-  val notation_binderN: string
-  val notations: string list
-  val notationN: string val notation: {kind: string, name: string} -> T
+  val notationN: string val notation: string -> T
   val notation0: T
   val expressionN: string val expression: string -> T
   val expression0: T
@@ -442,18 +436,10 @@
   | NONE => make_def a);
 
 
-(* notation: mixfix annotations *)
-
-val notation_mixfixN = "mixfix";
-val notation_prefixN = "prefix";
-val notation_postfixN = "postfix";
-val notation_infixN = "infix";
-val notation_binderN = "binder";
-val notations =
-  [notation_mixfixN, notation_prefixN, notation_postfixN, notation_infixN, notation_binderN];
+(* notation -- inner syntax clause *)
 
 val notationN = "notation";
-fun notation {kind, name} = (notationN, kind_proper kind @ name_proper name);
+fun notation kind = (notationN, kind_proper kind);
 
 val notation0 = (notationN, []);
 

--- a/src/Pure/PIDE/markup_kind.ML	Sun Sep 22 14:41:34 2024 +0200
+++ b/src/Pure/PIDE/markup_kind.ML	Sun Sep 22 15:46:19 2024 +0200
@@ -1,15 +1,26 @@
 (*  Title:      Pure/markup_kind.ML
     Author:     Makarius
 
-Formally defined kind for Markup.expression.
+Formally defined kind for Markup.notation and Markup.expression.
 *)
 
 signature MARKUP_KIND =
 sig
+  val get_notation_kinds: Proof.context -> string list
+  val check_notation_kind: Proof.context -> xstring * Position.T -> string
+  val setup_notation_kind: binding -> theory -> string * theory
+  val check_notation: Proof.context -> xstring * Position.T -> Markup.T
+  val setup_notation: binding -> Markup.T
+  val get_expression_kinds: Proof.context -> string list
   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_mixfix: Markup.T
+  val markup_prefix: Markup.T
+  val markup_postfix: Markup.T
+  val markup_infix: Markup.T
+  val markup_binder: Markup.T
   val markup_type: Markup.T
   val markup_type_application: Markup.T
   val markup_term: Markup.T
@@ -27,34 +38,70 @@
 
 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;
+  type T = unit Name_Space.table * unit Name_Space.table;
+  val empty : T =
+   (Name_Space.empty_table "markup_notation_kind",
+    Name_Space.empty_table "markup_expression_kind");
+  fun merge ((tab1, tab2), (tab1', tab2')) : T =
+   (Name_Space.merge_tables (tab1, tab1'),
+    Name_Space.merge_tables (tab2, tab2'));
 );
 
 
 (* kind *)
 
-fun check_expression_kind ctxt =
-  Name_Space.check (Context.Proof ctxt) (Data.get (Proof_Context.theory_of ctxt)) #> #1;
+local
 
-fun setup_expression_kind binding thy =
+fun get_kinds which ctxt =
+  which (Data.get (Proof_Context.theory_of ctxt))
+  |> Name_Space.dest_table
+  |> map #1
+  |> sort_strings;
+
+fun check_kind which ctxt =
+  Name_Space.check (Context.Proof ctxt) (which (Data.get (Proof_Context.theory_of ctxt))) #> #1;
+
+fun setup_kind which ap 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;
+    val (name, tab') = Name_Space.define context true (binding, ()) (which (Data.get thy));
+  in (name, (Data.map o ap) (K tab') thy) end;
+
+in
+
+val get_notation_kinds = get_kinds #1;
+val get_expression_kinds = get_kinds #2;
+
+val check_notation_kind = check_kind #1;
+val check_expression_kind = check_kind #2;
+
+val setup_notation_kind = setup_kind #1 apfst;
+val setup_expression_kind = setup_kind #2 apsnd;
+
+end;
 
 
 (* markup *)
 
+fun check_notation ctxt = check_notation_kind ctxt #> Markup.notation;
+
 fun check_expression ctxt = check_expression_kind ctxt #> Markup.expression;
 
+fun setup_notation binding =
+  Context.>>> (Context.map_theory_result (setup_notation_kind binding #>> Markup.notation));
+
 fun setup_expression binding =
   Context.>>> (Context.map_theory_result (setup_expression_kind binding #>> Markup.expression));
 
 
 (* concrete markup *)
 
+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>));
+val markup_infix = setup_notation (Binding.make ("infix", \<^here>));
+val markup_binder = setup_notation (Binding.make ("binder", \<^here>));
+
 val markup_type = setup_expression (Binding.make ("type", \<^here>));
 val markup_type_application = setup_expression (Binding.make ("type_application", \<^here>));
 

--- a/src/Pure/Syntax/mixfix.ML	Sun Sep 22 14:41:34 2024 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Sun Sep 22 15:46:19 2024 +0200
@@ -160,13 +160,11 @@
 val infix_arg1 = Symbol_Pos.explode0 "_ ";
 val infix_arg2 = Symbol_Pos.explode0 "/ _)";
 
-fun infix_block ctxt ss =
-  Syntax_Ext.make_notation
-   {kind = Markup.notation_infixN,
-    name = Syntax_Ext.mfix_name ctxt ss}
-  |> cartouche
-  |> Symbol_Pos.explode0
-  |> append infix_bg;
+fun infix_block ctxt =
+  Syntax_Ext.mfix_name ctxt #>
+  Syntax_Ext.block_annotation 0 Markup_Kind.markup_infix #>
+  Symbol_Pos.explode0 #>
+  append infix_bg;
 
 
 (* binder notation *)
@@ -177,15 +175,11 @@
 val binder_bg = Symbol_Pos.explode0 "(";
 val binder_en = Symbol_Pos.explode0 "_./ _)";
 
-fun binder_block ctxt ss =
-  implode_space
-   ["indent=3",
-    Syntax_Ext.make_notation
-     {kind = Markup.notation_binderN,
-      name = Syntax_Ext.mfix_name ctxt ss}]
-  |> cartouche
-  |> Symbol_Pos.explode0
-  |> append binder_bg;
+fun binder_block ctxt =
+  Syntax_Ext.mfix_name ctxt #>
+  Syntax_Ext.block_annotation 3 Markup_Kind.markup_binder #>
+  Symbol_Pos.explode0 #>
+  append binder_bg;
 
 fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) =
       [Type ("idts", []), ty2] ---> ty3

--- a/src/Pure/Syntax/syntax_ext.ML	Sun Sep 22 14:41:34 2024 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Sun Sep 22 15:46:19 2024 +0200
@@ -29,7 +29,7 @@
       print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list,
       print_rules: (Ast.ast * Ast.ast) list,
       print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list}
-  val make_notation: {kind: string, name: string} -> string
+  val block_annotation: int -> Markup.T -> string -> string
   val mfix_name: Proof.context -> Symbol_Pos.T list -> string
   val mfix_args: Proof.context -> Symbol_Pos.T list -> int
   val mixfix_args: Proof.context -> Input.source -> int
@@ -123,8 +123,17 @@
 
 (* properties *)
 
-fun make_notation {kind, name} =
-  Properties.print_eq (Markup.notationN, cartouche (implode_space (remove (op =) "" [kind, name])));
+fun block_annotation indent notation_markup notation_name =
+  let
+    val (elem, props) = notation_markup |> notation_name <> "" ? Markup.name notation_name;
+    val kind = Properties.get props Markup.kindN;
+    val name = Properties.get props Markup.nameN;
+    val s1 = if indent = 0 then [] else ["indent=" ^ Value.print_int indent];
+    val s2 =
+      if elem = Markup.notationN then
+        [Properties.print_eq (elem, cartouche (implode_space (the_list kind @ the_list name)))]
+      else raise Fail ("Bad markup element for notatio: " ^ quote elem)
+  in cartouche (implode_space (s1 @ s2)) end;
 
 fun show_names names =
   commas_quote (map (fn (name, pos) => Markup.markup (Position.markup pos) name) names);
@@ -157,19 +166,19 @@
       (parse (b, pos2) handle Fail msg =>
         error (msg ^ " for property " ^ quote name ^ Position.here_list [pos1, pos2])));
 
-fun parse_notation (s, pos) =
+fun parse_notation ctxt (s, pos) =
   let
     val (kind, name) =
       (case Symbol.explode_words s of
         [] => ("", "")
       | a :: bs => (a, space_implode " " bs));
-  in
-    if kind = "" orelse member (op =) Markup.notations kind then
-      Markup.notation {kind = kind, name = name}
-    else
-      error ("Bad notation kind " ^ quote kind ^ Position.here pos ^
-        ", expected: " ^ commas_quote Markup.notations)
-  end;
+    val markup =
+      (case try (fn () => Markup_Kind.check_notation ctxt (kind, Position.none)) () of
+        SOME m => m
+      | NONE =>
+          error ("Bad notation kind " ^ quote kind ^ Position.here pos ^
+            ", expected: " ^ commas_quote (Markup_Kind.get_notation_kinds ctxt)));
+  in markup |> Markup.properties (Markup.name_proper name) end;
 
 in
 
@@ -190,8 +199,8 @@
 val get_bool = get_property false true (Value.parse_bool o #1);
 val get_nat = get_property 0 1 (Value.parse_nat o #1);
 
-val get_notation_markup =
-  get_property NONE (SOME Markup.notation0) (SOME o parse_notation) Markup.notationN;
+fun get_notation_markup ctxt =
+  get_property NONE (SOME Markup.notation0) (SOME o parse_notation ctxt) Markup.notationN;
 
 fun get_expression_markup ctxt =
   get_property NONE (SOME Markup.expression0) (SOME o Markup_Kind.check_expression ctxt)
@@ -242,7 +251,7 @@
     val props = read_properties ss;
 
     val more_markups =
-      the_list (get_notation_markup props) @
+      the_list (get_notation_markup ctxt props) @
       the_list (get_expression_markup ctxt props);
 
     val markup_name = get_string Markup.markupN props;