From 42b4f4b6349d8d9065a64d440d440474008d0e9b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Sat, 18 Jan 2025 01:18:28 -0800
Subject: [PATCH] FStar.Issue: exposing doc_of_issue

---
 src/basic/FStarC.Errors.fst   | 18 +++++++++---------
 ulib/FStar.Issue.fsti         |  4 +++-
 ulib/ml/plugin/FStar_Issue.ml |  1 +
 3 files changed, 13 insertions(+), 10 deletions(-)

diff --git a/src/basic/FStarC.Errors.fst b/src/basic/FStarC.Errors.fst
index 15ab8ea43a1..db8f7b300d8 100644
--- a/src/basic/FStarC.Errors.fst
+++ b/src/basic/FStarC.Errors.fst
@@ -179,7 +179,7 @@ let optional_def (f : 'a -> PP.document) (def : PP.document) (o : option 'a) : P
   | Some x -> f x
   | None -> def
 
-let format_issue' (print_hdr:bool) (issue:issue) : string =
+let issue_to_doc' (print_hdr:bool) (issue:issue) : PP.document =
   let open FStarC.Pprint in
   let r = issue.issue_range in
   let hdr : document =
@@ -221,14 +221,14 @@ let format_issue' (print_hdr:bool) (issue:issue) : string =
   let mainmsg : document =
     concat (List.map (fun d -> subdoc (group d)) issue.issue_msg)
   in
-  let doc : document =
-    (* This ends in a hardline to get a 1-line spacing between errors *)
-    hdr ^^
-    mainmsg ^^
-    subdoc seealso ^^
-    subdoc ctx
-  in
-  renderdoc doc
+  (* This ends in a hardline to get a 1-line spacing between errors *)
+  hdr ^^
+  mainmsg ^^
+  subdoc seealso ^^
+  subdoc ctx
+
+let format_issue' (print_hdr:bool) (issue:issue) : string =
+  issue_to_doc' print_hdr issue |> renderdoc
 
 let format_issue issue : string = format_issue' true issue
 
diff --git a/ulib/FStar.Issue.fsti b/ulib/FStar.Issue.fsti
index 3697227fc1e..68b98a1139e 100644
--- a/ulib/FStar.Issue.fsti
+++ b/ulib/FStar.Issue.fsti
@@ -23,8 +23,10 @@ val range_of_issue (i:issue) : Tot (option range)
 
 val context_of_issue (i:issue) : Tot (list string)
 
+val issue_to_doc (i:issue) : Tot Pprint.document
+
 val render_issue (i:issue) : Tot string
-  
+
 (* NOTE: the only way to build a document that actually reduces
 in interpreted mode (like in tactics when not using plugins)
 is using arbitrary_string, as below. *)
diff --git a/ulib/ml/plugin/FStar_Issue.ml b/ulib/ml/plugin/FStar_Issue.ml
index a01130994e8..3286f0ca6cf 100644
--- a/ulib/ml/plugin/FStar_Issue.ml
+++ b/ulib/ml/plugin/FStar_Issue.ml
@@ -29,6 +29,7 @@ let mk_issue_level (i:issue_level_string)
     | "Info" -> EInfo
     | "Warning" -> EWarning
 
+let issue_to_doc (i:issue) : FStarC_Pprint.document = FStarC_Errors.issue_to_doc' true i
 let render_issue (i:issue) : string = FStarC_Errors.format_issue i
 
 let mk_issue_doc (i:issue_level_string)