# HG changeset patch
# User wenzelm
# Date 1728048061 -7200
# Node ID 6538332c08e0694775198ffb2a46e6b6178cf4b1
# Parent  6fefd6c602fa072c96a04b48b67751f9b34e8f3c
documentation for pretty block "notation" markup;

diff -r 6fefd6c602fa -r 6538332c08e0 src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Fri Oct 04 13:29:33 2024 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Fri Oct 04 15:21:01 2024 +0200
@@ -410,13 +410,48 @@
     This allows to specify free-form PIDE markup, e.g.\ for specialized
     output.
 
+    \<^item> \<open>notation\<close> (cartouche): a semi-formal description of the notation that
+    is surrounded by the block parentheses. The cartouche consists of multiple
+    words (separated by white-space). The first word specifies the \<^emph>\<open>kind\<close> of
+    notation as follows:
+
+      \<^item> @{notation_kind_def mixfix}: general mixfix notation, with delimiters
+      surrounding its arguments.
+
+      \<^item> @{notation_kind_def prefix}: notation with delimiters before its
+      arguments.
+
+      \<^item> @{notation_kind_def postfix}: notation with delimiters after its
+      arguments.
+
+      \<^item> @{notation_kind_def "infix"}: notation with delimiters between its
+      arguments (automatically inserted for @{keyword "infix"} annotations,
+      see \secref{sec:infixes}).
+
+      \<^item> @{notation_kind_def "binder"}: notation that binds variables within
+      its body argument (automatically inserted for @{keyword "binder"}
+      annotations, see \secref{sec:binders}).
+
+      \<^item> @{notation_kind_def type_application}: application of a type
+      constructor to its arguments.
+
+      \<^item> @{notation_kind_def application}: \<open>\<lambda>\<close>-term application.
+
+      \<^item> @{notation_kind_def abstraction}: \<open>\<lambda>\<close>-term abstraction.
+
+      \<^item> @{notation_kind_def judgment}: judgment form of the object-logic
+      (usually without delimiters).
+
+    Plenty of examples may be found in the Isabelle sources by searching for
+    ``\<^verbatim>\<open>notation=\<close>''.
+
   \<^medskip>
   Note that the general idea of pretty printing with blocks and breaks is
   described in \<^cite>\<open>"paulson-ml2"\<close>; it goes back to \<^cite>\<open>"Oppen:1980"\<close>.
 \<close>
 
 
-subsection \<open>Infixes\<close>
+subsection \<open>Infixes \label{sec:infixes}\<close>
 
 text \<open>
   Infix operators are specified by convenient short forms that abbreviate
@@ -448,7 +483,7 @@
 \<close>
 
 
-subsection \<open>Binders\<close>
+subsection \<open>Binders \label{sec:binders}\<close>
 
 text \<open>
   A \<^emph>\<open>binder\<close> is a variable-binding construct such as a quantifier. The idea
diff -r 6fefd6c602fa -r 6538332c08e0 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Fri Oct 04 13:29:33 2024 +0200
+++ b/src/Doc/antiquote_setup.ML	Fri Oct 04 15:21:01 2024 +0200
@@ -119,7 +119,8 @@
     entity_antiqs no_check "isasystem" \<^binding>\<open>executable\<close> #>
     entity_antiqs Isabelle_Tool.check "isatool" \<^binding>\<open>tool\<close> #>
     entity_antiqs ML_Context.check_antiquotation "" \<^binding>\<open>ML_antiquotation\<close> #>
-    entity_antiqs (K JEdit.check_action) "isasystem" \<^binding>\<open>action\<close>);
+    entity_antiqs (K JEdit.check_action) "isasystem" \<^binding>\<open>action\<close> #>
+    entity_antiqs Markup_Kind.check_notation_kind "" \<^binding>\<open>notation_kind\<close>);
 
 end;