Method propertyChange

app/src/processing/app/ui/WebFrame.java:60–65

(PropertyChangeEvent evt)

    // Title cannot be set until the page has loaded
    editorPane.addPropertyChangeListener("page", new PropertyChangeListener() {
      public void propertyChange(PropertyChangeEvent evt) {
        Object title = editorPane.getDocument().getProperty("title");
        if (title instanceof String) {
          setTitle((String) title);
        }
      }
    });

    editorPane.setPage(fileUrl);