# HG changeset patch
# User wenzelm
# Date 1726839316 -7200
# Node ID 8ad5e6df050bf3f7c476aaa21ec4c16d50d18d7a
# Parent  406a85a25189241992b97941f08acf478c28b641
block markup for specific notation, notably infix and binder;
tuned;

diff -r 406a85a25189 -r 8ad5e6df050b src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Fri Sep 20 14:28:13 2024 +0200
+++ b/src/Pure/PIDE/markup.ML	Fri Sep 20 15:35:16 2024 +0200
@@ -67,6 +67,12 @@
   val position_properties: string list
   val position_property: Properties.entry -> bool
   val def_name: string -> string
+  val notation_mixfixN: string
+  val notation_infixN: string
+  val notation_binderN: string
+  val notations: string list
+  val notationN: string val notation: {kind: string, name: string} -> T
+  val notation0: T
   val expressionN: string val expression: string -> T
   val expression0: T
   val citationN: string val citation: string -> T
@@ -434,6 +440,19 @@
   | NONE => make_def a);
 
 
+(* notation: mixfix annotations *)
+
+val notation_mixfixN = "mixfix";
+val notation_infixN = "infix";
+val notation_binderN = "binder";
+val notations = [notation_mixfixN, notation_infixN, notation_binderN];
+
+val notationN = "notation";
+fun notation {kind, name} = (notationN, kind_proper kind @ name_proper name);
+
+val notation0 = (notationN, []);
+
+
 (* expression *)
 
 val expressionN = "expression";
@@ -463,7 +482,7 @@
 val unbreakableN = "unbreakable";
 val indentN = "indent";
 
-val block_properties = [expressionN, markupN, consistentN, unbreakableN, indentN];
+val block_properties = [notationN, expressionN, markupN, consistentN, unbreakableN, indentN];
 
 val widthN = "width";
 
diff -r 406a85a25189 -r 8ad5e6df050b src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Fri Sep 20 14:28:13 2024 +0200
+++ b/src/Pure/PIDE/markup.scala	Fri Sep 20 15:35:16 2024 +0200
@@ -163,6 +163,18 @@
   def def_name(a: String): String = def_names.getOrElse(a, a + "def_")
 
 
+  /* notation */
+
+  val NOTATION = "notation"
+  object Notation {
+    def unapply(markup: Markup): Option[(String, String)] =
+      markup match {
+        case Markup(NOTATION, props) => Some((Kind.get(props), Name.get(props)))
+        case _ => None
+      }
+  }
+
+
   /* expression */
 
   val EXPRESSION = "expression"
diff -r 406a85a25189 -r 8ad5e6df050b src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Fri Sep 20 14:28:13 2024 +0200
+++ b/src/Pure/PIDE/rendering.scala	Fri Sep 20 15:35:16 2024 +0200
@@ -223,8 +223,8 @@
   val text_color_elements = Markup.Elements(text_color.keySet)
 
   val tooltip_elements =
-    Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
-      Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
+    Markup.Elements(Markup.LANGUAGE, Markup.NOTATION, Markup.EXPRESSION, Markup.TIMING,
+      Markup.ENTITY, Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
       Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL,
       Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name) ++
       Markup.Elements(tooltip_descriptions.keySet)
@@ -663,6 +663,14 @@
           case (info, Text.Info(r0, XML.Elem(Markup.Language(lang), _))) =>
             Some(info + (r0, true, XML.Text("language: " + lang.description)))
 
+          case (info, Text.Info(r0, XML.Elem(Markup.Notation(kind, name), _))) =>
+            val a = kind.nonEmpty
+            val b = name.nonEmpty
+            val description =
+              if (!a && !b) "notation"
+              else "notation: " + kind + if_proper(a && b, " ") + if_proper(b, quote(name))
+            Some(info + (r0, true, XML.Text(description)))
+
           case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind), _))) =>
             val description =
               if (kind.isEmpty) "expression"
diff -r 406a85a25189 -r 8ad5e6df050b src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Fri Sep 20 14:28:13 2024 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Fri Sep 20 15:35:16 2024 +0200
@@ -151,6 +151,47 @@
   else [];
 
 
+(* infix notation *)
+
+val prefix_bg = Symbol_Pos.explode0 "'(";
+val prefix_en = Symbol_Pos.explode0 "')";
+
+val infix_bg = Symbol_Pos.explode0 "(";
+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;
+
+
+(* binder notation *)
+
+val binder_stamp = stamp ();
+val binder_name = suffix "_binder";
+
+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_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) =
+      [Type ("idts", []), ty2] ---> ty3
+  | binder_typ c _ = error ("Bad type of binder: " ^ quote c);
+
+
 (* syn_ext_types *)
 
 val typeT = Type ("type", []);
@@ -159,9 +200,10 @@
 fun syn_ext_types ctxt type_decls =
   let
     fun mk_infix sy ty t p1 p2 p3 pos =
