From d38ae1a9a79eee7f9aee89df3edeb884607e0398 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Wed, 9 Oct 2024 09:08:12 -0500
Subject: [PATCH] refactor: factor out text handling as new modules `Text` and
 `Loctext` (#159)

---
 src-lsp/LspServer.ml          |  6 +--
 src/Asai.ml                   |  2 +
 src/Asai.mli                  | 10 +++++
 src/Diagnostic.ml             | 30 ++++++-------
 src/Diagnostic.mli            | 83 +++++++++++++++++++----------------
 src/DiagnosticData.ml         | 22 ++--------
 src/GitHub.ml                 |  4 +-
 src/Loctext.ml                |  7 +++
 src/Loctext.mli               | 23 ++++++++++
 src/Reporter.ml               |  6 +--
 src/ReporterSigs.ml           | 28 ++++++------
 src/StructuredReporterSigs.ml | 16 +++----
 src/Text.ml                   | 18 ++++++++
 src/Text.mli                  | 30 +++++++++++++
 src/tty/Tty.ml                |  2 +-
 src/tty/TtyTag.ml             |  2 +-
 test/TestDiagnostic.ml        | 13 ------
 test/TestText.ml              | 13 ++++++
 test/TestTty.ml               | 18 ++++----
 test/dune                     |  4 +-
 20 files changed, 207 insertions(+), 130 deletions(-)
 create mode 100644 src/Loctext.ml
 create mode 100644 src/Loctext.mli
 create mode 100644 src/Text.ml
 create mode 100644 src/Text.mli
 delete mode 100644 test/TestDiagnostic.ml
 create mode 100644 test/TestText.ml

diff --git a/src-lsp/LspServer.ml b/src-lsp/LspServer.ml
index 9588eede..2e91dd6e 100644
--- a/src-lsp/LspServer.ml
+++ b/src-lsp/LspServer.ml
@@ -56,10 +56,10 @@ 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 =
@@ -67,7 +67,7 @@ struct
     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
diff --git a/src/Asai.ml b/src/Asai.ml
index d75d2f3d..20567fbc 100644
--- a/src/Asai.ml
+++ b/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
diff --git a/src/Asai.mli b/src/Asai.mli
index 56a984c7..418ff03c 100644
--- a/src/Asai.mli
+++ b/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
 
diff --git a/src/Diagnostic.ml b/src/Diagnostic.ml
index 35c2f811..a9df61b6 100644
--- a/src/Diagnostic.ml
+++ b/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
diff --git a/src/Diagnostic.mli b/src/Diagnostic.mli
index 5c14a8e8..4bf7ba24 100644
--- a/src/Diagnostic.mli
+++ b/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,7 +54,7 @@ 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 ...)].
 
@@ -90,12 +62,47 @@ val makef : ?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 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"]
diff --git a/src/DiagnosticData.ml b/src/DiagnosticData.ml
index 46dee7b1..404ddf80 100644
--- a/src/DiagnosticData.ml
+++ b/src/DiagnosticData.ml
@@ -8,24 +8,8 @@ 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 = {
@@ -33,10 +17,10 @@ type 'message t = {
   (** 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. *)
 }
diff --git a/src/GitHub.ml b/src/GitHub.ml
index f5208607..a165f0b1 100644
--- a/src/GitHub.ml
+++ b/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
diff --git a/src/Loctext.ml b/src/Loctext.ml
new file mode 100644
index 00000000..8c410c36
--- /dev/null
+++ b/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
diff --git a/src/Loctext.mli b/src/Loctext.mli
new file mode 100644
index 00000000..f684fb65
--- /dev/null
+++ b/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
diff --git a/src/Reporter.ml b/src/Reporter.ml
index c7ac2095..81653cb1 100644
--- a/src/Reporter.ml
+++ b/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 *)
 
