aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction
diff options
context:
space:
mode:
authorGravatar Paul Steckler <steck@stecksoft.com>2017-11-22 14:48:04 -0500
committerGravatar Paul Steckler <steck@stecksoft.com>2017-11-22 14:48:04 -0500
commit79da97a3e02a079e3d91f04fd012886c57d4c1e8 (patch)
tree6d7082fac640c9f5e2aad9b2e8e99f2587479c83 /plugins/extraction
parentecfb73d655601e9aed736b0083a6f6b4682a2083 (diff)
allow whitespace around infix op
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/ocaml.ml6
1 files changed, 4 insertions, 2 deletions
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index eea5968ce..fb8dfb459 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -122,11 +122,13 @@ let is_infix r =
len >= 3 &&
(* parenthesized *)
(s.[0] == '(' && s.[len-1] == ')' &&
+ let inparens = String.trim (String.sub s 1 (len - 2)) in
+ let inparens_len = String.length inparens in
(* either, begins with infix symbol, any remainder is all operator chars *)
- (List.mem s.[1] infix_symbols && substring_all_opchars s 2 (len-1))
+ (List.mem inparens.[0] infix_symbols && substring_all_opchars inparens 1 inparens_len)
||
(* or, starts with #, at least one more char, all are operator chars *)
- (s.[1] == '#' && len >= 4 && substring_all_opchars s 2 (len-1))))
+ (inparens.[0] == '#' && inparens_len >= 2 && substring_all_opchars inparens 1 inparens_len)))
let get_infix r =
let s = find_custom r in