-      Syntax_Ext.Mfix
-        (Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)",
-          ty, t, [p1, p2], p3, pos);
+      let
+        val ss = Input.source_explode sy;
+        val syms = infix_block ctxt ss @ infix_arg1 @ ss @ infix_arg2;
+      in Syntax_Ext.Mfix (syms, ty, t, [p1, p2], p3, pos) end;
 
     fun mfix_of (t, ty, mx) =
       (case mx of
@@ -190,37 +232,30 @@
 
 (* syn_ext_consts *)
 
-val binder_stamp = stamp ();
-val binder_name = suffix "_binder";
-
-fun mk_prefix sy =
-  let val sy' = Input.source_explode (Input.reset_pos sy); 
-  in Symbol_Pos.explode0 "'(" @ sy' @ Symbol_Pos.explode0 "')" end
-
 fun syn_ext_consts ctxt logical_types const_decls =
   let
     fun mk_infix sy ty c p1 p2 p3 pos =
-      [Syntax_Ext.Mfix (mk_prefix sy, ty, c, [], 1000, Position.none),
-       Syntax_Ext.Mfix
-        (Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)",
-          ty, c, [p1, p2], p3, pos)];
-
-    fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) =
-          [Type ("idts", []), ty2] ---> ty3
-      | binder_typ c _ = error ("Bad type of binder: " ^ quote c);
+      let
+        val ss0 = Input.source_explode (Input.reset_pos sy);
+        val ss = Input.source_explode sy;
+        val syms = infix_block ctxt ss @ infix_arg1 @ ss @ infix_arg2;
+      in
+        [Syntax_Ext.Mfix (prefix_bg @ ss0 @ prefix_en, ty, c, [], 1000, Position.none),
+         Syntax_Ext.Mfix (syms, ty, c, [p1, p2], p3, pos)]
+      end;
 
     fun mfix_of (c, ty, mx) =
       (case mx of
         NoSyn => []
-      | Mixfix (sy, ps, p, _) =>
-          [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, ps, p, pos_of mx)]
+      | Mixfix (sy, ps, p, _) => [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, ps, p, pos_of mx)]
       | Infix (sy, p, _) => mk_infix sy ty c (p + 1) (p + 1) p (pos_of mx)
       | Infixl (sy, p, _) => mk_infix sy ty c p (p + 1) p (pos_of mx)
       | Infixr (sy, p, _) => mk_infix sy ty c (p + 1) p p (pos_of mx)
       | Binder (sy, p, q, _) =>
-          [Syntax_Ext.Mfix
-            (Symbol_Pos.explode0 "(3" @ Input.source_explode sy @ Symbol_Pos.explode0 "_./ _)",
-              binder_typ c ty, (binder_name c), [0, p], q, pos_of mx)]
+          let
+            val ss = Input.source_explode sy;
+            val syms = binder_block ctxt ss @ ss @ binder_en;
+          in [Syntax_Ext.Mfix (syms, binder_typ c ty, binder_name c, [0, p], q, pos_of mx)] end
       | _ => error ("Bad mixfix declaration for " ^ quote c ^ Position.here (pos_of mx)));
 
     fun binder (c, _, Binder _) = SOME (binder_name c, c)
diff -r 406a85a25189 -r 8ad5e6df050b src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Fri Sep 20 14:28:13 2024 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Fri Sep 20 15:35:16 2024 +0200
@@ -29,6 +29,8 @@
       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 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
   val escape: string -> string
@@ -121,6 +123,9 @@
 
 (* properties *)
 
+fun make_notation {kind, name} =
+  Properties.print_eq (Markup.notationN, cartouche (implode_space (remove (op =) "" [kind, name])));
+
 fun show_names names =
   commas_quote (map (fn (name, pos) => Markup.markup (Position.markup pos) name) names);
 
@@ -152,6 +157,20 @@
       (parse (b, pos2) handle Fail msg =>
         error (msg ^ " for property " ^ quote name ^ Position.here_list [pos1, pos2])));
 
+fun parse_notation (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;
+
 in
 
 fun read_properties ss =
@@ -171,6 +190,9 @@
 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_expression_markup ctxt =
   get_property NONE (SOME Markup.expression0) (SOME o Markup_Expression.check ctxt)
     Markup.expressionN;
@@ -219,7 +241,9 @@
   let
     val props = read_properties ss;
 
-    val more_markups = the_list (get_expression_markup ctxt props);
+    val more_markups =
+      the_list (get_notation_markup props) @
+      the_list (get_expression_markup ctxt props);
 
     val markup_name = get_string Markup.markupN props;
     val markup_props = props |> map_filter (fn (a, opt_b) =>
@@ -286,6 +310,9 @@
 
 val read_mfix0 = read_mfix o Context_Position.set_visible false;
 
+fun mfix_name ctxt =
+  read_mfix0 ctxt #> map_filter (fn (Delim s, _) => SOME s | _ => NONE) #> space_implode " ";
+
 fun mfix_args ctxt ss =
   Integer.build (read_mfix0 ctxt ss |> fold (fn (xsymb, _) => is_argument xsymb ? Integer.add 1));
 
diff -r 406a85a25189 -r 8ad5e6df050b src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Fri Sep 20 14:28:13 2024 +0200
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Fri Sep 20 15:35:16 2024 +0200
@@ -127,7 +127,7 @@
   private val breakpoint_elements = Markup.Elements(Markup.ML_BREAKPOINT)
 
   private val highlight_elements =
-    Markup.Elements(Markup.EXPRESSION, Markup.LANGUAGE, Markup.ML_TYPING,
+    Markup.Elements(Markup.NOTATION, Markup.EXPRESSION, Markup.LANGUAGE, Markup.ML_TYPING,
       Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL,
       Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.FREE, Markup.SKOLEM,
       Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT,