# Re: [isabelle] syntax for lifted / point-free operations

On Tue, 17 Nov 2015, Peter Gammie wrote:


One limitation is that \<^bold> does not work so well for multi-character tokens, such as:


\<^bold> is a control symbol, it operates on the subsequent symbol. Tokens are not involved here.


Multi-symbol control symbols are managed by Isabelle/jEdit: selecting a block and applying certain actions adds or removes control symbols for
each symbol in the text.

Quotation from the "jedit" manual:

\paragraph{Control symbols.} There are some special control symbols
to modify the display style of a single symbol (without
nesting). Control symbols may be applied to a region of selected
text, either using the \emph{Symbols} panel or keyboard shortcuts or
jEdit actions.  These editor operations produce a separate control
symbol for each symbol in the text, in order to make the whole text
appear in a certain style.

The manual tells more about these actions and default keyboard shortcuts.

Makarius



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.