add 'caseSensitive' field to NORMAL_SEARCH_MODE, so that we know what kind of DFA to build

2025-10-08 04:53:04 +01:00
parent 7a72bc2ed1
commit 7f68084398
4 changed files with 50 additions and 6 deletions
--- a/fcore/normal-mode/normal-mode.sml
+++ b/fcore/normal-mode/normal-mode.sml
@@ -7,7 +7,7 @@ struct

  fun switchToNormalSearchMode (app: app_type) =
    NormalSearchFinish.onSearchChanged
-      (app, "", PersistentVector.empty, 0, 0, #buffer app)
+      (app, "", PersistentVector.empty, 0, 0, true, #buffer app)

  fun getNumLength (pos, str) =
    if pos = String.size str then