Add an option to toggle document scrolling behavior

packages/codemirror-extension/schema/commands.json

@@ -5,7 +5,13 @@
   "description": "Text editor settings for all CodeMirror editors.",
   "properties": {
     "keyMap": { "type": "string", "title": "Key Map", "default": "default" },
-    "theme": { "type": "string", "title": "Theme", "default": "default" }
+    "theme": { "type": "string", "title": "Theme", "default": "default" },
+    "scrollPastEnd": {
+      "type": "boolean",
+      "title": "Scroll behavior",
+      "description": "Whether to scroll past the end of text document",
+      "default": true
+    }
   },
   "type": "object"
 }

packages/codemirror-extension/src/index.ts

@@ -134,7 +134,7 @@ function activateEditorCommands(
   settingRegistry: ISettingRegistry
 ): void {
   const { commands, restored } = app;
-  let { theme, keyMap } = CodeMirrorEditor.defaultConfig;
+  let { theme, keyMap, scrollPastEnd } = CodeMirrorEditor.defaultConfig;
 
   /**
    * Update the setting values.
@@ -142,6 +142,7 @@ function activateEditorCommands(
   function updateSettings(settings: ISettingRegistry.ISettings): void {
     keyMap = (settings.get('keyMap').composite as string | null) || keyMap;
     theme = (settings.get('theme').composite as string | null) || theme;
+    scrollPastEnd = settings.get('scrollPastEnd').composite as boolean | null;
   }
 
   /**
@@ -153,6 +154,7 @@ function activateEditorCommands(
         let cm = widget.content.editor.editor;
         cm.setOption('keyMap', keyMap);
         cm.setOption('theme', theme);
+        cm.setOption('scrollPastEnd', scrollPastEnd);
       }
     });
   }
@@ -180,6 +182,7 @@ function activateEditorCommands(
       let cm = widget.content.editor.editor;
       cm.setOption('keyMap', keyMap);
       cm.setOption('theme', theme);
+      cm.setOption('scrollPastEnd', scrollPastEnd);
     }
   });