--- a/NEWS Tue Apr 08 11:59:25 2008 +0200
+++ b/NEWS Tue Apr 08 15:47:05 2008 +0200
@@ -223,8 +223,12 @@
*** System ***
-* System: removed obsolete THIS_IS_ISABELLE_BUILD feature. NB: the
-documented way of changing the user's settings is via
+* YXML notation provides a simple and efficient alternative to
+standard XML transfer syntax. See src/Pure/General/yxml.ML and
+isatool yxml as described in the Isabelle system manual.
+
+* Removed obsolete THIS_IS_ISABELLE_BUILD feature. NB: the documented
+way of changing the user's settings is via
ISABELLE_HOME_USER/etc/settings, which is a fully featured bash
script.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/yxml Tue Apr 08 15:47:05 2008 +0200
@@ -0,0 +1,35 @@
+#!/usr/bin/env bash
+#
+# $Id$
+# Author: Makarius
+#
+# DESCRIPTION: simple XML to YXML converter
+
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+ echo
+ echo "Usage: $PRG"
+ echo
+ echo " Convert XML (stdin) to YXML (stdout)."
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+
+## process command line
+
+[ "$#" -ne 0 ] && usage
+
+
+## main
+
+exec perl -w "$ISABELLE_HOME/lib/scripts/yxml.pl"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/yxml.pl Tue Apr 08 15:47:05 2008 +0200
@@ -0,0 +1,36 @@
+#
+# $Id$
+# Author: Makarius
+#
+# yxml.pl - simple XML to YXML converter
+#
+
+use strict;
+use XML::Parser;
+
+binmode(STDOUT, ":utf8");
+
+sub handle_start {
+ print chr(5), chr(6), $_[1];
+ for (my $i = 2; $i <= $#_; $i++) {
+ print ($i % 2 == 0 ? chr(6) : "=");
+ print $_[$i];
+ }
+ print chr(5);
+}
+
+sub handle_end {
+ print chr(5), chr(6), chr(5);
+}
+
+sub handle_char {
+ print $_[1];
+}
+
+my $parser = new XML::Parser(Handlers =>
+ {Start => \&handle_start,
+ End => \&handle_end,
+ Char => \&handle_char});
+
+$parser->parse(*STDIN);
+