aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-03-30 14:39:32 -0400
committerEmilio Jesus Gallego Arias2020-03-30 14:39:32 -0400
commit86bb0b0e97d6aa1cdf2bd073cf7b5ac654aef67c (patch)
treeae2e85b1199984e5df2af7b2521da35733def68d
parent5d912bfd5bb7dbd3634be9a204bb1fabf10223fe (diff)
parente6d0c2d24acaa5d8470d36a9173f141000126952 (diff)
Merge PR #11965: Partial revert of #11817.
Reviewed-by: ejgallego
-rw-r--r--ide/wg_Completion.ml12
1 files changed, 11 insertions, 1 deletions
diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml
index a7f8c70499..dcb71d96a1 100644
--- a/ide/wg_Completion.ml
+++ b/ide/wg_Completion.ml
@@ -8,7 +8,17 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-module Proposals = CString.Set
+module StringOrd =
+struct
+ type t = string
+ let compare s1 s2 =
+ (* we use first size, then usual comparison *)
+ let d = String.length s1 - String.length s2 in
+ if d <> 0 then d
+ else compare s1 s2
+end
+
+module Proposals = Set.Make(StringOrd)
(** Retrieve completion proposals in the buffer *)
let get_syntactic_completion (buffer : GText.buffer) pattern accu =