--- 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.
--- 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"
--- 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 $!;
--- 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
--- 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