diff options
| author | Emilio Jesus Gallego Arias | 2019-07-03 12:54:37 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-08 13:18:47 +0200 |
| commit | dda7d129dba6c90d642cd99cd989e5f13c0eb4b4 (patch) | |
| tree | 23fdc06a01b17e81c0c03831e675bcc2b0bb94e7 /ide | |
| parent | 437063a0c745094c5693d1c5abba46ce375d69c6 (diff) | |
[core] [api] Support OCaml 4.08
The changes are large due to `Pervasives` deprecation:
- the `Pervasives` module has been deprecated in favor of `Stdlib`, we
have opted for introducing a few wrapping functions in `Util` and
just unqualified the rest of occurrences. We avoid the shims as in
the previous attempt.
- a bug regarding partial application have been fixed.
- some formatting functions have been deprecated, but previous
versions don't include a replacement, thus the warning has been
disabled.
We may want to clean up things a bit more, in particular
w.r.t. modules once we can move to OCaml 4.07 as the minimum required
version.
Note that there is a clash between 4.08.0 modules `Option` and `Int`
and Coq's ones. It is not clear if we should resolve that clash or
not, see PR #10469 for more discussion.
On the good side, OCaml 4.08.0 does provide a few interesting
functionalities, including nice new warnings useful for devs.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/protocol/richpp.ml | 6 | ||||
| -rw-r--r-- | ide/session.ml | 4 | ||||
| -rw-r--r-- | ide/wg_Completion.ml | 2 |
3 files changed, 6 insertions, 6 deletions
diff --git a/ide/protocol/richpp.ml b/ide/protocol/richpp.ml index 507b985d2f..463d93af0d 100644 --- a/ide/protocol/richpp.ml +++ b/ide/protocol/richpp.ml @@ -94,7 +94,7 @@ let rich_pp width ppcmds = print_close_tag = ignore; } in - pp_set_formatter_tag_functions ft tag_functions; + pp_set_formatter_tag_functions ft tag_functions [@warning "-3"]; pp_set_mark_tags ft true; (* Setting the formatter *) @@ -107,9 +107,9 @@ let rich_pp width ppcmds = (* The whole output must be a valid document. To that end, we nest the document inside <pp> tags. *) pp_open_box ft 0; - pp_open_tag ft "pp"; + pp_open_tag ft "pp" [@warning "-3"]; Pp.(pp_with ft ppcmds); - pp_close_tag ft (); + pp_close_tag ft () [@warning "-3"]; pp_close_box ft (); (* Get the resulting XML tree. *) diff --git a/ide/session.ml b/ide/session.ml index 3792730455..a9c106a765 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -275,9 +275,9 @@ let make_table_widget ?sort cd cb = let make_sorting i (_, c) = let sort (store : GTree.model) it1 it2 = match c with | `IntC c -> - Pervasives.compare (store#get ~row:it1 ~column:c) (store#get ~row:it2 ~column:c) + compare (store#get ~row:it1 ~column:c) (store#get ~row:it2 ~column:c) | `StringC c -> - Pervasives.compare (store#get ~row:it1 ~column:c) (store#get ~row:it2 ~column:c) + compare (store#get ~row:it1 ~column:c) (store#get ~row:it2 ~column:c) in store#set_sort_func i sort in diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml index 7758d89ed8..98390e810f 100644 --- a/ide/wg_Completion.ml +++ b/ide/wg_Completion.ml @@ -15,7 +15,7 @@ struct (* we use first size, then usual comparison *) let d = String.length s1 - String.length s2 in if d <> 0 then d - else Pervasives.compare s1 s2 + else compare s1 s2 end module Proposals = Set.Make(StringOrd) |
