removed obsolete "isabelle unsymbolize";
authorwenzelm
Fri Jun 27 15:30:57 2014 +0200 (2014-06-27)
changeset 57413c14af83bd8db
parent 57412 b441f330078b
child 57414 fe1be2844fda
removed obsolete "isabelle unsymbolize";
NEWS
lib/Tools/unsymbolize
lib/scripts/unsymbolize
src/Doc/System/Misc.thy
     1.1 --- a/NEWS	Fri Jun 27 15:24:56 2014 +0200
     1.2 +++ b/NEWS	Fri Jun 27 15:30:57 2014 +0200
     1.3 @@ -855,6 +855,10 @@
     1.4  incompatibility for old tools that do not use the $ISABELLE_PROCESS
     1.5  settings variable yet.
     1.6  
     1.7 +* Removed obsolete "isabelle unsymbolize".  Note that the usual format
     1.8 +for email communication is the Unicode rendering of Isabelle symbols,
     1.9 +as produced by Isabelle/jEdit, for example.
    1.10 +
    1.11  * Retired the now unused Isabelle tool "wwwfind". Similar
    1.12  functionality may be integrated into PIDE/jEdit at a later point.
    1.13  
     2.1 --- a/lib/Tools/unsymbolize	Fri Jun 27 15:24:56 2014 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,39 +0,0 @@
     2.4 -#!/usr/bin/env bash
     2.5 -#
     2.6 -# Author: Markus Wenzel, TU Muenchen
     2.7 -#
     2.8 -# DESCRIPTION: remove unreadable symbol names from sources
     2.9 -
    2.10 -
    2.11 -## diagnostics
    2.12 -
    2.13 -PRG="$(basename "$0")"
    2.14 -
    2.15 -function usage()
    2.16 -{
    2.17 -  echo
    2.18 -  echo "Usage: isabelle $PRG [FILES|DIRS...]"
    2.19 -  echo
    2.20 -  echo "  Recursively find .thy/.ML files and remove symbols that are unreadably"
    2.21 -  echo "  in plain text (e.g. \<Longrightarrow>)."
    2.22 -  echo
    2.23 -  echo "  Note: this is an ad-hoc script; there is no systematic way to replace"
    2.24 -  echo "  symbols independently of the inner syntax of a theory!"
    2.25 -  echo
    2.26 -  echo "  Old versions of files are preserved by appending \"~~\"."
    2.27 -  echo
    2.28 -  exit 1
    2.29 -}
    2.30 -
    2.31 -
    2.32 -## process command line
    2.33 -
    2.34 -[ "$#" -eq 0 -o "$1" = "-?" ] && usage
    2.35 -
    2.36 -SPECS="$@"; shift "$#"
    2.37 -
    2.38 -
    2.39 -## main
    2.40 -
    2.41 -find $SPECS \( -name \*.ML -o -name \*.thy \) -print0 | \
    2.42 -  xargs -0 "$ISABELLE_HOME/lib/scripts/unsymbolize"
     3.1 --- a/lib/scripts/unsymbolize	Fri Jun 27 15:24:56 2014 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,64 +0,0 @@
     3.4 -#!/usr/bin/env perl
     3.5 -#
     3.6 -# Author: Markus Wenzel, TU Muenchen
     3.7 -#
     3.8 -# unsymbolize - remove unreadable symbol names from sources
     3.9 -
    3.10 -use warnings;
    3.11 -use strict;
    3.12 -
    3.13 -sub unsymbolize {
    3.14 -    my ($file) = @_;
    3.15 -
    3.16 -    open (FILE, $file) || die $!;
    3.17 -    undef $/; my $text = <FILE>; $/ = "\n";         # slurp whole file
    3.18 -    close FILE || die $!;
    3.19 -
    3.20 -    $_ = $text;
    3.21 -
    3.22 -    # Pure
    3.23 -    s/\\?\\<And>/!!/g;
    3.24 -    s/\\?\\<Colon>/::/g;
    3.25 -    s/\\?\\<Longrightarrow>/==>/g;
    3.26 -    s/\\?\\<Midarrow>\\?\\<Rightarrow>/==>/g;
    3.27 -    s/\\?\\<Rightarrow>/=>/g;
    3.28 -    s/\\?\\<equiv>/==/g;
    3.29 -    s/\\?\\<dots>/.../g;
    3.30 -    s/\\?\\<lbrakk> ?/[| /g;
    3.31 -    s/\\?\\ ?<rbrakk>/ |]/g;
    3.32 -    s/\\?\\<lparr> ?/(| /g;
    3.33 -    s/\\?\\ ?<rparr>/ |)/g;
    3.34 -    # HOL
    3.35 -    s/\\?\\<longleftrightarrow>/<->/g;
    3.36 -    s/\\?\\<longrightarrow>/-->/g;
    3.37 -    s/\\?\\<midarrow>\\?\\<rightarrow>/-->/g;
    3.38 -    s/\\?\\<rightarrow>/->/g;
    3.39 -    s/\\?\\<not>/~/g;
    3.40 -    s/\\?\\<notin>/~:/g;
    3.41 -    s/\\?\\<noteq>/~=/g;
    3.42 -    s/\\?\\<some> ?/SOME /g;
    3.43 -    # outer syntax
    3.44 -    s/\\?\\<rightleftharpoons>/==/g;
    3.45 -    s/\\?\\<rightharpoonup>/=>/g;
    3.46 -    s/\\?\\<leftharpoondown>/<=/g;
    3.47 -
    3.48 -    my $result = $_;
    3.49 -
    3.50 -    if ($text ne $result) {
    3.51 -        print STDERR "changing $file\n";
    3.52 -        if (! -f "$file~~") {
    3.53 -            rename $file, "$file~~" || die $!;
    3.54 -        }
    3.55 -        open (FILE, "> $file") || die $!;
    3.56 -        print FILE $result;
    3.57 -        close FILE || die $!;
    3.58 -    }
    3.59 -}
    3.60 -
    3.61 -
    3.62 -## main
    3.63 -
    3.64 -foreach my $file (@ARGV) {
    3.65 -  eval { &unsymbolize($file); };
    3.66 -  if ($@) { print STDERR "*** unsymbolize $file: ", $@, "\n"; }
    3.67 -}
     4.1 --- a/src/Doc/System/Misc.thy	Fri Jun 27 15:24:56 2014 +0200
     4.2 +++ b/src/Doc/System/Misc.thy	Fri Jun 27 15:30:57 2014 +0200
     4.3 @@ -472,26 +472,6 @@
     4.4    "();"} in ML will return to the Isar toplevel.  *}
     4.5  
     4.6  
     4.7 -section {* Remove awkward symbol names from theory sources *}
     4.8 -
     4.9 -text {*
    4.10 -  The @{tool_def unsymbolize} tool tunes Isabelle theory sources to
    4.11 -  improve readability for plain ASCII output (e.g.\ in email
    4.12 -  communication).  Most notably, @{tool unsymbolize} replaces awkward
    4.13 -  arrow symbols such as @{verbatim "\\"}@{verbatim "<Longrightarrow>"}
    4.14 -  by @{verbatim "==>"}.
    4.15 -\begin{ttbox}
    4.16 -Usage: isabelle unsymbolize [FILES|DIRS...]
    4.17 -
    4.18 -  Recursively find .thy/.ML files, removing unreadable symbol names.
    4.19 -  Note: this is an ad-hoc script; there is no systematic way to replace
    4.20 -  symbols independently of the inner syntax of a theory!
    4.21 -
    4.22 -  Renames old versions of FILES by appending "~~".
    4.23 -\end{ttbox}
    4.24 -*}
    4.25 -
    4.26 -
    4.27  section {* Output the version identifier of the Isabelle distribution *}
    4.28  
    4.29  text {*