Merge branch 'java15' into java17

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) {

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();
+        }
+    }
+}

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;
+        }
+    }
+}

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));
 	}

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();
+			}
 		}
 	};