--- 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
--- 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;