From d3db47ec529df0c552055024e727f9f34ffe95e9 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Fri, 5 Apr 2019 00:19:52 +0100
Subject: 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.
---
 src/reporting.ml | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'src/reporting.ml')

diff --git a/src/reporting.ml b/src/reporting.ml
index 0bc73ed6..20e44c57 100644
--- a/src/reporting.ml
+++ b/src/reporting.ml
@@ -111,6 +111,20 @@ let loc_to_string ?code:(code=true) l =
   format_message (Location (l, Line "")) (buffer_formatter b);
   Buffer.contents b
 
+let rec simp_loc = function
+  | Parse_ast.Unknown -> None
+  | Parse_ast.Unique (_, l) -> simp_loc l
+  | Parse_ast.Generated l -> simp_loc l
+  | Parse_ast.Range (p1, p2) -> Some (p1, p2)
+  | Parse_ast.Documented (_, l) -> simp_loc l
+  
+let short_loc_to_string l =
+  match simp_loc l with
+  | None -> "unknown location"
+  | Some (p1, p2) ->
+     Printf.sprintf "%s %d:%d - %d:%d"
+       p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) p2.pos_lnum (p2.pos_cnum - p2.pos_bol)
+  
 let print_err l m1 m2 =
   print_err_internal (Loc l) m1 m2
 
-- 
cgit v1.2.3