aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto2/src
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-10-17 23:03:14 +0200
committerEmilio Jesus Gallego Arias2018-10-18 19:35:57 +0200
commit8303c9cab6bc403dfc209f65287b67e883a35711 (patch)
tree9e6a086583aec8c58ab43c489cc3b863f500a48f /doc/plugin_tutorial/tuto2/src
parentc3823156da73a63967d9d472e21560af1585b271 (diff)
[clib] Provide `filter_range` function.
This is very useful to compute efficiently a list of prefixes. Will be used in conjunction with the nametab to provide completion. Example of use: ``` let cprefix x y = String.(compare x (sub y 0 (min (length x) (length y)))) in M.filter_range (cprefix "foo") m ``` We could of course maintain a trie, but this is less invasive an should work at our scale.
Diffstat (limited to 'doc/plugin_tutorial/tuto2/src')
0 files changed, 0 insertions, 0 deletions