--- a/NEWS Fri Jun 27 15:24:56 2014 +0200
+++ b/NEWS Fri Jun 27 15:30:57 2014 +0200
@@ -855,6 +855,10 @@
incompatibility for old tools that do not use the $ISABELLE_PROCESS
settings variable yet.
+* Removed obsolete "isabelle unsymbolize". Note that the usual format
+for email communication is the Unicode rendering of Isabelle symbols,
+as produced by Isabelle/jEdit, for example.
+
* Retired the now unused Isabelle tool "wwwfind". Similar
functionality may be integrated into PIDE/jEdit at a later point.
--- a/lib/Tools/unsymbolize Fri Jun 27 15:24:56 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: remove unreadable symbol names from sources
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG [FILES|DIRS...]"
- echo
- echo " Recursively find .thy/.ML files and remove symbols that are unreadably"
- echo " in plain text (e.g. \<Longrightarrow>)."
- echo
- echo " Note: this is an ad-hoc script; there is no systematic way to replace"
- echo " symbols independently of the inner syntax of a theory!"
- echo
- echo " Old versions of files are preserved by appending \"~~\"."
- echo
- exit 1
-}
-
-
-## process command line
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-SPECS="$@"; shift "$#"
-
-
-## main
-
-find $SPECS \( -name \*.ML -o -name \*.thy \) -print0 | \
- xargs -0 "$ISABELLE_HOME/lib/scripts/unsymbolize"
--- a/lib/scripts/unsymbolize Fri Jun 27 15:24:56 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-#!/usr/bin/env perl
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# unsymbolize - remove unreadable symbol names from sources
-
-use warnings;
-use strict;
-
-sub unsymbolize {
- my ($file) = @_;
-
- open (FILE, $file) || die $!;
- undef $/; my $text = <FILE>; $/ = "\n"; # slurp whole file
- close FILE || die $!;
-
- $_ = $text;
-
- # Pure
- s/\\?\\<And>/!!/g;
- s/\\?\\<Colon>/::/g;
- s/\\?\\<Longrightarrow>/==>/g;
- s/\\?\\<Midarrow>\\?\\<Rightarrow>/==>/g;
- s/\\?\\<Rightarrow>/=>/g;
- s/\\?\\<equiv>/==/g;
- s/\\?\\<dots>/.../g;
- s/\\?\\<lbrakk> ?/[| /g;
- s/\\?\\ ?<rbrakk>/ |]/g;
- s/\\?\\<lparr> ?/(| /g;
- s/\\?\\ ?<rparr>/ |)/g;
- # HOL
- s/\\?\\<longleftrightarrow>/<->/g;
- s/\\?\\<longrightarrow>/-->/g;
- s/\\?\\<midarrow>\\?\\<rightarrow>/-->/g;
- s/\\?\\<rightarrow>/->/g;
- s/\\?\\<not>/~/g;
- s/\\?\\<notin>/~:/g;
- s/\\?\\<noteq>/~=/g;
- s/\\?\\<some> ?/SOME /g;
- # outer syntax
- s/\\?\\<rightleftharpoons>/==/g;
- s/\\?\\<rightharpoonup>/=>/g;
- s/\\?\\<leftharpoondown>/<=/g;
-
- my $result = $_;
-
- if ($text ne $result) {
- print STDERR "changing $file\n";
- if (! -f "$file~~") {
- rename $file, "$file~~" || die $!;
- }
- open (FILE, "> $file") || die $!;
- print FILE $result;
- close FILE || die $!;
- }
-}
-
-
-## main
-
-foreach my $file (@ARGV) {
- eval { &unsymbolize($file); };
- if ($@) { print STDERR "*** unsymbolize $file: ", $@, "\n"; }
-}
--- a/src/Doc/System/Misc.thy Fri Jun 27 15:24:56 2014 +0200
+++ b/src/Doc/System/Misc.thy Fri Jun 27 15:30:57 2014 +0200
@@ -472,26 +472,6 @@
"();"} in ML will return to the Isar toplevel. *}
-section {* Remove awkward symbol names from theory sources *}
-
-text {*
- The @{tool_def unsymbolize} tool tunes Isabelle theory sources to
- improve readability for plain ASCII output (e.g.\ in email
- communication). Most notably, @{tool unsymbolize} replaces awkward
- arrow symbols such as @{verbatim "\\"}@{verbatim "<Longrightarrow>"}
- by @{verbatim "==>"}.
-\begin{ttbox}
-Usage: isabelle unsymbolize [FILES|DIRS...]
-
- Recursively find .thy/.ML files, removing unreadable symbol names.
- Note: this is an ad-hoc script; there is no systematic way to replace
- symbols independently of the inner syntax of a theory!
-
- Renames old versions of FILES by appending "~~".
-\end{ttbox}
-*}
-
-
section {* Output the version identifier of the Isabelle distribution *}
text {*