Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: tip75.html Sprache: HTML

Original von: Isabelle^©

products/sources/formale sprachen/Isabelle/Tools/jEdit/dist/doc/tips/tip75.html

<html><body>
If quick copy is enabled in
the Mouse pane of the Utilities>Global
Options dialog box, dragging with the middle mouse button over some text
inserts that text at the previous caret position.

This feature has some additional behavior you might not expect:

<ul>
<li>It can be used to transfer text between edit panes in a split view.
<li>Holding down Shift while clicking the middle mouse button immediately duplicates all text between the caret position and the clicked location.
<li>If there already is a selection when you start middle-dragging, the selection
will be replaced with the region you marked with the mouse.</li>
<li>Holding down Control while dragging the middle mouse button marks a
rectangular area, and pastes it vertically at the caret location (or into the
current selection).</li>
</ul>

</body></html>

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.