From 9282955774715e6950f0f6ef19d01f285786f4ca Mon Sep 17 00:00:00 2001
From: Shachar Itzhaky <corwin.amber@gmail.com>
Date: Sat, 15 May 2021 22:05:32 +0300
Subject: [PATCH] [bugfix] [ui] Workaround horizontal scrolling.
Try to avoid a situation when the documents stays scrolled too much to
the right after a long sentence has been executed.
---
ui-js/cm-provider.js | 1 +
1 file changed, 1 insertion(+)
diff --git a/ui-js/cm-provider.js b/ui-js/cm-provider.js
index 0f2c8ea8..00a9130b 100644
--- a/ui-js/cm-provider.js
+++ b/ui-js/cm-provider.js
@@ -337,6 +337,7 @@ class CmCoqProvider {
}
cursorToEnd(stm) {
+ this.editor.scrollTo(0); // try to get back to the leftmost part
this.editor.setCursor(stm.end);
}
--
GitLab