# HG changeset patch
# User wenzelm
# Date 1456670636 -3600
# Node ID 040b94ffbddebeac3d268d22d3a18a5015c94914
# Parent  2154f709fc25861f059d493ee77c46742bd80b28
removed pointless "isabelle yxml";

diff -r 2154f709fc25 -r 040b94ffbdde NEWS
--- a/NEWS	Sun Feb 28 15:34:50 2016 +0100
+++ b/NEWS	Sun Feb 28 15:43:56 2016 +0100
@@ -182,6 +182,10 @@
 executables are found within the PATH: isabelle, isabelle_process,
 isabelle_scala_script.
 
+* The somewhat pointless command-line tool "isabelle yxml" has been
+discontinued. INCOMPATIBILITY, use operations from the modules "XML" and
+"YXML" in Isabelle/ML or Isabelle/Scala.
+
 * SML/NJ is no longer supported.
 
 
diff -r 2154f709fc25 -r 040b94ffbdde lib/Tools/yxml
--- a/lib/Tools/yxml	Sun Feb 28 15:34:50 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: simple XML to YXML converter
-
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: isabelle $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 "$ISABELLE_HOME/lib/scripts/yxml"
diff -r 2154f709fc25 -r 040b94ffbdde lib/scripts/yxml
--- a/lib/scripts/yxml	Sun Feb 28 15:34:50 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-#!/usr/bin/env perl
-#
-# Author: Makarius
-#
-# yxml.pl - simple XML to YXML converter
-#
-
-use warnings;
-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) or die $!;
diff -r 2154f709fc25 -r 040b94ffbdde src/Doc/System/Basics.thy
--- a/src/Doc/System/Basics.thy	Sun Feb 28 15:34:50 2016 +0100
+++ b/src/Doc/System/Basics.thy	Sun Feb 28 15:43:56 2016 +0100
@@ -447,4 +447,41 @@
   @{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>}
 \<close>
 
+
+section \<open>YXML versus XML\<close>
+
+text \<open>
+  Isabelle tools often use YXML, which is a simple and efficient syntax for
+  untyped XML trees. The YXML format is defined as follows.
+
+    \<^enum> The encoding is always UTF-8.
+
+    \<^enum> Body text is represented verbatim (no escaping, no special treatment of
+    white space, no named entities, no CDATA chunks, no comments).
+
+    \<^enum> Markup elements are represented via ASCII control characters \<open>\<^bold>X = 5\<close>
+    and \<open>\<^bold>Y = 6\<close> as follows:
+
+    \begin{tabular}{ll}
+      XML & YXML \\\hline
+      \<^verbatim>\<open><\<close>\<open>name attribute\<close>\<^verbatim>\<open>=\<close>\<open>value \<dots>\<close>\<^verbatim>\<open>>\<close> &
+      \<open>\<^bold>X\<^bold>Yname\<^bold>Yattribute\<close>\<^verbatim>\<open>=\<close>\<open>value\<dots>\<^bold>X\<close> \\
+      \<^verbatim>\<open></\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> & \<open>\<^bold>X\<^bold>Y\<^bold>X\<close> \\
+    \end{tabular}
+
+    There is no special case for empty body text, i.e.\ \<^verbatim>\<open><foo/>\<close> is treated
+    like \<^verbatim>\<open><foo></foo>\<close>. Also note that \<open>\<^bold>X\<close> and \<open>\<^bold>Y\<close> may never occur in
+    well-formed XML documents.
+
+  Parsing YXML is pretty straight-forward: split the text into chunks
+  separated by \<open>\<^bold>X\<close>, then split each chunk into sub-chunks separated by \<open>\<^bold>Y\<close>.
+  Markup chunks start with an empty sub-chunk, and a second empty sub-chunk
+  indicates close of an element. Any other non-empty chunk consists of plain
+  text. For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or @{file
+  "~~/src/Pure/PIDE/yxml.scala"}.
+
+  YXML documents may be detected quickly by checking that the first two
+  characters are \<open>\<^bold>X\<^bold>Y\<close>.
+\<close>
+
 end
\ No newline at end of file
diff -r 2154f709fc25 -r 040b94ffbdde src/Doc/System/Misc.thy
--- a/src/Doc/System/Misc.thy	Sun Feb 28 15:34:50 2016 +0100
+++ b/src/Doc/System/Misc.thy	Sun Feb 28 15:43:56 2016 +0100
@@ -265,42 +265,4 @@
   id of the @{setting ISABELLE_HOME} directory.
 \<close>
 
-
-section \<open>Convert XML to YXML\<close>
-
-text \<open>
-  The @{tool_def yxml} tool converts a standard XML document (stdin) to the
-  much simpler and more efficient YXML format of Isabelle (stdout). The YXML
-  format is defined as follows.
-
-    \<^enum> The encoding is always UTF-8.
-
-    \<^enum> Body text is represented verbatim (no escaping, no special treatment of
-    white space, no named entities, no CDATA chunks, no comments).
-
-    \<^enum> Markup elements are represented via ASCII control characters \<open>\<^bold>X = 5\<close>
-    and \<open>\<^bold>Y = 6\<close> as follows:
-
-    \begin{tabular}{ll}
-      XML & YXML \\\hline
-      \<^verbatim>\<open><\<close>\<open>name attribute\<close>\<^verbatim>\<open>=\<close>\<open>value \<dots>\<close>\<^verbatim>\<open>>\<close> &
-      \<open>\<^bold>X\<^bold>Yname\<^bold>Yattribute\<close>\<^verbatim>\<open>=\<close>\<open>value\<dots>\<^bold>X\<close> \\
-      \<^verbatim>\<open></\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> & \<open>\<^bold>X\<^bold>Y\<^bold>X\<close> \\
-    \end{tabular}
-
-    There is no special case for empty body text, i.e.\ \<^verbatim>\<open><foo/>\<close> is treated
-    like \<^verbatim>\<open><foo></foo>\<close>. Also note that \<open>\<^bold>X\<close> and \<open>\<^bold>Y\<close> may never occur in
-    well-formed XML documents.
-
-  Parsing YXML is pretty straight-forward: split the text into chunks
-  separated by \<open>\<^bold>X\<close>, then split each chunk into sub-chunks separated by \<open>\<^bold>Y\<close>.
-  Markup chunks start with an empty sub-chunk, and a second empty sub-chunk
-  indicates close of an element. Any other non-empty chunk consists of plain
-  text. For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or @{file
-  "~~/src/Pure/PIDE/yxml.scala"}.
-
-  YXML documents may be detected quickly by checking that the first two
-  characters are \<open>\<^bold>X\<^bold>Y\<close>.
-\<close>
-
 end
\ No newline at end of file