# HG changeset patch # User wenzelm # Date 1403875857 -7200 # Node ID c14af83bd8db7a608d6c0984a83fa24b0347a4d9 # Parent b441f330078b1d0fdc3a4b2c32eb134248b173e2 removed obsolete "isabelle unsymbolize"; diff -r b441f330078b -r c14af83bd8db NEWS --- 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. diff -r b441f330078b -r c14af83bd8db lib/Tools/unsymbolize --- 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. \)." - 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" diff -r b441f330078b -r c14af83bd8db 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 = ; $/ = "\n"; # slurp whole file - close FILE || die $!; - - $_ = $text; - - # Pure - s/\\?\\/!!/g; - s/\\?\\/::/g; - s/\\?\\/==>/g; - s/\\?\\\\?\\/==>/g; - s/\\?\\/=>/g; - s/\\?\\/==/g; - s/\\?\\/.../g; - s/\\?\\ ?/[| /g; - s/\\?\\ ?/ |]/g; - s/\\?\\ ?/(| /g; - s/\\?\\ ?/ |)/g; - # HOL - s/\\?\\/<->/g; - s/\\?\\/-->/g; - s/\\?\\\\?\\/-->/g; - s/\\?\\/->/g; - s/\\?\\/~/g; - s/\\?\\/~:/g; - s/\\?\\/~=/g; - s/\\?\\ ?/SOME /g; - # outer syntax - s/\\?\\/==/g; - s/\\?\\/=>/g; - s/\\?\\/<=/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"; } -} diff -r b441f330078b -r c14af83bd8db src/Doc/System/Misc.thy --- 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 ""} - 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 {*