Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
lib/scripts/recode.pl
author wenzelm
Mon, 16 Sep 2013 12:37:54 +0200
changeset 53657 64942a1f7187
parent 52835 0906c00bb21d
child 62506 860cd901ab43
permissions -rw-r--r--
prefer high-level ML_System.share_common_data, ML_System.save_state -- except for bootstrap images (RAW, Pure);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
52835
0906c00bb21d recode utf8 for ML, as done in feeder.pl;
wenzelm
parents:
diff changeset 
     1
 
#
0906c00bb21d recode utf8 for ML, as done in feeder.pl;
wenzelm
parents:
diff changeset 
     2
 
# Author: Makarius
0906c00bb21d recode utf8 for ML, as done in feeder.pl;
wenzelm
parents:
diff changeset 
     3
 
#
0906c00bb21d recode utf8 for ML, as done in feeder.pl;
wenzelm
parents:
diff changeset 
     4
 
# recode.pl - recode utf8 for ML
0906c00bb21d recode utf8 for ML, as done in feeder.pl;
wenzelm
parents:
diff changeset 
     5
 
#
0906c00bb21d recode utf8 for ML, as done in feeder.pl;
wenzelm
parents:
diff changeset 
     6
 












0906c00bb21d
recode utf8 for ML, as done in feeder.pl;



wenzelm


parents: 

diff
changeset




     7


for (@ARGV) {













0906c00bb21d
recode utf8 for ML, as done in feeder.pl;



wenzelm


parents: 

diff
changeset




     8


  utf8::upgrade($_);













0906c00bb21d
recode utf8 for ML, as done in feeder.pl;



wenzelm


parents: 

diff
changeset




     9


  s/([\x80-\xff])/\\${\(ord($1))}/g;













0906c00bb21d
recode utf8 for ML, as done in feeder.pl;



wenzelm


parents: 

diff
changeset




    10


  print $_, " ";













0906c00bb21d
recode utf8 for ML, as done in feeder.pl;



wenzelm


parents: 

diff
changeset




    11


}













0906c00bb21d
recode utf8 for ML, as done in feeder.pl;



wenzelm


parents: 

diff
changeset




    12
















isabelle