X-Git-Url: http://git.nikiroo.be/?p=nikiroo-utils.git;a=blobdiff_plain;f=teditor%2FDocument.java;h=b4a9a3bfb6b3ab476d29b45b3a01b4fbdca77816;hp=2abfef6635f3c1877fc733ee36ea8c67d01160b6;hb=e6bb1700749980e69b5e913acbfd276f129c24dc;hpb=cf01c92f5809a0732409e280fb0f32f27393618d diff --git a/teditor/Document.java b/teditor/Document.java index 2abfef6..b4a9a3b 100644 --- a/teditor/Document.java +++ b/teditor/Document.java @@ -76,6 +76,23 @@ public class Document { */ private Highlighter highlighter = new Highlighter(); + /** + * The tab stop size. + */ + private int tabSize = 8; + + /** + * If true, backspace at an indent level goes back a full indent level. + * If false, backspace always goes back one column. + */ + private boolean backspaceUnindents = false; + + /** + * If true, save files with tab characters. If false, convert tabs to + * spaces when saving files. + */ + private boolean saveWithTabs = false; + // ------------------------------------------------------------------------ // Constructors ----------------------------------------------------------- // ------------------------------------------------------------------------ @@ -89,7 +106,8 @@ public class Document { public Document(final String str, final CellAttributes defaultColor) { this.defaultColor = defaultColor; - // TODO: set different colors based on file extension + // Set colors to resemble the Borland IDE colors, but for Java + // language keywords. highlighter.setJavaColors(); String [] rawLines = str.split("\n"); @@ -98,16 +116,41 @@ public class Document { } } + /** + * Private constructor used by dup(). + */ + private Document() { + // NOP + } + // ------------------------------------------------------------------------ // Document --------------------------------------------------------------- // ------------------------------------------------------------------------ + /** + * Create a duplicate instance. + * + * @return duplicate intance + */ + public Document dup() { + Document other = new Document(); + for (Line line: lines) { + other.lines.add(line.dup()); + } + other.lineNumber = lineNumber; + other.overwrite = overwrite; + other.dirty = dirty; + other.defaultColor = defaultColor; + other.highlighter.setTo(highlighter); + return other; + } + /** * Get the overwrite flag. * * @return true if addChar() overwrites data, false if it inserts */ - public boolean getOverwrite() { + public boolean isOverwrite() { return overwrite; } @@ -120,6 +163,13 @@ public class Document { return dirty; } + /** + * Unset the dirty flag. + */ + public void setNotDirty() { + dirty = false; + } + /** * Save contents to file. * @@ -133,7 +183,11 @@ public class Document { "UTF-8"); for (Line line: lines) { - output.write(line.getRawString()); + if (saveWithTabs) { + output.write(convertSpacesToTabs(line.getRawString())); + } else { + output.write(line.getRawString()); + } output.write("\n"); } @@ -362,7 +416,7 @@ public class Document { // If at the beginning of a word already, push past it. if ((getChar() != -1) && (getRawLine().length() > 0) - && !Character.isSpace((char) getChar()) + && !Character.isWhitespace((char) getChar()) ) { left(); } @@ -370,7 +424,7 @@ public class Document { // int line = lineNumber; while ((getChar() == -1) || (getRawLine().length() == 0) - || Character.isSpace((char) getChar()) + || Character.isWhitespace((char) getChar()) ) { if (left() == false) { return; @@ -380,12 +434,12 @@ public class Document { assert (getChar() != -1); - if (!Character.isSpace((char) getChar()) + if (!Character.isWhitespace((char) getChar()) && (getRawLine().length() > 0) ) { // Advance until at the beginning of the document or a whitespace // is encountered. - while (!Character.isSpace((char) getChar())) { + while (!Character.isWhitespace((char) getChar())) { int line = lineNumber; if (left() == false) { // End of document, bail out. @@ -418,7 +472,7 @@ public class Document { } if (lineNumber != line) { // We wrapped a line. Here that counts as whitespace. - if (!Character.isSpace((char) getChar())) { + if (!Character.isWhitespace((char) getChar())) { // We found a character immediately after the line. // Done! return; @@ -429,12 +483,12 @@ public class Document { } assert (getChar() != -1); - if (!Character.isSpace((char) getChar()) + if (!Character.isWhitespace((char) getChar()) && (getRawLine().length() > 0) ) { // Advance until at the end of the document or a whitespace is // encountered. - while (!Character.isSpace((char) getChar())) { + while (!Character.isWhitespace((char) getChar())) { line = lineNumber; if (right() == false) { // End of document, bail out. @@ -442,7 +496,7 @@ public class Document { } if (lineNumber != line) { // We wrapped a line. Here that counts as whitespace. - if (!Character.isSpace((char) getChar()) + if (!Character.isWhitespace((char) getChar()) && (getRawLine().length() > 0) ) { // We found a character immediately after the line. @@ -462,7 +516,7 @@ public class Document { } if (lineNumber != line) { // We wrapped a line. Here that counts as whitespace. - if (!Character.isSpace((char) getChar())) { + if (!Character.isWhitespace((char) getChar())) { // We found a character immediately after the line. // Done! return; @@ -473,10 +527,10 @@ public class Document { } assert (getChar() != -1); - if (Character.isSpace((char) getChar())) { + if (Character.isWhitespace((char) getChar())) { // Advance until at the end of the document or a non-whitespace // is encountered. - while (Character.isSpace((char) getChar())) { + while (Character.isWhitespace((char) getChar())) { if (right() == false) { // End of document, bail out. return; @@ -543,7 +597,7 @@ public class Document { dirty = true; int cursor = lines.get(lineNumber).getCursor(); if (cursor > 0) { - lines.get(lineNumber).backspace(); + lines.get(lineNumber).backspace(tabSize, backspaceUnindents); } else if (lineNumber > 0) { // Join two lines lineNumber--; @@ -595,6 +649,62 @@ public class Document { } } + /** + * Get the tab stop size. + * + * @return the tab stop size + */ + public int getTabSize() { + return tabSize; + } + + /** + * Set the tab stop size. + * + * @param tabSize the new tab stop size + */ + public void setTabSize(final int tabSize) { + this.tabSize = tabSize; + } + + /** + * Set the backspace unindent option. + * + * @param backspaceUnindents If true, backspace at an indent level goes + * back a full indent level. If false, backspace always goes back one + * column. + */ + public void setBackspaceUnindents(final boolean backspaceUnindents) { + this.backspaceUnindents = backspaceUnindents; + } + + /** + * Set the save with tabs option. + * + * @param saveWithTabs If true, save files with tab characters. If + * false, convert tabs to spaces when saving files. + */ + public void setSaveWithTabs(final boolean saveWithTabs) { + this.saveWithTabs = saveWithTabs; + } + + /** + * Handle the tab character. + */ + public void tab() { + if (overwrite) { + del(); + } + lines.get(lineNumber).tab(tabSize); + } + + /** + * Handle the backtab (shift-tab) character. + */ + public void backTab() { + lines.get(lineNumber).backTab(tabSize); + } + /** * Get a (shallow) copy of the list of lines. * @@ -637,4 +747,77 @@ public class Document { return lines.get(lineNumber).getDisplayLength(); } + /** + * Get the entire contents of the document as one string. + * + * @return the document contents + */ + public String getText() { + StringBuilder sb = new StringBuilder(); + for (Line line: getLines()) { + sb.append(line.getRawString()); + sb.append("\n"); + } + return sb.toString(); + } + + /** + * Trim trailing whitespace from lines and trailing empty + * lines from the document. + */ + public void cleanWhitespace() { + for (Line line: getLines()) { + line.trimRight(); + } + if (lines.size() == 0) { + return; + } + while (lines.get(lines.size() - 1).length() == 0) { + lines.remove(lines.size() - 1); + } + if (lineNumber > lines.size() - 1) { + lineNumber = lines.size() - 1; + } + } + + /** + * Set keyword highlighting. + * + * @param enabled if true, enable keyword highlighting + */ + public void setHighlighting(final boolean enabled) { + highlighter.setEnabled(enabled); + for (Line line: getLines()) { + line.scanLine(); + } + } + + /** + * Convert a string with leading spaces to a mix of tabs and spaces. + * + * @param string the string to convert + */ + private String convertSpacesToTabs(final String string) { + if (string.length() == 0) { + return string; + } + + int start = 0; + while (string.charAt(start) == ' ') { + start++; + } + int tabCount = start / 8; + if (tabCount == 0) { + return string; + } + + StringBuilder sb = new StringBuilder(string.length()); + + for (int i = 0; i < tabCount; i++) { + sb.append('\t'); + } + sb.append(string.substring(tabCount * 8)); + return sb.toString(); + } + }