lib/scripts/yxml
author wenzelm
Thu Nov 13 23:45:15 2014 +0100 (2014-11-13)
changeset 58999 ed09ae4ea2d8
parent 35022 c844b93dd147
permissions -rwxr-xr-x
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 #!/usr/bin/env perl
     2 #
     3 # Author: Makarius
     4 #
     5 # yxml.pl - simple XML to YXML converter
     6 #
     7 
     8 use warnings;
     9 use strict;
    10 
    11 use XML::Parser;
    12 
    13 binmode(STDOUT, ":utf8");
    14 
    15 sub handle_start {
    16   print chr(5), chr(6), $_[1];
    17   for (my $i = 2; $i <= $#_; $i++) {
    18     print ($i % 2 == 0 ? chr(6) : "=");
    19     print $_[$i];
    20   }
    21   print chr(5);
    22 }
    23 
    24 sub handle_end {
    25   print chr(5), chr(6), chr(5);
    26 }
    27 
    28 sub handle_char {
    29   print $_[1];
    30 }
    31 
    32 my $parser = new XML::Parser(Handlers =>
    33   {Start => \&handle_start,
    34     End => \&handle_end,
    35     Char => \&handle_char});
    36 
    37 $parser->parse(*STDIN) or die $!;