Lem: Make generated assertion messages look nicer in prover output

Add a new short_loc_to_string function that produces just the file and line number as
a single line. loc_to_string adds a bunch of terminal color codes and other formatting
designed for producing pretty error-messages in the terminal, which isn't ideal when
the string appears in prover output as part of an assert statement. This is should be
purely an aesthetic change.

1 files changed, 6 insertions, 0 deletions

diff --git a/src/reporting.mli b/src/reporting.mli
index 2d886111..86399e84 100644
--- a/src/reporting.mli
+++ b/src/reporting.mli
@@ -65,6 +65,12 @@
 (** [loc_to_string] includes code from file if code optional argument is true (default) *)
 val loc_to_string : ?code:bool -> Parse_ast.l -> string
 
+(** Reduce a location to a pair of positions if possible *)
+val simp_loc : Ast.l -> (Lexing.position * Lexing.position) option
+
+(** [short_loc_to_string] prints the location as a single line in a simple format *)
+val short_loc_to_string : Parse_ast.l -> string
+  
 (** [print_err fatal print_loc_source l head mes] prints an error / warning message to
     std-err. It starts with printing location information stored in [l]
     It then prints "head: mes". If [fatal] is set, the program exists with error-code 1 afterwards.