--- a/src/HOL/TPTP/TPTP_Parser/make_tptp_parser Fri Mar 09 15:39:00 2012 +0000
+++ b/src/HOL/TPTP/TPTP_Parser/make_tptp_parser Fri Mar 09 15:39:06 2012 +0000
@@ -1,18 +1,15 @@
#!/bin/bash
#
-# make_tptp_parser - Generates Isabelle-friendly version of ML-Yacc's library,
-# runs ML-Yacc to generate TPTP parser, and makes the
-# generated parser Isabelle-friendly.
+# make_tptp_parser - Runs ML-Yacc to generate TPTP parser and makes it
+# Isabelle-friendly.
#
# This code is based on that used in src/Tools/Metis to adapt Metis for
# use in Isabelle.
-MLYACCDIR=./ml-yacc
INTERMEDIATE_FILES="tptp.yacc.sig tptp.lex.sml tptp.yacc.sml"
-MLYACCLIB_FILES="base.sig join.sml lrtable.sml stream.sml parser2.sml"
echo "Cleaning"
-rm -f {tptp_lexyacc,ml_yacc_lib}.ML
+rm -f tptp_lexyacc.ML
echo "Generating lexer and parser"
ml-lex tptp.lex && ml-yacc tptp.yacc
echo "Generating tptp_lexyacc.ML"
@@ -38,47 +35,3 @@
) > tptp_lexyacc.ML
rm -f $INTERMEDIATE_FILES tptp.yacc.desc
-
-#Now patch and collate ML-Yacc's library files
-echo "Generating ml_yacc_lib.ML"
-(
- cat <<EOF
-
-(******************************************************************)
-(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
-(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
-(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
-(******************************************************************)
-
-print_depth 0;
-
-(*
- This file is generated from the contents of ML-Yacc's lib directory.
- ML-Yacc's COPYRIGHT-file contents follow:
-
-EOF
- perl -pe 'print " ";' ml-yacc/COPYRIGHT
- echo "*)"
-
-for FILE in $MLYACCLIB_FILES
-do
- echo
- echo "(**** Original file: $FILE ****)"
- echo
- echo -e " $FILE" >&2
- perl -p -e 's/\bref\b/Unsynchronized.ref/g;' \
- -e 's/Unsafe\.(.*)/\1/g;' \
- -e 's/\bconcat\b/String.concat/g;' \
- -e 's/(?<!List\.)foldr\b/List.foldr/g;' \
- -e 's/\bfoldl\b/List.foldl/g;' \
- -e 's/val print = fn s => TextIO\.output\(TextIO\.stdOut,s\)$//g;' \
- -e 's/\bprint\b/TextIO.print/g;' \
- $MLYACCDIR/lib/$FILE
- done
-
- cat <<EOF
-;
-print_depth 10;
-EOF
-
-) > ml_yacc_lib.ML
\ No newline at end of file