# HG changeset patch
# User sultana
# Date 1331307546 0
# Node ID 9e99afaade178d5a1f3758521b78b96014eca3b2
# Parent  6431a93ffeb6ed9e336c80db2e225a84d652144d
split make_tptp_parser into two scripts, for parser and lib respectively;

diff -r 6431a93ffeb6 -r 9e99afaade17 src/HOL/TPTP/TPTP_Parser/README
--- a/src/HOL/TPTP/TPTP_Parser/README	Fri Mar 09 15:39:00 2012 +0000
+++ b/src/HOL/TPTP/TPTP_Parser/README	Fri Mar 09 15:39:06 2012 +0000
@@ -1,9 +1,11 @@
 The TPTP parser is generated using ML-Yacc and relies on the ML-Yacc
 library to function. The ML-Yacc library is an external piece of
-software that needs a small modification for use in Isabelle.  The
-file "make_tptp_parser" patches the ML-Yacc library, generates the
-TPTP parser, and patches that to conform to Isabelle's naming
-conventions.
+software that needs a small modification for use in Isabelle. The
+relationship between Isabelle and ML-Yacc is similar to that with
+Metis (see src/Tools/Metis).
+
+The file "make_tptp_parser" generates the TPTP parser and patches it
+to conform to Isabelle's naming conventions.
 
 In order to generate the parser from its lex/yacc definition you need
 to have the ML-Yacc binaries. The sources can be downloaded via SVN as
@@ -14,20 +16,17 @@
 
 ML-Yacc is usually distributed with Standard ML of New Jersey, and its
 binaries can also be obtained as packages for some distributions of
-Linux.
+Linux. The script "make_tptp_parser" will produce a file called
+tptp_lexyacc.ML -- this is a compilation of the SML files (generated
+by ML-Yacc) making up the TPTP parser.
 
 The generated parser needs ML-Yacc's library. This is distributed with
-ML-Yacc's source code, in the lib/ directory.
-
-Assuming that you've got the ml-lex and ml-yacc binaries, and have a
-copy of the ML-Yacc sources in this directory, then running
-"make_tptp_parser" will generate two files:
-
- ml_yacc_lib.ML -- this is a compilation of slightly modified files
-                   making up ML-Yacc's library.
-
- tptp_lexyacc.ML -- this is a compilation of the SML files making up
-                    the TPTP parser.
+ML-Yacc's source code, in the lib/ directory. The ML-Yacc library
+cannot be used directly and must be patched. The script
+"make_mlyacclib" takes the ML-Yacc library (for instance, as
+downloaded from the ML-Yacc repo) and produces the file ml_yacc_lib.ML
+-- this is a compilation of slightly modified files making up
+ML-Yacc's library.
 
 Nik Sultana
-8th March 2012
\ No newline at end of file
+9th March 2012
\ No newline at end of file
diff -r 6431a93ffeb6 -r 9e99afaade17 src/HOL/TPTP/TPTP_Parser/make_mlyacclib
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/TPTP_Parser/make_mlyacclib	Fri Mar 09 15:39:06 2012 +0000
@@ -0,0 +1,54 @@
+#!/bin/bash
+#
+# make_mlyacclib - Generates Isabelle-friendly version of ML-Yacc's library.
+#
+# This code is based on that used in src/Tools/Metis to adapt Metis for
+# use in Isabelle.
+
+MLYACCDIR=./ml-yacc
+MLYACCLIB_FILES="base.sig join.sml lrtable.sml stream.sml parser2.sml"
+
+echo "Cleaning"
+rm -f ml_yacc_lib.ML
+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
diff -r 6431a93ffeb6 -r 9e99afaade17 src/HOL/TPTP/TPTP_Parser/make_tptp_parser
--- 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