equal
deleted
inserted
replaced
54 } |
54 } |
55 } |
55 } |
56 |
56 |
57 class Document_Model(val session: Session, val buffer: Buffer) |
57 class Document_Model(val session: Session, val buffer: Buffer) |
58 { |
58 { |
|
59 /* visible line end */ |
|
60 |
|
61 // simplify slightly odd result of TextArea.getLineEndOffset |
|
62 // NB: jEdit already normalizes \r\n and \r to \n |
|
63 def visible_line_end(start: Int, end: Int): Int = |
|
64 { |
|
65 val end1 = end - 1 |
|
66 if (start <= end1 && end1 < buffer.getLength && |
|
67 buffer.getSegment(end1, 1).charAt(0) == '\n') end1 |
|
68 else end |
|
69 } |
|
70 |
|
71 |
59 /* history */ |
72 /* history */ |
60 |
73 |
61 private val document_0 = session.begin_document(buffer.getName) |
74 private val document_0 = session.begin_document(buffer.getName) |
62 |
75 |
63 @volatile private var history = // owned by Swing thread |
76 @volatile private var history = // owned by Swing thread |