# 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> \notation\ (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>\kind\ 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}: \\\-term application. + + \<^item> @{notation_kind_def abstraction}: \\\-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>\notation=\''. + \<^medskip> Note that the general idea of pretty printing with blocks and breaks is described in \<^cite>\"paulson-ml2"\; it goes back to \<^cite>\"Oppen:1980"\. \ -subsection \Infixes\ +subsection \Infixes \label{sec:infixes}\ text \ Infix operators are specified by convenient short forms that abbreviate @@ -448,7 +483,7 @@ \ -subsection \Binders\ +subsection \Binders \label{sec:binders}\ text \ A \<^emph>\binder\ 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>\executable\ #> entity_antiqs Isabelle_Tool.check "isatool" \<^binding>\tool\ #> entity_antiqs ML_Context.check_antiquotation "" \<^binding>\ML_antiquotation\ #> - entity_antiqs (K JEdit.check_action) "isasystem" \<^binding>\action\); + entity_antiqs (K JEdit.check_action) "isasystem" \<^binding>\action\ #> + entity_antiqs Markup_Kind.check_notation_kind "" \<^binding>\notation_kind\); end;