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
Thu, 03 Mar 2016 21:30:31 +0100
changeset 62506 860cd901ab43
parent 52835 0906c00bb21d
permissions -rw-r--r--
clarified isabelle_process;
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;








62506






860cd901ab43
clarified isabelle_process;



wenzelm


parents: 
52835

diff
changeset




    10


  print $_;








52835






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



wenzelm


parents: 

diff
changeset




    11


}















isabelle