| products/Sources/formale Sprachen/Isabelle/Tools/jEdit/dist/jEdit/doc/tips/tip0.html |
 |
<html><body>Using abbreviations saves a lot of time, by letting you
enter long strings using a shorthand notation. To define an
abbreviation, enter the desired shorthand string and press <b>C+;</b>.
You will then be prompted for the expansion. Now, to enter the expansion
in the buffer, all you have to do is type the shorthand and press
<b>C+;</b> again.</body></html>
¤ Dauer der Verarbeitung: 0.5 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
