From fbc606bc12ebeb2e62872b2d038215849d56bef6 Mon Sep 17 00:00:00 2001
From: Matthew Richards <mrichards30630@gmail.com>
Date: Mon, 15 Jul 2024 11:10:57 +1000
Subject: [PATCH] Refactor DB.find fix

---
 src/postkernel/DB.sml             |  5 ++---
 src/postkernel/DBSearchParser.sig |  2 +-
 src/postkernel/DBSearchParser.sml | 11 ++++++++---
 3 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/src/postkernel/DB.sml b/src/postkernel/DB.sml
index acf9e3fab4..b17f3db113 100644
--- a/src/postkernel/DB.sml
+++ b/src/postkernel/DB.sml
@@ -228,10 +228,9 @@ fun thy s =
 fun findpred pat =
     let
         val pat = toLower pat
-        open DBSearchParser regexpMatch
-        val r = translate_regexp $ parse_regexp pat
+        open DBSearchParser
     in
-        match (contains r) o toLower
+        contains_regexp pat o toLower
     end
 
 fun find0 incprivatep s =
diff --git a/src/postkernel/DBSearchParser.sig b/src/postkernel/DBSearchParser.sig
index 44c3340802..4dcf2cf139 100644
--- a/src/postkernel/DBSearchParser.sig
+++ b/src/postkernel/DBSearchParser.sig
@@ -9,5 +9,5 @@ sig
                 | Any
     val parse_regexp : string -> search_regexp
     val translate_regexp : search_regexp -> regexpMatch.regexp
-    val contains : regexpMatch.regexp -> regexpMatch.regexp
+    val contains_regexp : string -> string -> bool
 end
diff --git a/src/postkernel/DBSearchParser.sml b/src/postkernel/DBSearchParser.sml
index e860c7f4ec..14586ac884 100644
--- a/src/postkernel/DBSearchParser.sml
+++ b/src/postkernel/DBSearchParser.sml
@@ -77,6 +77,7 @@ fun parse_regexp input = let
           | T(#"*")::(E a)::ts => E(Many(a))::ts
           | T(#"*")::(T c)::ts => E(Many(Word [c]))::ts
           | (T #")")::(E x)::(T #"(")::ts => E x::ts
+          | (T #")")::(E x)::(E y)::ts => (T #")")::E(Seq(y, x))::ts
           | (E a)::(E b)::ts => E(Seq(b, a))::ts
           | T(c)::E(Word cs)::ts => E(Word(cs@[c]))::ts
           | T(c)::ts => E(Word [c])::ts
@@ -115,8 +116,12 @@ in
       | Any => Symbs word_set
 end
 
-val is_regexp = List.exists is_special_char o String.explode
-
-fun contains pat = Dot (any, Dot (pat, any))
+fun contains_regexp pattern = let
+    val intermediate = parse_regexp pattern
+    val compiled_pattern = translate_regexp intermediate
+    fun contains pat = Dot (any, Dot (pat, any))
+in
+    match (contains compiled_pattern)
+end
 
 end