Make the source setter not reset the editor state.

It now only changes the source code in the editor, but maintains
undo/redo history.

A new `setSource` method is added that will reset the editor state
entirely (as the source setter did before).

README.md

@@ -68,8 +68,14 @@ The options are described below.
 
 ### `source: string`
 
-Set the source code to be edited with the `source` getter, and get the current source with the `source` setter. Note
-that setting the source will reset the editor state (including undo and redo history).
+Get the source code to be edited with the `source` getter, and set the current source with the `source` setter. Note
+that setting the source will only update the code shown with the new contents, and the editor state will be maintained
+(including undo and redo history). If the intent is to reset the state with a new document use the `newSource` method
+instead.
+
+### `newSource(doc: string): void`
+
+Set the source code to be edited in the editor. This resets the editor state, and loads the new code.
 
 ### `setLanguage(languageName: string): Promise<void>`
 

package.json

@@ -1,6 +1,6 @@
 {
     "name": "@openwebwork/pg-codemirror-editor",
-    "version": "0.0.1-beta.9",
+    "version": "0.0.1-beta.10",
     "description": "PG CodeMirror Editor",
     "author": "The WeBWorK Project",
     "license": "MIT",

public/editor.js

@@ -17,7 +17,7 @@ if (codeMirrorElt instanceof HTMLElement) {
             reader.readAsText(file);
             reader.addEventListener('load', () => {
                 sourceInput.value = reader.result;
-                pgEditor.source = sourceInput.value;
+                pgEditor.newSource(sourceInput.value);
             });
         }
     });

src/pg-codemirror-editor.ts

@@ -330,16 +330,20 @@ export class View {
     }
 
     set source(doc: string) {
-        this.view.setState(EditorState.create({ doc, extensions: this.extensions }));
-        void this.setLanguage(this.currentLanguage);
-        void this.setTheme(this.currentTheme);
-        void this.setKeyMap(this.currentKeyMap);
+        this.view.dispatch({ changes: { from: 0, to: this.view.state.doc.length, insert: doc } });
     }
 
     get source() {
         return this.view.state.doc.toString();
     }
 
+    newSource(doc: string) {
+        this.view.setState(EditorState.create({ doc, extensions: this.extensions }));
+        void this.setLanguage(this.currentLanguage);
+        void this.setTheme(this.currentTheme);
+        void this.setKeyMap(this.currentKeyMap);
+    }
+
     async setLanguage(languageName: string) {
         const language = this.languages.get(languageName);
         if (language) {