summaryrefslogtreecommitdiff
path: root/src/search.sml
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@mit.edu>2020-05-30 19:49:56 -0400
committerGravatar Benjamin Barenblat <bbaren@mit.edu>2020-05-30 19:49:56 -0400
commitc2f1e1096f602b1cbd4531352f3e1ea6d656a186 (patch)
treeae102982878bb0c31bdfe07209e60bfc14030490 /src/search.sml
parent095c2640aa2070ed4e2765875238d5e6e6673856 (diff)
parent5a0b639dfbd7db9d16c6995f72ba17152a1f362d (diff)
Merge branch 'upstream' into dfsg_clean20200209+dfsgdfsg_clean
Diffstat (limited to 'src/search.sml')
-rw-r--r--src/search.sml8
1 files changed, 8 insertions, 0 deletions
diff --git a/src/search.sml b/src/search.sml
index 563496fe..5e4e135f 100644
--- a/src/search.sml
+++ b/src/search.sml
@@ -70,4 +70,12 @@ fun bindP (r, f) =
((x', pos), acc'))
| Return x => Return x
+fun bindPWithPos (r, f) =
+ case r of
+ Continue ((x, pos), acc) =>
+ map (f (x, pos) acc,
+ fn (x', acc') =>
+ ((x', pos), acc'))
+ | Return x => Return x
+
end