Fixing the code to undo the function ascii_of
authorpaulson
Wed Aug 08 13:59:46 2007 +0200 (2007-08-08)
changeset 24182a39c5e7de6a7
parent 24181 102ebceaa495
child 24183 a46b758941a4
Fixing the code to undo the function ascii_of
src/HOL/Tools/res_reconstruct.ML
     1.1 --- a/src/HOL/Tools/res_reconstruct.ML	Wed Aug 08 13:14:31 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Wed Aug 08 13:59:46 2007 +0200
     1.3 @@ -91,64 +91,14 @@
     1.4                  clause -- Scan.option annotations --| $$ ")";
     1.5  
     1.6  
     1.7 -(**** DUPLICATE of Susanto's code to remove ASCII armouring from names in proof files ****)
     1.8 -
     1.9 -(*original file: Isabelle_ext.sml*)
    1.10 -
    1.11 -val A_min_spc = Char.ord #"A" - Char.ord #" ";
    1.12 -
    1.13 -fun cList2int chs = getOpt (Int.fromString (String.implode (rev chs)), 0);
    1.14 -
    1.15 -(*why such a tiny range?*)
    1.16 -fun check_valid_int x =
    1.17 -  let val val_x = cList2int x
    1.18 -  in (length x = 3) andalso (val_x >= 123) andalso (val_x <= 126)
    1.19 -  end;
    1.20 -
    1.21 -fun normalise_s s [] st_ sti =
    1.22 -      String.implode(rev(
    1.23 -        if st_
    1.24 -        then if null sti
    1.25 -             then (#"_" :: s)
    1.26 -             else if check_valid_int sti
    1.27 -                  then (Char.chr (cList2int sti) :: s)
    1.28 -                  else (sti @ (#"_" :: s))
    1.29 -        else s))
    1.30 -  | normalise_s s (#"_"::cs) st_ sti =
    1.31 -      if st_
    1.32 -      then let val s' = if null sti
    1.33 -                        then (#"_"::s)
    1.34 -                        else if check_valid_int sti
    1.35 -                             then (Char.chr (cList2int sti) :: s)
    1.36 -                             else (sti @ (#"_" :: s))
    1.37 -           in normalise_s s' cs false []
    1.38 -           end
    1.39 -      else normalise_s s cs true []
    1.40 -  | normalise_s s (c::cs) true sti =
    1.41 -      if (Char.isDigit c)
    1.42 -      then normalise_s s cs true (c::sti)
    1.43 -      else let val s' = if null sti
    1.44 -                        then if ((c >= #"A") andalso (c<= #"P"))
    1.45 -                             then ((Char.chr(Char.ord c - A_min_spc))::s)
    1.46 -                             else (c :: (#"_" :: s))
    1.47 -                        else if check_valid_int sti
    1.48 -                             then (Char.chr (cList2int sti) :: s)
    1.49 -                             else (sti @ (#"_" :: s))
    1.50 -           in normalise_s s' cs false []
    1.51 -           end
    1.52 -  | normalise_s s (c::cs) _ _ = normalise_s (c::s) cs false [];
    1.53 -
    1.54 -(*This version does not look for standard prefixes first.*)
    1.55 -fun normalise_string s = normalise_s [] (String.explode s) false [];
    1.56 -
    1.57 -
    1.58  (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
    1.59  
    1.60  exception STREE of stree;
    1.61  
    1.62  (*If string s has the prefix s1, return the result of deleting it.*)
    1.63  fun strip_prefix s1 s =
    1.64 -  if String.isPrefix s1 s then SOME (normalise_string (String.extract (s, size s1, NONE)))
    1.65 +  if String.isPrefix s1 s 
    1.66 +  then SOME (ResClause.undo_ascii_of (String.extract (s, size s1, NONE)))
    1.67    else NONE;
    1.68  
    1.69  (*Invert the table of translations between Isabelle and ATPs*)