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
Fri, 08 May 2015 10:19:44 +0200
changeset 60274 c2837a39da01
parent 52835 0906c00bb21d
child 62506 860cd901ab43
permissions -rw-r--r--
more conservative Document_Model.init: avoid Document.Node.Clear due to change of token marker (e.g. due to change of jEdit mode properties); clarified Isabelle.buffer_token_marker;
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