| products/Sources/formale Sprachen/Isabelle/Tools/jEdit/dist/doc/tips/tip29.html |
 |
<html><body>jEdit supports "folding"; a "fold" is a section of a
buffer that can be hidden and shown by clicking in the gutter or
using the commands in the <b>Folding</b> menu.
Folds can be nested.<p>
Two folding modes are supported; "indent" and "explicit". In the
former, folds are created based on the leading indent of a line;
in the latter, the buffer is parsed for the strings
<code>{{{</code> and <code>}}}</code>.<p>
Folding can be enabled in the <b>Buffer Options</b> and
<b>Global Options</b> dialog boxes.
</body></html>
¤ Dauer der Verarbeitung: 0.15 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.
|
