From 9d33336846d9aed507ecec907dd7226951cdf9b0 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 17 Oct 2022 09:57:06 -0400 Subject: [PATCH] wip: try to fix escaping of identifiers in TPTP output (#93) --- src/core/Util.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/core/Util.ml b/src/core/Util.ml index 23a4a795e..c27568e27 100644 --- a/src/core/Util.ml +++ b/src/core/Util.ml @@ -281,7 +281,12 @@ let pp_list0 ?(sep=" ") pp_x out = function let tstp_needs_escaping s = assert (s<>""); s.[0] = '_' || - CCString.exists (function ' ' | '#' | '$' | '+' | '-' | '/' -> true | _ -> false) s + CCString.exists + (function + | ' ' | '#' | '$' | '+' | '-' | '/' | '\n' + | '\t' | '\r' | '<' | '>' -> true + | _ -> false) + s let pp_str_tstp out s = CCFormat.string out (if tstp_needs_escaping s then "'" ^ String.escaped s ^ "'" else s)