From b70ba5f6986e0875d151a459f307c71df9104019 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Sun, 29 Sep 2024 15:37:07 +0200
Subject: [PATCH 1/2] [fleche] Aesthetic refactoring.

---
 fleche/doc.ml | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/fleche/doc.ml b/fleche/doc.ml
index 4c02c7b2..f21c548b 100644
--- a/fleche/doc.ml
+++ b/fleche/doc.ml
@@ -670,16 +670,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 -> (

From 64943ff21997ea1de6e769936633d64a8e767550 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 30 Sep 2024 13:22:03 +0200
Subject: [PATCH 2/2] [internal] Don't make severity type private.

This wasn't a good tradeoff in the end, but a nuisance.
---
 controller/rq_goals.ml |  4 +---
 fleche/doc.ml          |  6 ++++--
 lang/diagnostic.ml     |  1 -
 lang/diagnostic.mli    | 13 +++++--------
 lsp/jLang.ml           |  1 -
 5 files changed, 10 insertions(+), 15 deletions(-)

diff --git a/controller/rq_goals.ml b/controller/rq_goals.ml
index 2299de66..e420b884 100644
--- a/controller/rq_goals.ml
+++ b/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
diff --git a/fleche/doc.ml b/fleche/doc.ml
index f21c548b..282afecc 100644
--- a/fleche/doc.ml
+++ b/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)
diff --git a/lang/diagnostic.ml b/lang/diagnostic.ml
index 84b30753..db01508c 100644
--- a/lang/diagnostic.ml
+++ b/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 =
diff --git a/lang/diagnostic.mli b/lang/diagnostic.mli
index 282d10f6..1087171f 100644
--- a/lang/diagnostic.mli
+++ b/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 =
diff --git a/lsp/jLang.ml b/lsp/jLang.ml
index 27e17c04..631d902a 100644
--- a/lsp/jLang.ml
+++ b/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