1.1 --- a/NEWS	Tue Apr 08 11:59:25 2008 +0200
     1.2 +++ b/NEWS	Tue Apr 08 15:47:05 2008 +0200
     1.3 @@ -223,8 +223,12 @@
     1.4  
     1.5  *** System ***
     1.6  
     1.7 -* System: removed obsolete THIS_IS_ISABELLE_BUILD feature.  NB: the
     1.8 -documented way of changing the user's settings is via
     1.9 +* YXML notation provides a simple and efficient alternative to
    1.10 +standard XML transfer syntax.  See src/Pure/General/yxml.ML and
    1.11 +isatool yxml as described in the Isabelle system manual.
    1.12 +
    1.13 +* Removed obsolete THIS_IS_ISABELLE_BUILD feature.  NB: the documented
    1.14 +way of changing the user's settings is via
    1.15  ISABELLE_HOME_USER/etc/settings, which is a fully featured bash
    1.16  script.
    1.17  

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/lib/Tools/yxml	Tue Apr 08 15:47:05 2008 +0200
     2.3 @@ -0,0 +1,35 @@
     2.4 +#!/usr/bin/env bash
     2.5 +#
     2.6 +# $Id$
     2.7 +# Author: Makarius
     2.8 +#
     2.9 +# DESCRIPTION: simple XML to YXML converter
    2.10 +
    2.11 +
    2.12 +PRG="$(basename "$0")"
    2.13 +
    2.14 +function usage()
    2.15 +{
    2.16 +  echo
    2.17 +  echo "Usage: $PRG"
    2.18 +  echo
    2.19 +  echo "  Convert XML (stdin) to YXML (stdout)."
    2.20 +  echo
    2.21 +  exit 1
    2.22 +}
    2.23 +
    2.24 +function fail()
    2.25 +{
    2.26 +  echo "$1" >&2
    2.27 +  exit 2
    2.28 +}
    2.29 +
    2.30 +
    2.31 +## process command line
    2.32 +
    2.33 +[ "$#" -ne 0 ] && usage
    2.34 +
    2.35 +
    2.36 +## main
    2.37 +
    2.38 +exec perl -w "$ISABELLE_HOME/lib/scripts/yxml.pl"

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/lib/scripts/yxml.pl	Tue Apr 08 15:47:05 2008 +0200
     3.3 @@ -0,0 +1,36 @@
     3.4 +#
     3.5 +# $Id$
     3.6 +# Author: Makarius
     3.7 +#
     3.8 +# yxml.pl - simple XML to YXML converter
     3.9 +#
    3.10 +
    3.11 +use strict;
    3.12 +use XML::Parser;
    3.13 +
    3.14 +binmode(STDOUT, ":utf8");
    3.15 +
    3.16 +sub handle_start {
    3.17 +  print chr(5), chr(6), $_[1];
    3.18 +  for (my $i = 2; $i <= $#_; $i++) {
    3.19 +    print ($i % 2 == 0 ? chr(6) : "=");
    3.20 +    print $_[$i];
    3.21 +  }
    3.22 +  print chr(5);
    3.23 +}
    3.24 +
    3.25 +sub handle_end {
    3.26 +  print chr(5), chr(6), chr(5);
    3.27 +}
    3.28 +
    3.29 +sub handle_char {
    3.30 +  print $_[1];
    3.31 +}
    3.32 +
    3.33 +my $parser = new XML::Parser(Handlers =>
    3.34 +  {Start => \&handle_start,
    3.35 +    End => \&handle_end,
    3.36 +    Char => \&handle_char});
    3.37 +
    3.38 +$parser->parse(*STDIN);
    3.39 +