src/HOL/Tools/res_clause.ML
changeset 24183 a46b758941a4
parent 23881 851c74f1bb69
child 24310 af4af9993922
equal deleted inserted replaced
24182:a39c5e7de6a7 24183:a46b758941a4
   121 
   121 
   122 (*Escaping of special characters.
   122 (*Escaping of special characters.
   123   Alphanumeric characters are left unchanged.
   123   Alphanumeric characters are left unchanged.
   124   The character _ goes to __
   124   The character _ goes to __
   125   Characters in the range ASCII space to / go to _A to _P, respectively.
   125   Characters in the range ASCII space to / go to _A to _P, respectively.
   126   Other printing characters go to _NNN where NNN is the decimal ASCII code.*)
   126   Other printing characters go to _nnn where nnn is the decimal ASCII code.*)
   127 local
       
   128 
       
   129 val A_minus_space = Char.ord #"A" - Char.ord #" ";
   127 val A_minus_space = Char.ord #"A" - Char.ord #" ";
       
   128 
       
   129 fun stringN_of_int 0 _ = ""
       
   130   | stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10);
   130 
   131 
   131 fun ascii_of_c c =
   132 fun ascii_of_c c =
   132   if Char.isAlphaNum c then String.str c
   133   if Char.isAlphaNum c then String.str c
   133   else if c = #"_" then "__"
   134   else if c = #"_" then "__"
   134   else if #" " <= c andalso c <= #"/" 
   135   else if #" " <= c andalso c <= #"/" 
   135        then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
   136        then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
   136   else if Char.isPrint c then ("_" ^ Int.toString (Char.ord c))
   137   else if Char.isPrint c 
       
   138        then ("_" ^ stringN_of_int 3 (Char.ord c))  (*fixed width, in case more digits follow*)
   137   else ""
   139   else ""
   138 
   140 
   139 in
       
   140 
       
   141 val ascii_of = String.translate ascii_of_c;
   141 val ascii_of = String.translate ascii_of_c;
   142 
   142 
   143 end;
   143 (** Remove ASCII armouring from names in proof files **)
       
   144 
       
   145 (*We don't raise error exceptions because this code can run inside the watcher.
       
   146   Also, the errors are "impossible" (hah!)*)
       
   147 fun undo_ascii_aux rcs [] = String.implode(rev rcs)
       
   148   | undo_ascii_aux rcs [#"_"] = undo_ascii_aux (#"_"::rcs) []  (*ERROR*)
       
   149       (*Three types of _ escapes: __, _A to _P, _nnn*)
       
   150   | undo_ascii_aux rcs (#"_" :: #"_" :: cs) = undo_ascii_aux (#"_"::rcs) cs
       
   151   | undo_ascii_aux rcs (#"_" :: c :: cs) = 
       
   152       if #"A" <= c andalso c<= #"P"  (*translation of #" " to #"/"*)
       
   153       then undo_ascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
       
   154       else 
       
   155         let val digits = List.take (c::cs, 3) handle Subscript => []
       
   156         in  
       
   157             case Int.fromString (String.implode digits) of
       
   158                 NONE => undo_ascii_aux (c:: #"_"::rcs) cs  (*ERROR*)
       
   159               | SOME n => undo_ascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
       
   160         end
       
   161   | undo_ascii_aux rcs (c::cs) = undo_ascii_aux (c::rcs) cs;
       
   162 
       
   163 val undo_ascii_of = undo_ascii_aux [] o String.explode;
   144 
   164 
   145 (* convert a list of strings into one single string; surrounded by brackets *)
   165 (* convert a list of strings into one single string; surrounded by brackets *)
   146 fun paren_pack [] = ""   (*empty argument list*)
   166 fun paren_pack [] = ""   (*empty argument list*)
   147   | paren_pack strings = "(" ^ commas strings ^ ")";
   167   | paren_pack strings = "(" ^ commas strings ^ ")";
   148 
   168