diff options
| author | Alasdair | 2019-04-05 00:19:52 +0100 |
|---|---|---|
| committer | Alasdair | 2019-04-05 00:19:52 +0100 |
| commit | d3db47ec529df0c552055024e727f9f34ffe95e9 (patch) | |
| tree | 3122134d898c76c6f2469ce60ba8c3929687c143 /src/reporting.ml | |
| parent | 8dca40d218b5fbc0956b29887d9c1065b1c1757f (diff) | |
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.
Diffstat (limited to 'src/reporting.ml')
| -rw-r--r-- | src/reporting.ml | 14 |
1 files changed, 14 insertions, 0 deletions
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 |