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, 27 Feb 2014 12:37:43 +0100
changeset 55781 b3a4207fb9a6
parent 52835 0906c00bb21d
child 62506 860cd901ab43
permissions -rw-r--r--
proper update of text perspective for nodes with changed blobs, which is important to refresh the corresponding command perspective (otherwise it might refer to invalid thy_load commands and cause full execution of the node by the prover);
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