diff --git a/init.js b/init.js index 97ef572..f85e78e 100644 --- a/init.js +++ b/init.js @@ -409,7 +409,7 @@ function classpath() { return java.lang.System.getProperty("java.class.path"); } -// require org.scala-lang#scala3-compiler_3;3.1.3 +// require org.scala-lang#scala3-compiler_3;3.3.1 function dotc(srcDir, destDir, options) { if (srcDir == undefined) { diff --git a/mail/src/linoleum/mail/EditorPane.java b/mail/src/linoleum/mail/EditorPane.java new file mode 100644 index 0000000..da273c1 --- /dev/null +++ b/mail/src/linoleum/mail/EditorPane.java @@ -0,0 +1,90 @@ +package linoleum.mail; + +import java.io.IOException; +import java.io.InputStream; +import java.io.InputStreamReader; +import java.io.BufferedInputStream; +import java.io.Reader; +import java.net.URL; +import java.net.URLConnection; +import javax.swing.JEditorPane; +import javax.swing.text.Document; +import javax.swing.text.BadLocationException; +import javax.swing.text.ChangedCharSetException; + +class EditorPane extends JEditorPane { + void read(InputStream in, Document doc) throws IOException { + if (! Boolean.TRUE.equals(doc.getProperty("IgnoreCharsetDirective"))) { + final int READ_LIMIT = 1024 * 10; + in = new BufferedInputStream(in, READ_LIMIT); + in.mark(READ_LIMIT); + } + String charset = (String) getClientProperty("charset"); + try(Reader r = (charset != null) ? new InputStreamReader(in, charset) : + new InputStreamReader(in)) { + try { + getEditorKit().read(r, doc, 0); + } catch (BadLocationException e) { + throw new IOException(e.getMessage()); + } catch (ChangedCharSetException changedCharSetException) { + String charSetSpec = changedCharSetException.getCharSetSpec(); + if (changedCharSetException.keyEqualsCharSet()) { + putClientProperty("charset", charSetSpec); + } else { + setCharsetFromContentTypeParameters(charSetSpec); + } + try { + in.reset(); + } catch (IOException exception) { + //mark was invalidated + in.close(); + URL url = (URL)doc.getProperty(Document.StreamDescriptionProperty); + if (url != null) { + URLConnection conn = url.openConnection(); + in = conn.getInputStream(); + } else { + //there is nothing we can do to recover stream + throw changedCharSetException; + } + } + try { + doc.remove(0, doc.getLength()); + } catch (BadLocationException e) {} + doc.putProperty("IgnoreCharsetDirective", Boolean.valueOf(true)); + read(in, doc); + } + } + } + + private void setCharsetFromContentTypeParameters(String paramlist) { + String charset; + try { + // paramlist is handed to us with a leading ';', strip it. + int semi = paramlist.indexOf(';'); + if (semi > -1 && semi < paramlist.length()-1) { + paramlist = paramlist.substring(semi + 1); + } + + if (paramlist.length() > 0) { + // parse the paramlist into attr-value pairs & get the + // charset pair's value + HeaderParser hdrParser = new HeaderParser(paramlist); + charset = hdrParser.findValue("charset"); + if (charset != null) { + putClientProperty("charset", charset); + } + } + } + catch (IndexOutOfBoundsException e) { + // malformed parameter list, use charset we have + } + catch (NullPointerException e) { + // malformed parameter list, use charset we have + } + catch (Exception e) { + // malformed parameter list, use charset we have; but complain + System.err.println("JEditorPane.getCharsetFromContentTypeParameters failed on: " + paramlist); + e.printStackTrace(); + } + } +} diff --git a/mail/src/linoleum/mail/HeaderParser.java b/mail/src/linoleum/mail/HeaderParser.java new file mode 100644 index 0000000..ddb6841 --- /dev/null +++ b/mail/src/linoleum/mail/HeaderParser.java @@ -0,0 +1,126 @@ +package linoleum.mail; + +class HeaderParser { + + /* table of key/val pairs - maxes out at 10!!!!*/ + String raw; + String[][] tab; + + public HeaderParser(String raw) { + this.raw = raw; + tab = new String[10][2]; + parse(); + } + + private void parse() { + + if (raw != null) { + raw = raw.trim(); + char[] ca = raw.toCharArray(); + int beg = 0, end = 0, i = 0; + boolean inKey = true; + boolean inQuote = false; + int len = ca.length; + while (end < len) { + char c = ca[end]; + if (c == '=') { // end of a key + tab[i][0] = new String(ca, beg, end-beg).toLowerCase(); + inKey = false; + end++; + beg = end; + } else if (c == '\"') { + if (inQuote) { + tab[i++][1]= new String(ca, beg, end-beg); + inQuote=false; + do { + end++; + } while (end < len && (ca[end] == ' ' || ca[end] == ',')); + inKey=true; + beg=end; + } else { + inQuote=true; + end++; + beg=end; + } + } else if (c == ' ' || c == ',') { // end key/val, of whatever we're in + if (inQuote) { + end++; + continue; + } else if (inKey) { + tab[i++][0] = (new String(ca, beg, end-beg)).toLowerCase(); + } else { + tab[i++][1] = (new String(ca, beg, end-beg)); + } + while (end < len && (ca[end] == ' ' || ca[end] == ',')) { + end++; + } + inKey = true; + beg = end; + } else { + end++; + } + } + // get last key/val, if any + if (--end > beg) { + if (!inKey) { + if (ca[end] == '\"') { + tab[i++][1] = (new String(ca, beg, end-beg)); + } else { + tab[i++][1] = (new String(ca, beg, end-beg+1)); + } + } else { + tab[i][0] = (new String(ca, beg, end-beg+1)).toLowerCase(); + } + } else if (end == beg) { + if (!inKey) { + if (ca[end] == '\"') { + tab[i++][1] = String.valueOf(ca[end-1]); + } else { + tab[i++][1] = String.valueOf(ca[end]); + } + } else { + tab[i][0] = String.valueOf(ca[end]).toLowerCase(); + } + } + } + + } + + public String findKey(int i) { + if (i < 0 || i > 10) + return null; + return tab[i][0]; + } + + public String findValue(int i) { + if (i < 0 || i > 10) + return null; + return tab[i][1]; + } + + public String findValue(String key) { + return findValue(key, null); + } + + public String findValue(String k, String Default) { + if (k == null) + return Default; + k = k.toLowerCase(); + for (int i = 0; i < 10; ++i) { + if (tab[i][0] == null) { + return Default; + } else if (k.equals(tab[i][0])) { + return tab[i][1]; + } + } + return Default; + } + + public int findInt(String k, int Default) { + try { + return Integer.parseInt(findValue(k, String.valueOf(Default))); + } catch (Throwable t) { + return Default; + } + } +} diff --git a/mail/src/linoleum/mail/TextViewer.java b/mail/src/linoleum/mail/TextViewer.java index 28b2c01..3306134 100644 --- a/mail/src/linoleum/mail/TextViewer.java +++ b/mail/src/linoleum/mail/TextViewer.java @@ -3,21 +3,20 @@ import java.awt.*; import java.io.*; import javax.activation.*; -import javax.swing.JEditorPane; import javax.swing.JPopupMenu; import javax.swing.JScrollPane; import javax.swing.text.Document; import javax.swing.text.EditorKit; public class TextViewer extends AbstractViewer { - private final JEditorPane text_area; + private final EditorPane text_area; private final JPopupMenu menu = new JPopupMenu(); public TextViewer() { super(new GridLayout(1,1)); // create the text area - text_area = new JEditorPane(); + text_area = new EditorPane(); text_area.setEditable(false); // create a scroll pane for the JTextArea @@ -39,6 +38,7 @@ public void setCommandContext(final String verb, final DataHandler dh) throws IO text_area.setContentType(type.toLowerCase()); final EditorKit kit = text_area.getEditorKit(); final Document doc = kit.createDefaultDocument(); + text_area.setDocument(doc); text_area.read(ins, doc); menu.add(new SaveAsAction(dh, null)); } diff --git a/notepad/src/linoleum/notepad/Frame.java b/notepad/src/linoleum/notepad/Frame.java index 2dc7bb3..e34c8f3 100644 --- a/notepad/src/linoleum/notepad/Frame.java +++ b/notepad/src/linoleum/notepad/Frame.java @@ -56,6 +56,7 @@ import javax.swing.undo.CannotRedoException; import javax.swing.undo.CannotUndoException; import javax.swing.undo.UndoManager; +import javax.swing.undo.UndoableEdit; import linoleum.application.FileChooser; import linoleum.application.FileSupport; @@ -284,10 +285,13 @@ private String[] getItemKeys(final String key) { private UndoableEditListener undoHandler = new UndoableEditListener() { public void undoableEditHappened(final UndoableEditEvent e) { - undo.addEdit(e.getEdit()); - if (modified >= 0) modified += 1; - undoAction.update(); - redoAction.update(); + final UndoableEdit edit = e.getEdit(); + if (edit.isSignificant()) { + undo.addEdit(edit); + if (modified >= 0) modified += 1; + undoAction.update(); + redoAction.update(); + } } };