diff --git a/src/ReporterSigs.ml b/src/ReporterSigs.ml
index f0df6e90..ef79b12c 100644
--- a/src/ReporterSigs.ml
+++ b/src/ReporterSigs.ml
@@ -32,9 +32,9 @@ sig
       @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 emit : ?severity:Diagnostic.severity -> ?loc:Range.t -> ?backtrace:Diagnostic.backtrace -> ?extra_remarks:Diagnostic.loctext list -> Message.t -> string -> unit
+  val emit : ?severity:Diagnostic.severity -> ?loc:Range.t -> ?backtrace:Diagnostic.backtrace -> ?extra_remarks:Loctext.t list -> Message.t -> string -> unit
 
-  (** [emitf message format ...] formats and emits a message, and then continues the computation. Note that there should not be any literal control characters. See {!type:Diagnostic.text}.
+  (** [emitf message format ...] formats and emits a message, and then continues the computation. Note that there should not be any literal control characters. See {!type:Text.t}.
 
       Example:
       {[
@@ -46,7 +46,7 @@ sig
       @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 emitf : ?severity:Diagnostic.severity -> ?loc:Range.t -> ?backtrace:Diagnostic.backtrace -> ?extra_remarks:Diagnostic.loctext list -> Message.t -> ('a, Format.formatter, unit, unit) format4 -> 'a
+  val emitf : ?severity:Diagnostic.severity -> ?loc:Range.t -> ?backtrace:Diagnostic.backtrace -> ?extra_remarks:Loctext.t list -> Message.t -> ('a, Format.formatter, unit, unit) format4 -> 'a
 
   (** Emit a diagnostic and continue the computation. *)
   val emit_diagnostic : Message.t Diagnostic.t -> unit
@@ -63,9 +63,9 @@ sig
       @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 fatal : ?severity:Diagnostic.severity -> ?loc:Range.t -> ?backtrace:Diagnostic.backtrace -> ?extra_remarks:Diagnostic.loctext list -> Message.t -> string -> 'a
+  val fatal : ?severity:Diagnostic.severity -> ?loc:Range.t -> ?backtrace:Diagnostic.backtrace -> ?extra_remarks:Loctext.t list -> Message.t -> string -> 'a
 
-  (** [fatalf message format ...] constructs a diagnostic and aborts the current computation with the diagnostic. Note that there should not be any literal control characters. See {!type:Diagnostic.text}.
+  (** [fatalf message format ...] constructs a diagnostic and aborts the current computation with the diagnostic. Note that there should not be any literal control characters. See {!type:Text.t}.
 
       Example:
       {[
@@ -77,7 +77,7 @@ sig
       @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 fatalf : ?severity:Diagnostic.severity -> ?loc:Range.t -> ?backtrace:Diagnostic.backtrace -> ?extra_remarks:Diagnostic.loctext list -> Message.t -> ('a, Format.formatter, unit, 'b) format4 -> 'a
+  val fatalf : ?severity:Diagnostic.severity -> ?loc:Range.t -> ?backtrace:Diagnostic.backtrace -> ?extra_remarks:Loctext.t list -> Message.t -> ('a, Format.formatter, unit, 'b) format4 -> 'a
 
   (** Abort the computation with a diagnostic. *)
   val fatal_diagnostic: Message.t Diagnostic.t -> 'a
@@ -103,7 +103,7 @@ sig
   *)
   val trace : ?loc:Range.t -> string -> (unit -> 'a) -> 'a
 
-  (** [tracef format ... f] formats and records a frame in the backtrace, and runs the thunk [f] with the new backtrace. Note that there should not be any literal control characters. See {!type:Diagnostic.text}.
+  (** [tracef format ... f] formats and records a frame in the backtrace, and runs the thunk [f] with the new backtrace. Note that there should not be any literal control characters. See {!type:Text.t}.
 
       @param loc The location of the text (usually the code) to highlight. Note that a location given here will become the new default location for inner {!val:emit} and {!val:fatal}.
   *)
@@ -113,10 +113,10 @@ sig
 
       @param loc The location of the text (usually the code) to highlight. Note that a location given here will become the new default location for inner {!val:emit} and {!val:fatal}.
   *)
-  val trace_text : ?loc:Range.t -> Diagnostic.text -> (unit -> 'a) -> 'a
+  val trace_text : ?loc:Range.t -> Text.t -> (unit -> 'a) -> 'a
 
   (** [trace_loctext loctext f] records the [loctext] and runs the thunk [f] with the new backtrace. Note that a non-[None] location given here will become the new default location for inner {!val:emit} and {!val:fatal}. *)
-  val trace_loctext : Diagnostic.loctext -> (unit -> 'a) -> 'a
+  val trace_loctext : Loctext.t -> (unit -> 'a) -> 'a
 
   (** {2 Locations} *)
 
@@ -145,9 +145,9 @@ sig
       @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 diagnostic : ?severity:Diagnostic.severity -> ?loc:Range.t -> ?backtrace:Diagnostic.backtrace -> ?extra_remarks:Diagnostic.loctext list -> Message.t -> string -> Message.t Diagnostic.t
+  val diagnostic : ?severity:Diagnostic.severity -> ?loc:Range.t -> ?backtrace:Diagnostic.backtrace -> ?extra_remarks:Loctext.t list -> Message.t -> string -> Message.t Diagnostic.t
 
-  (** [diagnosticf message format ...] constructs a diagnostic along with the backtrace frames recorded via {!val:trace}. Note that there should not be any literal control characters. See {!type:Diagnostic.text}.
+  (** [diagnosticf message format ...] constructs a diagnostic along with the backtrace frames recorded via {!val:trace}. Note that there should not be any literal control characters. See {!type:Text.t}.
 
       Example:
       {[
@@ -159,16 +159,16 @@ sig
       @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 diagnosticf : ?severity:Diagnostic.severity -> ?loc:Range.t -> ?backtrace:Diagnostic.backtrace -> ?extra_remarks:Diagnostic.loctext list -> Message.t -> ('a, Format.formatter, unit, Message.t Diagnostic.t) format4 -> 'a
+  val diagnosticf : ?severity:Diagnostic.severity -> ?loc:Range.t -> ?backtrace:Diagnostic.backtrace -> ?extra_remarks:Loctext.t list -> Message.t -> ('a, Format.formatter, unit, Message.t Diagnostic.t) format4 -> 'a
 
-  (** [kdiagnosticf kont message format ...] is [kont (diagnosticf message format ...)]. Note that there should not be any literal control characters. See {!type:Diagnostic.text}.
+  (** [kdiagnosticf kont message format ...] is [kont (diagnosticf message format ...)]. Note that there should not be any literal control characters. See {!type:Text.t}.
 
       @param severity The severity (to overwrite the default severity inferred from the [message]).
       @param loc The location of the text (usually the code) to highlight. The default value is the innermost location given by {!val:trace}, {!val:with_loc}, {!val:merge_loc}, or {!run}.
       @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 kdiagnosticf : ?severity:Diagnostic.severity -> ?loc:Range.t -> ?backtrace:Diagnostic.backtrace -> ?extra_remarks:Diagnostic.loctext list -> (Message.t Diagnostic.t -> 'b) -> Message.t -> ('a, Format.formatter, unit, 'b) format4 -> 'a
+  val kdiagnosticf : ?severity:Diagnostic.severity -> ?loc:Range.t -> ?backtrace:Diagnostic.backtrace -> ?extra_remarks:Loctext.t list -> (Message.t Diagnostic.t -> 'b) -> Message.t -> ('a, Format.formatter, unit, 'b) format4 -> 'a
 
   (** {2 Algebraic Effects} *)
 
diff --git a/src/StructuredReporterSigs.ml b/src/StructuredReporterSigs.ml
index 400938eb..e361bbd5 100644
--- a/src/StructuredReporterSigs.ml
+++ b/src/StructuredReporterSigs.ml
@@ -7,8 +7,8 @@ sig
   (** The default severity level of a message. Severity levels classify diagnostics into errors, warnings, etc. It is about how serious the {i end user} should take the diagnostic, not whether the program should stop or continue. The severity may be overwritten at the time of issuing a diagnostic. *)
   val default_severity : t -> Diagnostic.severity
 
-  (** The default text of the message. This is the long explanation of the message that the end user would see. You might find helper functions {!val:Diagnostic.text} and {!val:Diagnostic.textf} useful. The text may be overwritten at the time of issuing a diagnostic. *)
-  val default_text : t -> Diagnostic.text
+  (** The default text of the message. This is the long explanation of the message that the end user would see. You might find helper functions {!val:Text.t} and {!val:Text.tf} useful. The text may be overwritten at the time of issuing a diagnostic. *)
+  val default_text : t -> Text.t
 
   (** A concise, ideally Google-able string representation of each message. Detailed or long descriptions should be avoided---the shorter, the better. For example, [E001] works better than [type-checking error]. It will be assumed that the string representation has no control characters (such as newline characters). *)
   val short_code : t -> string
@@ -33,7 +33,7 @@ sig
       @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 emit : ?severity:Diagnostic.severity -> ?loc:Range.t -> ?text:Diagnostic.text -> ?backtrace:Diagnostic.backtrace -> ?extra_remarks:Diagnostic.loctext list -> Message.t -> unit
+  val emit : ?severity:Diagnostic.severity -> ?loc:Range.t -> ?text:Text.t -> ?backtrace:Diagnostic.backtrace -> ?extra_remarks:Loctext.t list -> Message.t -> unit
 
   (** Emit a diagnostic and continue the computation. *)
   val emit_diagnostic : Message.t Diagnostic.t -> unit
@@ -51,7 +51,7 @@ sig
       @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 fatal : ?severity:Diagnostic.severity -> ?loc:Range.t -> ?text:Diagnostic.text -> ?backtrace:Diagnostic.backtrace -> ?extra_remarks:Diagnostic.loctext list -> Message.t -> 'a
+  val fatal : ?severity:Diagnostic.severity -> ?loc:Range.t -> ?text:Text.t -> ?backtrace:Diagnostic.backtrace -> ?extra_remarks:Loctext.t list -> Message.t -> 'a
 
   (** Abort the computation with a diagnostic. *)
   val fatal_diagnostic: Message.t Diagnostic.t -> 'a
@@ -77,7 +77,7 @@ sig
   *)
   val trace : ?loc:Range.t -> string -> (unit -> 'a) -> 'a
 
-  (** [tracef format ... f] formats and records a frame in the backtrace, and runs the thunk [f] with the new backtrace. Note that there should not be any literal control characters. See {!type:Diagnostic.text}.
+  (** [tracef format ... f] formats and records a frame in the backtrace, and runs the thunk [f] with the new backtrace. Note that there should not be any literal control characters. See {!type:Text.t}.
 
       @param loc The location of the text (usually the code) to highlight. Note that a location given here will become the new default location for inner {!val:emit} and {!val:fatal}.
   *)
@@ -87,10 +87,10 @@ sig
 
       @param loc The location of the text (usually the code) to highlight. Note that a location given here will become the new default location for inner {!val:emit} and {!val:fatal}.
   *)
-  val trace_text : ?loc:Range.t -> Diagnostic.text -> (unit -> 'a) -> 'a
+  val trace_text : ?loc:Range.t -> Text.t -> (unit -> 'a) -> 'a
 
   (** [trace_loctext loctext f] records the [loctext] and runs the thunk [f] with the new backtrace. Note that a non-[None] location given here will become the new default location for inner {!val:emit} and {!val:fatal}. *)
-  val trace_loctext : Diagnostic.loctext -> (unit -> 'a) -> 'a
+  val trace_loctext : Loctext.t -> (unit -> 'a) -> 'a
 
   (** {2 Locations} *)
 
@@ -120,7 +120,7 @@ sig
       @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 diagnostic : ?severity:Diagnostic.severity -> ?loc:Range.t -> ?text:Diagnostic.text -> ?backtrace:Diagnostic.backtrace -> ?extra_remarks:Diagnostic.loctext list -> Message.t -> Message.t Diagnostic.t
+  val diagnostic : ?severity:Diagnostic.severity -> ?loc:Range.t -> ?text:Text.t -> ?backtrace:Diagnostic.backtrace -> ?extra_remarks:Loctext.t list -> Message.t -> Message.t Diagnostic.t
 
   (** {2 Algebraic Effects} *)
 
diff --git a/src/Text.ml b/src/Text.ml
new file mode 100644
index 00000000..be36d0c6
--- /dev/null
+++ b/src/Text.ml
@@ -0,0 +1,18 @@
+type t = Format.formatter -> unit
+
+let make s fmt =
+  Format.(pp_print_list ~pp_sep:pp_force_newline pp_print_string) fmt @@
+  String.split_on_char '\n' s
+
+let makef = Format.dprintf
+
+let kmakef = Format.kdprintf
+
+let to_string text : string =
+  let buf = Buffer.create 20 in
+  let fmt = Format.formatter_of_buffer buf in
+  let () = Format.pp_set_geometry fmt ~max_indent:2 ~margin:(Format.pp_infinity-1) in
+  text fmt;
+  Format.pp_print_flush fmt ();
+  Str.global_replace (Str.regexp "\\([\r\n]+ *\\)+") " " @@
+  Buffer.contents buf
diff --git a/src/Text.mli b/src/Text.mli
new file mode 100644
index 00000000..f9422649
--- /dev/null
+++ b/src/Text.mli
@@ -0,0 +1,30 @@
+(** {1 Types} *)
+
+(** 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 t = Format.formatter -> unit
+
+(** {1 Builders} *)
+
+(** [make str] converts the string [str] into a text, converting each ['\n'] into a call to {!val:Format.pp_force_newline}. *)
+val make : string -> t
+
+(** [makef 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 makef : ('a, Format.formatter, unit, t) format4 -> 'a
+
+(** [kmakef kont format ...] is [kont (makef format ...)]. It is an alias of {!val:Format.kdprintf}. *)
+val kmakef : (t -> 'b) -> ('a, Format.formatter, unit, 'b) format4 -> 'a
+
+(** {1 Helper Functions} *)
+
+(** 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 to_string : t -> string
diff --git a/src/tty/Tty.ml b/src/tty/Tty.ml
index e77a603c..27ecd93c 100644
--- a/src/tty/Tty.ml
+++ b/src/tty/Tty.ml
@@ -166,7 +166,7 @@ struct
     in
     String.length @@ Int.to_string @@ max_line_number explication
 
-  let render_textloc ~param ~severity ~extra_remarks fmt (textloc : Diagnostic.loctext) =
+  let render_textloc ~param ~severity ~extra_remarks fmt (textloc : Loctext.t) =
     let located_tags, unlocated_tags =
       let main = TtyTag.Main, textloc in
       let extra_remarks = List.mapi (fun i r -> TtyTag.Extra i, r) (Bwd.to_list extra_remarks) in
diff --git a/src/tty/TtyTag.ml b/src/tty/TtyTag.ml
index 0d1df0fa..def310bd 100644
--- a/src/tty/TtyTag.ml
+++ b/src/tty/TtyTag.ml
@@ -1,5 +1,5 @@
 type index = Main | Extra of int
-type t = index * Diagnostic.text
+type t = index * Text.t
 let equal (x : t) y = fst x = fst y
 let priority =
   function
diff --git a/test/TestDiagnostic.ml b/test/TestDiagnostic.ml
deleted file mode 100644
index 170b4522..00000000
--- a/test/TestDiagnostic.ml
+++ /dev/null
@@ -1,13 +0,0 @@
-let of_test name input expected =
-  Alcotest.test_case name `Quick @@ fun () ->
-  Alcotest.(check string) "Output matched" expected @@
-  Asai.Diagnostic.string_of_text input
-
-let () =
-  Alcotest.run "UserContent" [
-    "string_of_text",
-    [
-      of_test "\\n" (Asai.Diagnostic.text " \r   e \n  f  \n   g   ") "  e  f   g   ";
-      of_test "\\n" (Asai.Diagnostic.textf "@[<v>123@[456@]789@]") "123 456789";
-    ]
-  ]
diff --git a/test/TestText.ml b/test/TestText.ml
new file mode 100644
index 00000000..8756eb77
--- /dev/null
+++ b/test/TestText.ml
@@ -0,0 +1,13 @@
+let of_test name input expected =
+  Alcotest.test_case name `Quick @@ fun () ->
+  Alcotest.(check string) "Output matched" expected @@
+  Asai.Text.to_string input
+
+let () =
+  Alcotest.run "UserContent" [
+    "Text.to_string",
+    [
+      of_test "\\n" (Asai.Text.make " \r   e \n  f  \n   g   ") "  e  f   g   ";
+      of_test "\\n" (Asai.Text.makef "@[<v>123@[456@]789@]") "123 456789";
+    ]
+  ]
diff --git a/test/TestTty.ml b/test/TestTty.ml
index 1071a80f..72e99f15 100644
--- a/test/TestTty.ml
+++ b/test/TestTty.ml
@@ -69,19 +69,19 @@ let exec handler =
 
   Reporter.emit ~loc:(Range.make (~@ s1 2 3, ~@ s1 2 7)) Hello "this is the main message"
     ~extra_remarks:[
-      Diagnostic.loctext "message 1";
-      Diagnostic.loctext ~loc:(Range.make (~@ s2 1 3, ~@ s2 3 4)) "message 2";
-      Diagnostic.loctext "message 3";
-      Diagnostic.loctext ~loc:(Range.make (~@ s1 3 4, ~@ s1 3 5)) "message 4";
-      Diagnostic.loctext ~loc:(Range.make (~@ s1 2 8, ~@ s1 2 9)) "message 5";
-      Diagnostic.loctext ~loc:(Range.make (~@ s1 1 3, ~@ s1 2 1)) "message 6";
-      Diagnostic.loctext ~loc:(Range.make (~@ s2 1 3, ~@ s2 2 1)) "message 7";
-      Diagnostic.loctext ~loc:(Range.make (~@ s2 10 0, ~@ s2 10 0)) "message 8";
+      Loctext.make "message 1";
+      Loctext.make ~loc:(Range.make (~@ s2 1 3, ~@ s2 3 4)) "message 2";
+      Loctext.make "message 3";
+      Loctext.make ~loc:(Range.make (~@ s1 3 4, ~@ s1 3 5)) "message 4";
+      Loctext.make ~loc:(Range.make (~@ s1 2 8, ~@ s1 2 9)) "message 5";
+      Loctext.make ~loc:(Range.make (~@ s1 1 3, ~@ s1 2 1)) "message 6";
+      Loctext.make ~loc:(Range.make (~@ s2 1 3, ~@ s2 2 1)) "message 7";
+      Loctext.make ~loc:(Range.make (~@ s2 10 0, ~@ s2 10 0)) "message 8";
     ];
 
   Reporter.emit ~loc:(Range.eof (~@ s1 23 width)) Hello "this is the main message"
     ~extra_remarks:[
-      Diagnostic.loctext ~loc:(Range.eof (~@ s2 23 width)) "ending of another file";
+      Loctext.make ~loc:(Range.eof (~@ s2 23 width)) "ending of another file";
     ]
 
 let () =
diff --git a/test/dune b/test/dune
index 5e8acd9f..16dd101e 100644
--- a/test/dune
+++ b/test/dune
@@ -4,8 +4,8 @@
  (libraries asai alcotest))
 
 (tests
- (names TestUserContent TestDiagnostic)
- (modules TestUserContent TestDiagnostic)
+ (names TestUserContent TestText)
+ (modules TestUserContent TestText)
  (libraries asai alcotest))
 
 (test