add dfa field to app_type so that we don't rebuild DFA each time we want to execute a search again (like after deleting)

2025-10-08 05:02:15 +01:00
parent 7f68084398
commit fd8385fa81
5 changed files with 27 additions and 3 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, true, #buffer app)
+      (app, "", PersistentVector.empty, 0, 0, false, #buffer app)

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