118 ; |
118 ; |
119 localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+)) |
119 localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+)) |
120 ; |
120 ; |
121 |
121 |
122 contextexpr: nameref | '(' contextexpr ')' | |
122 contextexpr: nameref | '(' contextexpr ')' | |
123 (contextexpr (name+)) | (contextexpr + '+') |
123 (contextexpr (name mixfix? +)) | (contextexpr + '+') |
124 ; |
124 ; |
125 contextelem: fixes | assumes | defines | notes | includes |
125 contextelem: fixes | assumes | defines | notes | includes |
126 ; |
126 ; |
127 fixes: 'fixes' (name ('::' type)? structmixfix? + 'and') |
127 fixes: 'fixes' (name ('::' type)? structmixfix? + 'and') |
128 ; |
128 ; |
146 expressions automatically takes care of the most general typing that the |
146 expressions automatically takes care of the most general typing that the |
147 combined context elements may acquire. |
147 combined context elements may acquire. |
148 |
148 |
149 The $import$ consists of a structured context expression, consisting of |
149 The $import$ consists of a structured context expression, consisting of |
150 references to existing locales, renamed contexts, or merged contexts. |
150 references to existing locales, renamed contexts, or merged contexts. |
151 Renaming uses positional notation: $c~\vec x$ means that (a prefix) the |
151 Renaming uses positional notation: $c~\vec x$ means that (a prefix of) the |
152 fixed parameters of context $c$ are named according to $\vec x$; a |
152 fixed parameters of context $c$ are named according to $\vec x$; a |
153 ``\texttt{_}'' (underscore).\indexisarthm{_@\texttt{_}} means to skip that |
153 ``\texttt{_}'' (underscore) \indexisarthm{_@\texttt{_}} means to skip that |
154 position. Also note that concrete syntax only works with the original name. |
154 position. Renaming by default deletes existing syntax. Optionally, |
|
155 new syntax may by specified with a mixfix annotation. Note that the |
|
156 special syntax declared with ``$(structure)$'' (see below) is |
|
157 neither deleted nor can it be changed. |
155 Merging proceeds from left-to-right, suppressing any duplicates stemming |
158 Merging proceeds from left-to-right, suppressing any duplicates stemming |
156 from different paths through the import hierarchy. |
159 from different paths through the import hierarchy. |
157 |
160 |
158 The $body$ consists of basic context elements, further context expressions |
161 The $body$ consists of basic context elements, further context expressions |
159 may be included as well. |
162 may be included as well. |