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.