Merge pull request #844 from ejgallego/nits_refactor_fleche

Nits refactor fleche

controller/rq_goals.ml

@@ -6,9 +6,7 @@
 (************************************************************************)
 
 (* Replace by ppx when we can print goals properly in the client *)
-let mk_message (range, level, text) =
-  let level = Lang.Diagnostic.Severity.to_int level in
-  Lsp.JFleche.Message.{ range; level; text }
+let mk_message (range, level, text) = Lsp.JFleche.Message.{ range; level; text }
 
 let mk_messages node =
   Option.map Fleche.Doc.Node.messages node

fleche/doc.ml

@@ -225,8 +225,10 @@ end = struct
       else 3
     in
     let f (_, lvl, _) =
-      let lvl = Lang.Diagnostic.Severity.to_int lvl in
-      if lvl = 2 then Both else if lvl < cutoff then Left else Right
+      (* warning = 2 *)
+      if lvl = Lang.Diagnostic.Severity.warning then Both
+      else if lvl < cutoff then Left
+      else Right
     in
     let diags, messages = partition ~f fbs in
     (List.map (of_feed ~drange) diags, messages)
@@ -670,16 +672,17 @@ let search_node ~command ~doc ~st =
       (fun (node : Node.t) -> Option.default Memo.Stats.zero node.info.stats)
       Memo.Stats.zero node
   in
+  let back_overflow num =
+    let ll = List.length doc.nodes in
+    Pp.(
+      str "not enough nodes: [" ++ int num ++ str " > " ++ int ll
+      ++ str "] available document nodes")
+  in
   match command with
   | Coq.Ast.Meta.Command.Back num -> (
     match Base.List.nth doc.nodes num with
     | None ->
-      let ll = List.length doc.nodes in
-      let message =
-        Pp.(
-          str "not enough nodes: [" ++ int num ++ str " > " ++ int ll
-          ++ str "] available document nodes")
-      in
+      let message = back_overflow num in
       (Coq.Protect.E.error message, nstats None)
     | Some node -> (Coq.Protect.E.ok node.state, nstats (Some node)))
   | Restart -> (

lang/diagnostic.ml

@@ -25,7 +25,6 @@ module Severity = struct
   let warning = 2
   let information = 3
   let hint = 4
-  let to_int x = x
 end
 
 type t =

lang/diagnostic.mli

@@ -19,15 +19,12 @@ module Data : sig
 end
 
 module Severity : sig
-  type t
+  type t = int
 
-  val error : t
-  val warning : t
-  val information : t
-  val hint : t
-
-  (** Convert to LSP-like levels *)
-  val to_int : t -> int
+  val error : t (* 1 *)
+  val warning : t (* 2 *)
+  val information : t (* 3 *)
+  val hint : t (* 4 *)
 end
 
 type t =

lsp/jLang.ml

@@ -89,7 +89,6 @@ module Diagnostic = struct
 
   let to_yojson { Lang.Diagnostic.range; severity; message; data } =
     let range = Range.conv range in
-    let severity = Lang.Diagnostic.Severity.to_int severity in
     let message = Pp.to_string message in
     _t_to_yojson { range; severity; message; data }
 end