# HG changeset patch
# User wenzelm
# Date 1207662425 -7200
# Node ID 042617a1c86cdd58e98330455ed2cce39ef4ae8a
# Parent  560d07845442b925c4b0cb4429cc0e2206c4cc32
support for YXML notation -- XML done right;

diff -r 560d07845442 -r 042617a1c86c NEWS
--- 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.
 
diff -r 560d07845442 -r 042617a1c86c lib/Tools/yxml
--- /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"
diff -r 560d07845442 -r 042617a1c86c 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);
+