Code to undo the function ascii_of
authorpaulson
Wed Aug 08 14:00:09 2007 +0200 (2007-08-08)
changeset 24183a46b758941a4
parent 24182 a39c5e7de6a7
child 24184 19cb051154fd
Code to undo the function ascii_of
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/Tools/res_clause.ML	Wed Aug 08 13:59:46 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Aug 08 14:00:09 2007 +0200
     1.3 @@ -123,24 +123,44 @@
     1.4    Alphanumeric characters are left unchanged.
     1.5    The character _ goes to __
     1.6    Characters in the range ASCII space to / go to _A to _P, respectively.
     1.7 -  Other printing characters go to _NNN where NNN is the decimal ASCII code.*)
     1.8 -local
     1.9 +  Other printing characters go to _nnn where nnn is the decimal ASCII code.*)
    1.10 +val A_minus_space = Char.ord #"A" - Char.ord #" ";
    1.11  
    1.12 -val A_minus_space = Char.ord #"A" - Char.ord #" ";
    1.13 +fun stringN_of_int 0 _ = ""
    1.14 +  | stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10);
    1.15  
    1.16  fun ascii_of_c c =
    1.17    if Char.isAlphaNum c then String.str c
    1.18    else if c = #"_" then "__"
    1.19    else if #" " <= c andalso c <= #"/" 
    1.20         then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
    1.21 -  else if Char.isPrint c then ("_" ^ Int.toString (Char.ord c))
    1.22 +  else if Char.isPrint c 
    1.23 +       then ("_" ^ stringN_of_int 3 (Char.ord c))  (*fixed width, in case more digits follow*)
    1.24    else ""
    1.25  
    1.26 -in
    1.27 -
    1.28  val ascii_of = String.translate ascii_of_c;
    1.29  
    1.30 -end;
    1.31 +(** Remove ASCII armouring from names in proof files **)
    1.32 +
    1.33 +(*We don't raise error exceptions because this code can run inside the watcher.
    1.34 +  Also, the errors are "impossible" (hah!)*)
    1.35 +fun undo_ascii_aux rcs [] = String.implode(rev rcs)
    1.36 +  | undo_ascii_aux rcs [#"_"] = undo_ascii_aux (#"_"::rcs) []  (*ERROR*)
    1.37 +      (*Three types of _ escapes: __, _A to _P, _nnn*)
    1.38 +  | undo_ascii_aux rcs (#"_" :: #"_" :: cs) = undo_ascii_aux (#"_"::rcs) cs
    1.39 +  | undo_ascii_aux rcs (#"_" :: c :: cs) = 
    1.40 +      if #"A" <= c andalso c<= #"P"  (*translation of #" " to #"/"*)
    1.41 +      then undo_ascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
    1.42 +      else 
    1.43 +        let val digits = List.take (c::cs, 3) handle Subscript => []
    1.44 +        in  
    1.45 +            case Int.fromString (String.implode digits) of
    1.46 +                NONE => undo_ascii_aux (c:: #"_"::rcs) cs  (*ERROR*)
    1.47 +              | SOME n => undo_ascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
    1.48 +        end
    1.49 +  | undo_ascii_aux rcs (c::cs) = undo_ascii_aux (c::rcs) cs;
    1.50 +
    1.51 +val undo_ascii_of = undo_ascii_aux [] o String.explode;
    1.52  
    1.53  (* convert a list of strings into one single string; surrounded by brackets *)
    1.54  fun paren_pack [] = ""   (*empty argument list*)