equal
deleted
inserted
replaced
315 Segment data = new Segment(); |
315 Segment data = new Segment(); |
316 int nleft = len; |
316 int nleft = len; |
317 int offs = pos; |
317 int offs = pos; |
318 Object endOfLineProperty = doc.getProperty(EndOfLineStringProperty); |
318 Object endOfLineProperty = doc.getProperty(EndOfLineStringProperty); |
319 if (endOfLineProperty == null) { |
319 if (endOfLineProperty == null) { |
320 try { |
320 endOfLineProperty = System.lineSeparator(); |
321 endOfLineProperty = System.getProperty("line.separator"); |
|
322 } catch (SecurityException se) { } |
|
323 } |
321 } |
324 String endOfLine; |
322 String endOfLine; |
325 if (endOfLineProperty instanceof String) { |
323 if (endOfLineProperty instanceof String) { |
326 endOfLine = (String)endOfLineProperty; |
324 endOfLine = (String)endOfLineProperty; |
327 } |
325 } |