Work around for undefined user event type. Fixes #69.

This commit is contained in:
bakuzan 2023-01-30 11:12:39 +00:00
parent 566f8531b5
commit 44dfcb9fe3

View file

@ -1,3 +1,4 @@
import { Transaction } from "@codemirror/state";
import { import {
ViewUpdate, ViewUpdate,
PluginValue, PluginValue,
@ -22,9 +23,19 @@ class EditorPlugin implements PluginValue {
} }
const tr = update.transactions[0]; const tr = update.transactions[0];
if (!tr) return;
if (!tr) {
return;
}
// When selecting text with Shift+Home the userEventType is undefined.
// This is probably a bug in codemirror, for the time being doing an explict check
// for the type allows us to update the stats for the selection.
const userEventTypeUndefined =
tr.annotation(Transaction.userEvent) === undefined;
if ( if (
tr.isUserEvent("select") && (tr.isUserEvent("select") || userEventTypeUndefined) &&
tr.newSelection.ranges[0].from !== tr.newSelection.ranges[0].to tr.newSelection.ranges[0].from !== tr.newSelection.ranges[0].to
) { ) {
let text = ""; let text = "";
@ -42,6 +53,7 @@ class EditorPlugin implements PluginValue {
tr.isUserEvent("redo") || tr.isUserEvent("redo") ||
tr.isUserEvent("select") tr.isUserEvent("select")
) { ) {
console.log("OTHER EVENTS");
const textIter = tr.newDoc.iter(); const textIter = tr.newDoc.iter();
let text = ""; let text = "";
while (!textIter.done) { while (!textIter.done) {