# HG changeset patch # User wenzelm # Date 1226610090 -3600 # Node ID a25630deacaf01cb68a0fa8605ed9ef5949bb055 # Parent 2eeeced17228dd1889b436928c2bd8065fa3a3e7 misc tuning of inner syntax; diff -r 2eeeced17228 -r a25630deacaf doc-src/IsarRef/Thy/Inner_Syntax.thy --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Nov 13 22:00:39 2008 +0100 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Nov 13 22:01:30 2008 +0100 @@ -4,7 +4,7 @@ imports Main begin -chapter {* Inner syntax --- the term language *} +chapter {* Inner syntax --- the term language \label{ch:inner-syntax} *} section {* Printing logical entities *} @@ -302,7 +302,7 @@ general template format is a sequence over any of the following entities. - \begin{itemize} + \begin{description} \item @{text "d"} is a delimiter, namely a non-empty sequence of characters other than the following special characters: @@ -349,7 +349,7 @@ stands for the string of spaces (zero or more) right after the slash. These spaces are printed if the break is \emph{not} taken. - \end{itemize} + \end{description} For example, the template @{verbatim "(_ +/ _)"} specifies an infix operator. There are two argument positions; the delimiter @@ -389,7 +389,8 @@ \end{description} *} -section {* The Pure syntax *} + +section {* The Pure syntax \label{sec:pure-syntax} *} subsection {* Priority grammars \label{sec:priority-grammar} *} @@ -477,9 +478,9 @@ \begin{center} \begin{supertabular}{rclr} - @{text any} & = & @{text "prop | logic"} \\\\ + @{syntax_def (inner) any} & = & @{text "prop | logic"} \\\\ - @{text prop} & = & @{verbatim "("} @{text prop} @{verbatim ")"} \\ + @{syntax_def (inner) prop} & = & @{verbatim "("} @{text prop} @{verbatim ")"} \\ & @{text "|"} & @{text "prop\<^sup>(\<^sup>4\<^sup>)"} @{verbatim "::"} @{text type} & @{text "(3)"} \\ & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=?="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\ & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\ @@ -494,10 +495,10 @@ & @{text "|"} & @{verbatim SORT_CONSTRAINT} @{verbatim "("} @{text type} @{verbatim ")"} \\ & @{text "|"} & @{verbatim PROP} @{text aprop} \\\\ - @{text aprop} & = & @{text "id | longid | var | "}@{verbatim "_"}@{text " | "}@{verbatim "..."} \\ + @{syntax_def (inner) aprop} & = & @{text "id | longid | var | "}@{verbatim "_"}@{text " | "}@{verbatim "..."} \\ & @{text "|"} & @{text "logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \ any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "(999)"} \\\\ - @{text logic} & = & @{verbatim "("} @{text logic} @{verbatim ")"} \\ + @{syntax_def (inner) logic} & = & @{verbatim "("} @{text logic} @{verbatim ")"} \\ & @{text "|"} & @{text "logic\<^sup>(\<^sup>4\<^sup>)"} @{verbatim "::"} @{text type} & @{text "(3)"} \\ & @{text "|"} & @{text "id | longid | var | "}@{verbatim "_"}@{text " | "}@{verbatim "..."} \\ & @{text "|"} & @{text "logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \ any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "(999)"} \\ @@ -506,17 +507,17 @@ & @{text "|"} & @{verbatim CONST} @{text "id | "}@{verbatim CONST} @{text "longid"} \\ & @{text "|"} & @{verbatim TYPE} @{verbatim "("} @{text type} @{verbatim ")"} \\\\ - @{text idt} & = & @{verbatim "("} @{text idt} @{verbatim ")"}@{text " | id | "}@{verbatim "_"} \\ + @{syntax_def (inner) idt} & = & @{verbatim "("} @{text idt} @{verbatim ")"}@{text " | id | "}@{verbatim "_"} \\ & @{text "|"} & @{text id} @{verbatim "::"} @{text type} & @{text "(0)"} \\ & @{text "|"} & @{verbatim "_"} @{verbatim "::"} @{text type} & @{text "(0)"} \\\\ - @{text idts} & = & @{text "idt | idt\<^sup>(\<^sup>1\<^sup>) idts"} & @{text "(0)"} \\\\ + @{syntax_def (inner) idts} & = & @{text "idt | idt\<^sup>(\<^sup>1\<^sup>) idts"} & @{text "(0)"} \\\\ - @{text pttrn} & = & @{text idt} \\\\ + @{syntax_def (inner) pttrn} & = & @{text idt} \\\\ - @{text pttrns} & = & @{text "pttrn | pttrn\<^sup>(\<^sup>1\<^sup>) pttrns"} & @{text "(0)"} \\\\ + @{syntax_def (inner) pttrns} & = & @{text "pttrn | pttrn\<^sup>(\<^sup>1\<^sup>) pttrns"} & @{text "(0)"} \\\\ - @{text type} & = & @{verbatim "("} @{text type} @{verbatim ")"} \\ + @{syntax_def (inner) type} & = & @{verbatim "("} @{text type} @{verbatim ")"} \\ & @{text "|"} & @{text "tid | tvar | "}@{verbatim "_"} \\ & @{text "|"} & @{text "tid"} @{verbatim "::"} @{text "sort | tvar "}@{verbatim "::"} @{text "sort | "}@{verbatim "_"} @{verbatim "::"} @{text "sort"} \\ & @{text "|"} & @{text "id | type\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) id | "}@{verbatim "("} @{text type} @{verbatim ","} @{text "\"} @{verbatim ","} @{text type} @{verbatim ")"} @{text id} \\ @@ -526,7 +527,7 @@ & @{text "|"} & @{verbatim "["} @{text type} @{verbatim ","} @{text "\"} @{verbatim ","} @{text type} @{verbatim "]"} @{verbatim "=>"} @{text type} & @{text "(0)"} \\ & @{text "|"} & @{verbatim "["} @{text type} @{verbatim ","} @{text "\"} @{verbatim ","} @{text type} @{verbatim "]"} @{text "\"} @{text type} & @{text "(0)"} \\\\ - @{text sort} & = & @{text "id | longid | "}@{verbatim "{}"}@{text " | "}@{verbatim "{"} @{text "(id | longid)"} @{verbatim ","} @{text "\"} @{verbatim ","} @{text "(id | longid)"} @{verbatim "}"} \\ + @{syntax_def (inner) sort} & = & @{text "id | longid | "}@{verbatim "{}"}@{text " | "}@{verbatim "{"} @{text "(id | longid)"} @{verbatim ","} @{text "\"} @{verbatim ","} @{text "(id | longid)"} @{verbatim "}"} \\ \end{supertabular} \end{center} @@ -537,49 +538,50 @@ \begin{description} - \item @{text any} denotes any term. + \item @{syntax_ref (inner) any} denotes any term. - \item @{text prop} denotes meta-level propositions, which are terms - of type @{typ prop}. The syntax of such formulae of the meta-logic - is carefully distinguished from usual conventions for object-logics. - In particular, plain @{text "\"}-term notation is \emph{not} - recognized as @{text "prop"}. + \item @{syntax_ref (inner) prop} denotes meta-level propositions, + which are terms of type @{typ prop}. The syntax of such formulae of + the meta-logic is carefully distinguished from usual conventions for + object-logics. In particular, plain @{text "\"}-term notation is + \emph{not} recognized as @{syntax (inner) prop}. - \item @{text aprop} denotes atomic propositions, which are embedded - into regular @{typ prop} by means of an explicit @{verbatim PROP} - token. + \item @{syntax_ref (inner) aprop} denotes atomic propositions, which + are embedded into regular @{syntax (inner) prop} by means of an + explicit @{verbatim PROP} token. Terms of type @{typ prop} with non-constant head, e.g.\ a plain variable, are printed in this form. Constants that yield type @{typ prop} are expected to provide their own concrete syntax; otherwise - the printed version will appear like @{typ logic} and cannot be - parsed again as @{typ prop}. + the printed version will appear like @{syntax (inner) logic} and + cannot be parsed again as @{syntax (inner) prop}. - \item @{text logic} denotes arbitrary terms of a logical type, - excluding type @{typ prop}. This is the main syntactic category of - object-logic entities, covering plain @{text \}-term notation - (variables, abstraction, application), plus anything defined by the - user. + \item @{syntax_ref (inner) logic} denotes arbitrary terms of a + logical type, excluding type @{typ prop}. This is the main + syntactic category of object-logic entities, covering plain @{text + \}-term notation (variables, abstraction, application), plus + anything defined by the user. When specifying notation for logical entities, all logical types (excluding @{typ prop}) are \emph{collapsed} to this single category - of @{typ logic}. + of @{syntax (inner) logic}. - \item @{text idt} denotes identifiers, possibly constrained by - types. + \item @{syntax_ref (inner) idt} denotes identifiers, possibly + constrained by types. - \item @{text idts} denotes a sequence of @{text idt}. This is the - most basic category for variables in iterated binders, such as - @{text "\"} or @{text "\"}. + \item @{syntax_ref (inner) idts} denotes a sequence of @{syntax_ref + (inner) idt}. This is the most basic category for variables in + iterated binders, such as @{text "\"} or @{text "\"}. - \item @{text pttrn} and @{text pttrns} denote patterns for - abstraction, cases bindings etc. In Pure, these categories start as - a merely copy of @{text idt} and @{text idts}, respectively. - Object-logics may add additional productions for binding forms. + \item @{syntax_ref (inner) pttrn} and @{syntax_ref (inner) pttrns} + denote patterns for abstraction, cases bindings etc. In Pure, these + categories start as a merely copy of @{syntax (inner) idt} and + @{syntax (inner) idts}, respectively. Object-logics may add + additional productions for binding forms. - \item @{text type} denotes types of the meta-logic. + \item @{syntax_ref (inner) type} denotes types of the meta-logic. - \item @{text sort} denotes meta-level sorts. + \item @{syntax_ref (inner) sort} denotes meta-level sorts. \end{description} @@ -587,10 +589,10 @@ \begin{itemize} - \item In @{text idts}, note that @{text "x :: nat y"} is parsed as - @{text "x :: (nat y)"}, treating @{text y} like a type constructor - applied to @{text nat}. To avoid this interpretation, write @{text - "(x :: nat) y"} with explicit parentheses. + \item In @{syntax (inner) idts}, note that @{text "x :: nat y"} is + parsed as @{text "x :: (nat y)"}, treating @{text y} like a type + constructor applied to @{text nat}. To avoid this interpretation, + write @{text "(x :: nat) y"} with explicit parentheses. \item Similarly, @{text "x :: nat y :: nat"} is parsed as @{text "x :: (nat y :: nat)"}. The correct form is @{text "(x :: nat) (y :: diff -r 2eeeced17228 -r a25630deacaf doc-src/IsarRef/Thy/Misc.thy --- a/doc-src/IsarRef/Thy/Misc.thy Thu Nov 13 22:00:39 2008 +0100 +++ b/doc-src/IsarRef/Thy/Misc.thy Thu Nov 13 22:01:30 2008 +0100 @@ -48,11 +48,10 @@ the theory context; the ``@{text "!"}'' option indicates extra verbosity. - \item @{command "print_syntax"} prints the inner syntax of types - and terms, depending on the current context. The output can be very + \item @{command "print_syntax"} prints the inner syntax of types and + terms, depending on the current context. The output can be very verbose, including grammar tables and syntax translation rules. See - \cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's - inner syntax. + \chref{ch:inner-syntax} for further information on inner syntax. \item @{command "print_methods"} prints all proof methods available in the current theory context. diff -r 2eeeced17228 -r a25630deacaf doc-src/IsarRef/Thy/Outer_Syntax.thy --- a/doc-src/IsarRef/Thy/Outer_Syntax.thy Thu Nov 13 22:00:39 2008 +0100 +++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy Thu Nov 13 22:01:30 2008 +0100 @@ -135,31 +135,45 @@ \end{supertabular} \end{center} - The syntax of @{syntax string} admits any characters, including + A @{syntax_ref var} or @{syntax_ref typevar} describes an unknown, + which is internally a pair of base name and index (ML type @{ML_type + indexname}). These components are either separated by a dot as in + @{text "?x.1"} or @{text "?x7.3"} or run together as in @{text + "?x1"}. The latter form is possible if the base name does not end + with digits. If the index is 0, it may be dropped altogether: + @{text "?x"} and @{text "?x0"} and @{text "?x.0"} all refer to the + same unknown, with basename @{text "x"} and index 0. + + The syntax of @{syntax_ref string} admits any characters, including newlines; ``@{verbatim "\""}'' (double-quote) and ``@{verbatim "\\"}'' (backslash) need to be escaped by a backslash; arbitrary character codes may be specified as ``@{verbatim "\\"}@{text ddd}'', with three decimal digits. Alternative strings according to - @{syntax altstring} are analogous, using single back-quotes instead. - The body of @{syntax verbatim} may consist of any text not + @{syntax_ref altstring} are analogous, using single back-quotes + instead. + + The body of @{syntax_ref verbatim} may consist of any text not containing ``@{verbatim "*"}@{verbatim "}"}''; this allows - convenient inclusion of quotes without further escapes. The greek - letters do \emph{not} include @{verbatim "\"}, which is already used - differently in the meta-logic. + convenient inclusion of quotes without further escapes. There is no + way to escape ``@{verbatim "*"}@{verbatim "}"}''. If the quoted + text is {\LaTeX} source, one may usually add some blank or comment + to avoid the critical character sequence. + + Source comments take the form @{verbatim "(*"}~@{text + "\"}~@{verbatim "*)"} and may be nested, although the user-interface + might prevent this. Note that this form indicates source comments + only, which are stripped after lexical analysis of the input. The + Isar syntax also provides proper \emph{document comments} that are + considered as part of the text (see \secref{sec:comments}). Common mathematical symbols such as @{text \} are represented in Isabelle as @{verbatim \}. There are infinitely many Isabelle symbols like this, although proper presentation is left to front-end tools such as {\LaTeX} or Proof~General with the X-Symbol package. A list of standard Isabelle symbols that work well with these tools - is given in \cite[appendix~A]{isabelle-sys}. - - Source comments take the form @{verbatim "(*"}~@{text - "\"}~@{verbatim "*)"} and may be nested, although the user-interface - might prevent this. Note that this form indicates source comments - only, which are stripped after lexical analysis of the input. The - Isar syntax also provides proper \emph{document comments} that are - considered as part of the text (see \secref{sec:comments}). + is given in \cite[appendix~A]{isabelle-sys}. Note that @{verbatim + "\"} does not belong to the @{text letter} category, since it is + already used differently in the Pure term language. *}