refactor: factor out text handling as new modules Text and Loctext (

#159)

src-lsp/LspServer.ml

@@ -56,18 +56,18 @@ struct
     let msg = Broadcast.to_jsonrpc notif in
     send (RPC.Packet.Notification msg)
 
-  let render_lsp_related_info (uri : L.DocumentUri.t) (message : Asai.Diagnostic.loctext) : L.DiagnosticRelatedInformation.t =
+  let render_lsp_related_info (uri : L.DocumentUri.t) (message : Asai.Loctext.t) : L.DiagnosticRelatedInformation.t =
     let range = LspShims.Loc.lsp_range_of_range message.loc in
     let location = L.Location.create ~uri ~range in
-    let message = Asai.Diagnostic.string_of_text message.value in
+    let message = Asai.Text.to_string message.value in
     L.DiagnosticRelatedInformation.create ~location ~message
 
   let render_lsp_diagnostic (uri : L.DocumentUri.t) (diag : diagnostic) : Lsp_Diagnostic.t =
     let range = LspShims.Loc.lsp_range_of_range diag.explanation.loc in
     let severity = LspShims.Diagnostic.lsp_severity_of_severity @@ diag.severity in
     let code = `String (Message.short_code diag.message) in
     let source = (State.get ()).source in
-    let message = Asai.Diagnostic.string_of_text diag.explanation.value in
+    let message = Asai.Text.to_string diag.explanation.value in
     let relatedInformation = Bwd.to_list @@ Bwd.map (render_lsp_related_info uri) diag.extra_remarks in
     Lsp_Diagnostic.create
       ~range

src/Asai.ml

@@ -1,4 +1,6 @@
 module Range = Range
+module Text = Text
+module Loctext = Loctext
 module Diagnostic = Diagnostic
 module Reporter = Reporter
 module StructuredReporter = StructuredReporter

src/Asai.mli

@@ -7,6 +7,16 @@
 (** Locations and ranges. *)
 module Range = Range
 
+(** Texts that preserve pretty-printing structures.
+
+    @since 0.3.2 *)
+module Text = Text
+
+(** Located texts. "Loctext" is a portmanteau of "locate" and "text".
+
+    @since 0.3.2 *)
+module Loctext = Loctext
+
 (** The definition of diagnostics and some utility functions. *)
 module Diagnostic = Diagnostic
 

src/Diagnostic.ml

@@ -2,20 +2,6 @@ open Bwd
 
 include DiagnosticData
 
-let text s fmt =
-  Format.(pp_print_list ~pp_sep:pp_force_newline pp_print_string) fmt @@
-  String.split_on_char '\n' s
-
-let textf = Format.dprintf
-
-let ktextf = Format.kdprintf
-
-let loctext ?loc s = Range.{ loc; value = text s }
-
-let kloctextf ?loc k = ktextf @@ fun loctext -> k Range.{ loc; value = loctext }
-
-let loctextf ?loc = kloctextf Fun.id ?loc
-
 let of_loctext ?(backtrace=Bwd.Emp) ?(extra_remarks=[]) severity message explanation : _ t =
   { severity
   ; message
@@ -28,14 +14,14 @@ let of_text ?loc ?backtrace ?extra_remarks severity message text : _ t =
   of_loctext ?backtrace ?extra_remarks severity message {loc; value = text}
 
 let make ?loc ?backtrace ?extra_remarks severity message explanation =
-  of_text ?loc ?backtrace ?extra_remarks severity message @@ text explanation
+  of_text ?loc ?backtrace ?extra_remarks severity message @@ Text.make explanation
 
 let kmakef ?loc ?backtrace ?extra_remarks k severity message =
-  ktextf @@ fun text ->
+  Text.kmakef @@ fun text ->
   k @@ of_text ?loc ?backtrace ?extra_remarks severity message text
 
 let makef ?loc ?backtrace ?extra_remarks severity message =
-  ktextf @@ of_text ?loc ?backtrace ?extra_remarks severity message
+  Text.kmakef @@ of_text ?loc ?backtrace ?extra_remarks severity message
 
 let map f d = {d with message = f d.message}
 
@@ -47,3 +33,13 @@ let string_of_text text : string =
   Format.pp_print_flush fmt ();
   Str.global_replace (Str.regexp "\\([\r\n]+ *\\)+") " " @@
   Buffer.contents buf
+
+type text = Text.t
+let text = Text.make
+let textf = Text.makef
+let ktextf = Text.kmakef
+
+type loctext = Loctext.t
+let loctext = Loctext.make
+let loctextf = Loctext.makef
+let kloctextf = Loctext.kmakef

src/Diagnostic.mli

@@ -3,37 +3,9 @@
 (* @include *)
 include module type of DiagnosticData
 
-(** {1 Constructing Messages} *)
-
-(** [text str] converts the string [str] into a text, converting each ['\n'] into a call to {!val:Format.pp_force_newline}. *)
-val text : string -> text
-
-(** [textf format ...] formats a text. It is an alias of {!val:Format.dprintf}. Note that there should not be any literal control characters (e.g., literal newline characters). *)
-val textf : ('a, Format.formatter, unit, text) format4 -> 'a
-
-(** [ktextf kont format ...] is [kont (textf format ...)]. It is an alias of {!val:Format.kdprintf}. *)
-val ktextf : (text -> 'b) -> ('a, Format.formatter, unit, 'b) format4 -> 'a
-
-(** [loctext str] converts the string [str] into a loctext.
-
-    @param loc The location of the loctext (usually the code) to highlight. *)
-val loctext : ?loc:Range.t -> string -> loctext
-
-(** [loctextf format ...] constructs a loctext. Note that there should not be any literal control characters (e.g., literal newline characters).
-
-    @param loc The location of the loctext (usually the code) to highlight.
-*)
-val loctextf : ?loc:Range.t -> ('a, Format.formatter, unit, loctext) format4 -> 'a
-
-(** [kloctextf kont format ...] is [kont (loctextf format ...)].
-
-    @param loc The location of the loctext (usually the code) to highlight.
-*)
-val kloctextf : ?loc:Range.t -> (loctext -> 'b) -> ('a, Format.formatter, unit, 'b) format4 -> 'a
-
 (** {1 Constructing Diagnostics} *)
 
-(** [of_text severity message text] constructs a diagnostic from a {!type:text}.
+(** [of_text severity message text] constructs a diagnostic from a {!type:Text.t}.
 
     Example:
     {[
@@ -45,9 +17,9 @@ val kloctextf : ?loc:Range.t -> (loctext -> 'b) -> ('a, Format.formatter, unit,
 
     @since 0.2.0
 *)
-val of_text : ?loc:Range.t -> ?backtrace:backtrace -> ?extra_remarks:loctext list -> severity -> 'message -> text -> 'message t
+val of_text : ?loc:Range.t -> ?backtrace:backtrace -> ?extra_remarks:Loctext.t list -> severity -> 'message -> Text.t -> 'message t
 
-(** [of_loctext severity message loctext] constructs a diagnostic from a {!type:loctext}.
+(** [of_loctext severity message loctext] constructs a diagnostic from a {!type:Loctext.t}.
 
     Example:
     {[
@@ -57,7 +29,7 @@ val of_text : ?loc:Range.t -> ?backtrace:backtrace -> ?extra_remarks:loctext lis
     @param backtrace The backtrace (to overwrite the accumulative frames up to this point).
     @param extra_remarks Additional remarks that are not part of the backtrace.
 *)
-val of_loctext : ?backtrace:backtrace -> ?extra_remarks:loctext list -> severity -> 'message -> loctext -> 'message t
+val of_loctext : ?backtrace:backtrace -> ?extra_remarks:Loctext.t list -> severity -> 'message -> Loctext.t -> 'message t
 
 (** [make severity message loctext] constructs a diagnostic with the [loctext].
 
@@ -69,9 +41,9 @@ val of_loctext : ?backtrace:backtrace -> ?extra_remarks:loctext list -> severity
     @param backtrace The backtrace (to overwrite the accumulative frames up to this point).
     @param extra_remarks Additional remarks that are not part of the backtrace.
 *)
-val make : ?loc:Range.t -> ?backtrace:backtrace -> ?extra_remarks:loctext list -> severity -> 'message -> string -> 'message t
+val make : ?loc:Range.t -> ?backtrace:backtrace -> ?extra_remarks:Loctext.t list -> severity -> 'message -> string -> 'message t
 
-(** [makef severity message format ...] is [of_loctext severity message (loctextf format ...)]. It formats the message and constructs a diagnostic out of it.
+(** [makef severity message format ...] is [of_loctext severity message (Loctext.makef format ...)]. It formats the message and constructs a diagnostic out of it.
 
     Example:
     {[
@@ -82,20 +54,55 @@ val make : ?loc:Range.t -> ?backtrace:backtrace -> ?extra_remarks:loctext list -
     @param backtrace The backtrace (to overwrite the accumulative frames up to this point).
     @param extra_remarks Additional remarks that are not part of the backtrace.
 *)
-val makef : ?loc:Range.t -> ?backtrace:backtrace -> ?extra_remarks:loctext list -> severity -> 'message -> ('a, Format.formatter, unit, 'message t) format4 -> 'a
+val makef : ?loc:Range.t -> ?backtrace:backtrace -> ?extra_remarks:Loctext.t list -> severity -> 'message -> ('a, Format.formatter, unit, 'message t) format4 -> 'a
 
 (** [kmakef kont severity message format ...] is [kont (makef severity message format ...)].
 
     @param loc The location of the text (usually the code) to highlight.
     @param backtrace The backtrace (to overwrite the accumulative frames up to this point).
     @param extra_remarks Additional remarks that are not part of the backtrace.
 *)
-val kmakef : ?loc:Range.t -> ?backtrace:backtrace -> ?extra_remarks:loctext list -> ('message t -> 'b) -> severity -> 'message -> ('a, Format.formatter, unit, 'b) format4 -> 'a
+val kmakef : ?loc:Range.t -> ?backtrace:backtrace -> ?extra_remarks:Loctext.t list -> ('message t -> 'b) -> severity -> 'message -> ('a, Format.formatter, unit, 'b) format4 -> 'a
 
 (** {1 Other Helper Functions} *)
 
 (** A convenience function that maps the message of a diagnostic. This is helpful when using {!val:Reporter.S.adopt}. *)
 val map : ('message1 -> 'message2) -> 'message1 t -> 'message2 t
 
-(** A convenience function that converts a {!type:text} into a string by formatting it with the maximum admissible margin and then replacing newlines and indentation with a space character. *)
-val string_of_text : text -> string
+(** {1 Deprecated Types and Functions} *)
+
+(** An alias of [Text.t] for backward compatibility. *)
+type text = Text.t
+[@@ocaml.alert deprecated "Use Text.t instead"]
+
+(** An alias of [Loctext.t] for backward compatibility. *)
+type loctext = Loctext.t
+[@@ocaml.alert deprecated "Use Loctext.t instead"]
+
+(** An alias of [Text.make] for backward compatibility. *)
+val text : string -> Text.t
+[@@ocaml.alert deprecated "Use Text.make instead"]
+
+(** An alias of [Text.makef] for backward compatibility. *)
+val textf : ('a, Format.formatter, unit, Text.t) format4 -> 'a
+[@@ocaml.alert deprecated "Use Text.makef instead"]
+
+(** An alias of [Text.kmakef] for backward compatibility. *)
+val ktextf : (Text.t -> 'b) -> ('a, Format.formatter, unit, 'b) format4 -> 'a
+[@@ocaml.alert deprecated "Use Text.kmakef instead"]
+
+(** An alias of [Loctext.make] for backward compatibility. *)
+val loctext : ?loc:Range.t -> string -> Loctext.t
+[@@ocaml.alert deprecated "Use Loctext.make instead"]
+
+(** An alias of [Loctext.makef] for backward compatibility. *)
+val loctextf : ?loc:Range.t -> ('a, Format.formatter, unit, Loctext.t) format4 -> 'a
+[@@ocaml.alert deprecated "Use Loctext.makef instead"]
+
+(** An alias of [Loctext.kmakef] for backward compatibility. *)
+val kloctextf : ?loc:Range.t -> (Loctext.t -> 'b) -> ('a, Format.formatter, unit, 'b) format4 -> 'a
+[@@ocaml.alert deprecated "Use Loctext.kmakef instead"]
+
+(** An alias of [Text.to_string] for backward compatibility. *)
+val string_of_text : Text.t -> string
+[@@ocaml.alert deprecated "Use Text.to_string instead"]

src/DiagnosticData.ml

@@ -8,35 +8,19 @@ type severity =
   | Error (** A serious error caused by the end user (the user of your proof assistant or compiler) or other external factors (e.g., internet not working). *)
   | Bug (** A serious error likely caused by a bug in the proof assistant. You would want the end user to report the bug back to you. This is useful for indicating that certain branches in a pattern matching should be "impossible", while printing out debugging information in case the program logic is flawed. *)
 
-(** The type of texts.
-
-    When we render a diagnostic, the layout engine of the diagnostic handler should be the one making layout choices. Therefore, we cannot pass already formatted strings. Instead, a text is defined to be a function that takes a formatter and uses it to render the content. A valid text must satisfy the following two conditions:
-    + {b All string (and character) literals must be encoded using UTF-8.}
-    + {b All string (and character) literals must not contain control characters (such as the newline character [\n]).} It is okay to have break hints (such as [@,] and [@ ]) but not literal control characters. This means you should avoid pre-formatted strings, and if you must use them, use {!val:text} to convert newline characters. Control characters include `U+0000-001F` (C0 controls), `U+007F` (backspace) and `U+0080-009F` (C1 controls). These characters are banned because they would mess up the cursor position.
-
-    {i Pro-tip:} to format a text in another text, use [%t]:
-    {[
-      let t = textf "@[<2>this is what the master said:@ @[%t@]@]" inner_text
-    ]}
-*)
-type text = Format.formatter -> unit
-
-(** A loctext is a {!type:text} with location information. "loctext" is a portmanteau of "locate" and "text". *)
-type loctext = text Range.located
-
 (** A backtrace is a (backward) list of loctexts. *)
-type backtrace = loctext bwd
+type backtrace = Loctext.t bwd
 
 (** The type of diagnostics. *)
 type 'message t = {
   severity : severity;
   (** Severity of the diagnostic. *)
   message : 'message;
   (** The (structured) message. *)
-  explanation : loctext;
+  explanation : Loctext.t;
   (** The free-form explanation. *)
   backtrace : backtrace;
   (** The backtrace leading to this diagnostic. *)
-  extra_remarks : loctext bwd;
+  extra_remarks : Loctext.t bwd;
   (** Additional remarks that are relevant to the main message but not part of the backtrace. It is a backward list so that new remarks can be added to its end easily. *)
 }

src/GitHub.ml

@@ -13,7 +13,7 @@ module Make (Message : Reporter.Message) = struct
     Format.printf "::%s title=%s::%s@."
       (command_of_severity severity)
       (Message.short_code msg)
-      (Diagnostic.string_of_text text)
+      (Text.to_string text)
 
   let print_with_loc severity msg loc text =
     match Range.source loc with
@@ -26,7 +26,7 @@ module Make (Message : Reporter.Message) = struct
         (Range.begin_line_num loc)
         (Range.end_line_num loc)
         (Message.short_code msg)
-        (Diagnostic.string_of_text text)
+        (Text.to_string text)
 
   let print Diagnostic.{severity; message; explanation = {loc; value = text}; _} =
     match loc with

src/Loctext.ml

@@ -0,0 +1,7 @@
+type t = Text.t Range.located
+
+let make ?loc s : t = Range.locate_opt loc @@ Text.make s
+
+let kmakef ?loc k = Text.kmakef @@ fun t -> k @@ Range.locate_opt loc t
+
+let makef ?loc = Text.kmakef @@ Range.locate_opt loc

src/Loctext.mli

@@ -0,0 +1,23 @@
+(** {1 Types} *)
+
+(** A located text *)
+type t = Text.t Range.located
+
+(** {1 Builders} *)
+
+(** [make str] converts the string [str] into a located text.
+
+    @param loc The location of the text (usually the code) to highlight. *)
+val make : ?loc:Range.t -> string -> t
+
+(** [makef format ...] constructs a located text. Note that there should not be any literal control characters (e.g., literal newline characters).
+
+    @param loc The location of the text (usually the code) to highlight.
+*)
+val makef : ?loc:Range.t -> ('a, Format.formatter, unit, t) format4 -> 'a
+
+(** [kmakef kont format ...] is [kont (makef format ...)].
+
+    @param loc The location of the text (usually the code) to highlight.
+*)
+val kmakef : ?loc:Range.t -> (t -> 'b) -> ('a, Format.formatter, unit, 'b) format4 -> 'a

src/Reporter.ml

@@ -27,12 +27,12 @@ struct
     (match loc with None -> l | Some _ -> loc),
     bt <: {loc; value = text}
 
-  let trace_loctext (t : Diagnostic.loctext) =
+  let trace_loctext (t : Loctext.t) =
     trace_text ?loc:t.loc t.value
 
-  let trace ?loc str = trace_text ?loc @@ Diagnostic.text str
+  let trace ?loc str = trace_text ?loc @@ Text.make str
 
-  let tracef ?loc = Diagnostic.kloctextf trace_loctext ?loc
+  let tracef ?loc = Loctext.kmakef trace_loctext ?loc
 
   (* Constructing diagnostics *)