FStar.Issue: exposing doc_of_issue

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
 

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. *)

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)