# HG changeset patch
# User sultana
# Date 1378241200 -3600
# Node ID 63034189f9ecbac7644612e74620ec8e1d698720
# Parent  e93772b451ef595c21e339e133b4a4a5aec161af
improved handling of nonstandard problem names;

diff -r e93772b451ef -r 63034189f9ec src/HOL/TPTP/TPTP_Parser/tptp_problem_name.ML
--- 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