lib/scripts/recode.pl
author wenzelm
Thu Nov 13 23:45:15 2014 +0100 (2014-11-13)
changeset 58999 ed09ae4ea2d8
parent 52835 0906c00bb21d
child 62506 860cd901ab43
permissions -rw-r--r--
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
discontinued obsolete 'txt_raw' (superseded by 'text_raw');
eliminated obsolete Outer_Syntax.markup (superseded by keyword kinds);
'text' and 'txt' no longer appear in Sidekick tree due to change of keyword kind;
changed tagging of diagnostic commands within proof;
     1 #
     2 # Author: Makarius
     3 #
     4 # recode.pl - recode utf8 for ML
     5 #
     6 
     7 for (@ARGV) {
     8   utf8::upgrade($_);
     9   s/([\x80-\xff])/\\${\(ord($1))}/g;
    10   print $_, " ";
    11 }
    12