--- a/src/HOL/TPTP/TPTP_Parser/tptp_problem_name.ML Tue Sep 03 22:30:52 2013 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_problem_name.ML Tue Sep 03 21:46:40 2013 +0100
@@ -122,6 +122,20 @@
end
end
+(*Restricts the character set used in a string*)
+fun restricted_ascii only_exclude =
+ let
+ fun restrict x = "_" ^ Int.toString (Char.ord x)
+ fun restrict_uniform x =
+ if member (op =) (numerics @ alphabetics) x then Char.toString x else restrict x
+ fun restrict_specific x =
+ if member (op =) only_exclude x then restrict x else Char.toString x
+ val restrict_ascii =
+ if List.null only_exclude
+ then map restrict_uniform
+ else map restrict_specific
+ in String.explode #> restrict_ascii #> implode end;
+
(*Produces an ASCII encoding of a TPTP problem-file name.*)
fun mangle_problem_name (prob : problem_name) : string =
case prob of
@@ -148,6 +162,6 @@
prob_form ^
suffix
end
- | Nonstandard str => str
+ | Nonstandard str => restricted_ascii [] str
end