Changeset 273838 in git

Timestamp:

Apr 17, 1997, 4:31:30 PM (26 years ago)

Author:

Jens Schmidt <schmidt@…>

Branches:

(u'spielwiese', '0d6b7fcd9813a1ca1ed4220cfa2b104b97a0a003')

Children:

8591c5247e9885df77234d8c0f31a9ad77cf7bf9

Parents:

50b2dfd4d9dbd3086efcc841c997bede4fe6b7a7

Message:

o makeheader.pl reads new format now


git-svn-id: file:///usr/local/Singular/svn/trunk@170 2c84dea3-7e68-4137-9b89-c4e89433aadc

File:

• factory/bin/makeheader.pl (modified) (3 diffs)

factory/bin/makeheader.pl

@@ -1 +1 @@
 #!/usr/bin/perl
-# $ Id: $
+# $Id: makeheader.pl,v 1.2 1997-04-17 14:31:30 schmidt Exp $
 #
-# makeheader - generate a header file out of several header file (ver 1.2).
+# makeheader.pl - generate a header file out of several header file (ver 1.2).
 #
 
@@ -27 +27 @@
 
 To include a header file into the generated header file
-\(= <outfile>) use the command `.INCLUDE <includefile>' on a
-single line in <templatefile>.
-This line is replaced by sections marked with /*BEGINPUBLIC*/
-and /*ENDPUBLIC*/ from <includefile>. <includefile> is looked up
-in all <includedir>s, then in the current directory, then in
-the base directory of <templatefile>.\n";
+\(= <outfile>) use the two lines 
+
+/*MAKEHEADER*/
+#include \"<includefile>\"
+
+in <templatefile>.
+
+If you use the alternate form
+
+/*MAKEHEADER PUBLIC ONLY*/
+#include \"<includefile>\"
+
+only sections marked with /*BEGINPUBLIC*/ and /*ENDPUBLIC*/ are
+pasted from <includefile> into <outfile>.
+
+<includefile> is looked up in all <includedir>s, then in the
+current directory, then in the base directory of
+<templatefile>.\n";
 }
 
@@ -62 +74 @@
 
 while( <INFILE> ) {
-    if ( /^\.INCLUDE/ ) {
-        s/^\.INCLUDE //;
-        chop;
-        $inclfile = &searchpath( $_, $includes ) ||
-            die "makeheader: Can not open included file $_ for reading!\n";
+    if ( /^\/\*MAKEHEADER(.*)\*\/$/ ) {
+        # check whether we have to read public part only
+        if ( $1 eq " PUBLIC ONLY" ) {
+            $public_only = 1;
+        } else {
+            $public_only = 0;
+        }
+
+        # get name of file to include
+        $_ = <INFILE>; chop;
+        if ( /^\#include \"(.*)\"$/ ) {
+            $inclfile = $1;
+        } else {
+            die "makeheader: $_ is not a valid include directive!\n";
+        }
+
+        $inclfile = &searchpath( $inclfile, $includes ) ||
+            die "makeheader: Can not open included file $inclfile for reading!\n";
         open( INCLFILE, $inclfile ) ||
-            die "makeheader: Can not open included file $_ for reading!\n";
+            die "makeheader: Can not open included file $inclfile for reading!\n";
 
-        print OUTFILE "/* Stuff from $_ */";
-        while ( <INCLFILE> ) {
-            if ( /\/\*BEGINPUBLIC\*\// ) {
-                while ( <INCLFILE> ) {
-                    last if ( /\/\*ENDPUBLIC\*\// );
-                    print OUTFILE $_;
+        print OUTFILE "\n/* Stuff included from $inclfile */\n";
+        if ( $public_only ) {
+            # read public part only
+            while ( <INCLFILE> ) {
+                if ( /^\/\*BEGINPUBLIC\*\/$/ ) {
+                    while ( <INCLFILE> ) {
+                        last if ( /^\/\*ENDPUBLIC\*\/$/ );
+                        print OUTFILE $_;
+                    }
                 }
             }
+        } else {
+            # just paste contents into output
+            while ( <INCLFILE> ) { print OUTFILE $_; }
         }
         close INCLFILE;