Quelle gutter

Sprache: SML

diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/Gutter.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/Gutter.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/Gutter.java 2024-08-03 19:53:18.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/Gutter.java 2025-04-22 22:08:05.106604316 +0200
@@ -682,7 +682,7 @@
  //{{{ Private members

  //{{{ Instance variables
- private static final int FOLD_MARKER_SIZE = 12;
+ public static final int FOLD_MARKER_SIZE = 12;
  private static final int SELECTION_GUTTER_WIDTH = 12;
   // The selection gutter exists only if the gutter is not expanded

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.1 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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 und die Messung sind noch experimentell.