Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/jEdit/patches/line_separator
author desharna
Mon, 17 Mar 2025 11:30:39 +0100
changeset 82298 c65013be534b
parent 82015 fe186fd7a168
permissions -rw-r--r--
added lemmas wf_on_bot[simp] and wfp_on_bot[simp]
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
82015
fe186fd7a168 make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;
wenzelm
parents:
diff changeset 
     1
 
diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/bufferio/BufferIORequest.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/bufferio/BufferIORequest.java
fe186fd7a168 make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;
wenzelm
parents:
diff changeset 
     2
 
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/bufferio/BufferIORequest.java	2024-08-03 19:53:19.000000000 +0200
fe186fd7a168 make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;
wenzelm
parents:
diff changeset 
     3
 
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/bufferio/BufferIORequest.java	2025-01-29 20:03:36.236518733 +0100
fe186fd7a168 make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;
wenzelm
parents:
diff changeset 
     4
 
@@ -357,7 +357,7 @@
fe186fd7a168 make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;
wenzelm
parents:
diff changeset 
     5
fe186fd7a168 make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;
wenzelm
parents:
diff changeset 
     6
 
 		Segment lineSegment = new Segment();
fe186fd7a168 make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;
wenzelm
parents:
diff changeset 
     7
 
 		String newline = buffer.getStringProperty(JEditBuffer.LINESEP);
fe186fd7a168 make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;
wenzelm
parents:
diff changeset 
     8
 
-		if(newline == null)
fe186fd7a168 make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;
wenzelm
parents:
diff changeset 
     9
 
+		if(newline == null || newline.isEmpty())
fe186fd7a168 make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;
wenzelm
parents:
diff changeset 
    10
 
 			newline = System.getProperty("line.separator");
fe186fd7a168 make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;
wenzelm
parents:
diff changeset 
    11
fe186fd7a168 make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;
wenzelm
parents:
diff changeset 
    12
 
 		final int bufferLineCount = buffer.getLineCount();
fe186fd7a168 make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;
wenzelm
parents:
diff changeset 
    13
 
diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/Buffer.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/Buffer.java
fe186fd7a168 make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;
wenzelm
parents:
diff changeset 
    14
 
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/Buffer.java	2024-08-03 19:53:15.000000000 +0200
fe186fd7a168 make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;
wenzelm
parents:
diff changeset 
    15
 
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/Buffer.java	2025-01-29 20:00:53.025217244 +0100
fe186fd7a168 make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;
wenzelm
parents:
diff changeset 
    16
 
@@ -1236,6 +1236,7 @@
fe186fd7a168 make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;
wenzelm
parents:
diff changeset 
    17
 
 	 */
fe186fd7a168 make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;
wenzelm
parents:
diff changeset 
    18
 
 	public void setLineSeparator(String lineSep)
fe186fd7a168 make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;
wenzelm
parents:
diff changeset 
    19
 
 	{
fe186fd7a168 make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;
wenzelm
parents:
diff changeset 
    20
 
+		lineSep = org.jedit.misc.LineSepType.fromSeparator(lineSep).getSeparator();
fe186fd7a168 make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;
wenzelm
parents:
diff changeset 
    21
 
 		setProperty(LINESEP, lineSep);
fe186fd7a168 make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;
wenzelm
parents:
diff changeset 
    22
 
 		setDirty(true);
fe186fd7a168 make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;
wenzelm
parents:
diff changeset 
    23
 
 		propertiesChanged();
isabelle