| author | wenzelm | 
| Sat, 29 Apr 2017 11:06:39 +0200 | |
| changeset 65633 | 826311fca263 | 
| parent 39444 | beabb8443ee4 | 
| child 72004 | 913162a47d9f | 
| permissions | -rwxr-xr-x | 
| 
23442
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
1  | 
#!/usr/bin/perl  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
2  | 
|
| 39444 | 3  | 
# Copyright (c) 2006 Joe Hurd, distributed under the BSD License  | 
| 
23442
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
4  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
5  | 
use strict;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
6  | 
use warnings;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
7  | 
use Pod::Usage;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
8  | 
use Getopt::Std;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
9  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
10  | 
use vars qw($opt_h $opt_c $opt_r);  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
11  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
12  | 
getopts('hc:r:');
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
13  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
14  | 
if ($opt_h or scalar @ARGV == 0)  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
15  | 
{
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
16  | 
    pod2usage({-exitval => 2,
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
17  | 
-verbose => 2});  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
18  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
19  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
20  | 
if (!$opt_c) { die "mlpp: you must specify the SML compiler\n"; }
 | 
| 39350 | 21  | 
if ($opt_c ne "mosml" && $opt_c ne "mlton" && $opt_c ne "polyml") {
 | 
22  | 
    die "mlpp: the SML compiler must be one of {mosml,mlton,polyml}.\n";
 | 
|
| 
23442
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
23  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
24  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
25  | 
# Autoflush STDIN  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
26  | 
$|++;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
27  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
28  | 
sub unquotify {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
29  | 
    if (scalar @_ == 0) { return; }
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
30  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
31  | 
my $pre = "[";  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
32  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
33  | 
    for my $quote (@_) {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
34  | 
my $nl = chomp $quote;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
35  | 
my @qs = split (/\^(\w+)/, $quote);  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
36  | 
my @ps = ();  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
37  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
38  | 
        for (my $s = 0; 0 < scalar @qs; $s = 1 - $s) {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
39  | 
my $q = shift @qs;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
40  | 
            if ($s == 0) {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
41  | 
$q =~ s/\\/\\\\/g;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
42  | 
$q =~ s/\"/\\\"/g;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
43  | 
push @ps, "QUOTE \"$q\"" unless ($q eq "");  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
44  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
45  | 
            elsif ($s == 1) {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
46  | 
push @ps, "ANTIQUOTE $q";  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
47  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
48  | 
            else { die; }
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
49  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
50  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
51  | 
        if (0 < $nl) {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
52  | 
            if (0 < scalar @ps) {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
53  | 
my $p = pop @ps;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
54  | 
                if ($p =~ /QUOTE \"(.*)\"/) { push @ps, "QUOTE \"$1\\n\""; }
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
55  | 
                else { push @ps, $p; push @ps, "QUOTE \"\\n\""; }
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
56  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
57  | 
            else { push @ps, "QUOTE \"\\n\""; }
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
58  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
59  | 
        else {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
60  | 
(0 < scalar @ps) or die;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
61  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
62  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
63  | 
        print STDOUT ($pre . join (", ", @ps));
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
64  | 
$pre = ",\n";  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
65  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
66  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
67  | 
print STDOUT "]";  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
68  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
69  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
70  | 
sub print_normal {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
71  | 
(scalar @_ == 1) or die;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
72  | 
my $text = shift @_;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
73  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
74  | 
    if ($opt_c eq "mosml") {
 | 
| 39350 | 75  | 
$text =~ s/Array\.copy/Array_copy/g;  | 
76  | 
$text =~ s/Array\.foldli/Array_foldli/g;  | 
|
77  | 
$text =~ s/Array\.foldri/Array_foldri/g;  | 
|
78  | 
$text =~ s/Array\.modifyi/Array_modifyi/g;  | 
|
79  | 
$text =~ s/OS\.Process\.isSuccess/OS_Process_isSuccess/g;  | 
|
| 
23442
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
80  | 
$text =~ s/PP\.ppstream/ppstream/g;  | 
| 
39443
 
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
 
blanchet 
parents: 
39350 
diff
changeset
 | 
81  | 
$text =~ s/String\.concatWith/String_concatWith/g;  | 
| 
 
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
 
blanchet 
parents: 
39350 
diff
changeset
 | 
82  | 
$text =~ s/String\.isSubstring/String_isSubstring/g;  | 
| 39350 | 83  | 
$text =~ s/String\.isSuffix/String_isSuffix/g;  | 
84  | 
$text =~ s/Substring\.full/Substring_full/g;  | 
|
| 
23442
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
85  | 
$text =~ s/TextIO\.inputLine/TextIO_inputLine/g;  | 
| 39350 | 86  | 
$text =~ s/Vector\.foldli/Vector_foldli/g;  | 
87  | 
$text =~ s/Vector\.mapi/Vector_mapi/g;  | 
|
| 
23442
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
88  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
89  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
90  | 
print STDOUT $text;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
91  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
92  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
93  | 
sub process_file {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
94  | 
(scalar @_ == 1) or die;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
95  | 
my $filename = shift @_;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
96  | 
my $line_num = 0;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
97  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
98  | 
    if ($opt_c eq "mlton") {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
99  | 
print STDOUT "(*#line 0.0 \"$filename\"*)\n";  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
100  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
101  | 
|
| 39350 | 102  | 
open my $INPUT, "$filename" or  | 
103  | 
die "mlpp: couldn't open $filename: $!\n";  | 
|
| 
23442
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
104  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
105  | 
my $state = "normal";  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
106  | 
my $comment = 0;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
107  | 
my $revealed_comment = 0;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
108  | 
my @quotes = ();  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
109  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
110  | 
    while (my $line = <$INPUT>) {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
111  | 
(chomp ($line) == 1)  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
112  | 
or warn "no terminating newline in $filename\nline = '$line'\n";  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
113  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
114  | 
        while (1) {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
115  | 
            if ($state eq "quote") {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
116  | 
                if ($line =~ /(.*?)\`(.*)$/) {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
117  | 
push @quotes, $1;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
118  | 
$line = $2;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
119  | 
unquotify @quotes;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
120  | 
@quotes = ();  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
121  | 
$state = "normal";  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
122  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
123  | 
                else {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
124  | 
push @quotes, "$line\n";  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
125  | 
last;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
126  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
127  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
128  | 
            elsif ($state eq "comment") {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
129  | 
                if ($line =~ /^(.*?)(\(\*|\*\))(.*)$/) {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
130  | 
my $leadup = $1;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
131  | 
my $pat = $2;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
132  | 
$line = $3;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
133  | 
print STDOUT $leadup;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
134  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
135  | 
                    if ($pat eq "(*") {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
136  | 
print STDOUT $pat;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
137  | 
++$comment;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
138  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
139  | 
                    elsif ($pat eq "*)") {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
140  | 
print STDOUT $pat;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
141  | 
--$comment;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
142  | 
                        if ($comment == 0) { $state = "normal"; }
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
143  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
144  | 
                    else {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
145  | 
die;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
146  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
147  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
148  | 
                else {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
149  | 
print STDOUT "$line\n";  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
150  | 
last;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
151  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
152  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
153  | 
            elsif ($state eq "dquote") {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
154  | 
                if ($line =~ /^(.*?)\"(.*)$/) {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
155  | 
my $leadup = $1;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
156  | 
$line = $2;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
157  | 
print STDOUT ($leadup . "\"");  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
158  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
159  | 
                    if ($leadup =~ /(\\+)$/ && ((length $1) % 2 == 1)) {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
160  | 
# This is an escaped double quote  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
161  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
162  | 
                    else {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
163  | 
$state = "normal";  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
164  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
165  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
166  | 
                else {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
167  | 
die "EOL inside \" quote\n";  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
168  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
169  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
170  | 
            elsif ($state eq "normal") {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
171  | 
                if ($line =~ /^ *use *\"([^"]+)\" *; *$/) {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
172  | 
my $use_filename = $1;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
173  | 
                    if ($use_filename !~ /^\// && $filename =~ /^(.*)\//) {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
174  | 
$use_filename = $1 . '/' . $use_filename;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
175  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
176  | 
process_file ($use_filename);  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
177  | 
                    if ($opt_c eq "mlton") {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
178  | 
print STDOUT "(*#line $line_num.0 \"$filename\"*)\n";  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
179  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
180  | 
print STDOUT "\n";  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
181  | 
last;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
182  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
183  | 
                elsif ($line =~ /^(.*?)(\`|\(\*|\*\)|\")(.*)$/) {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
184  | 
my $leadup = $1;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
185  | 
my $pat = $2;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
186  | 
$line = $3;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
187  | 
print_normal $leadup;  | 
| 39350 | 188  | 
|
| 
23442
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
189  | 
                    if ($pat eq "`") {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
190  | 
$state = "quote";  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
191  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
192  | 
                    elsif ($pat eq "(*") {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
193  | 
my $is_revealed = 0;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
194  | 
                        if ($line =~ /^([[:alnum:]_-]+)/) {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
195  | 
my $rev = $1;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
196  | 
if ($rev eq $opt_c ||  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
197  | 
                                ($opt_r && $rev =~ /^$opt_r$/)) {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
198  | 
my $rev_len = length $rev;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
199  | 
$line = substr $line, $rev_len;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
200  | 
++$revealed_comment;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
201  | 
$is_revealed = 1;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
202  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
203  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
204  | 
                        if (!$is_revealed) {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
205  | 
print STDOUT $pat;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
206  | 
$state = "comment";  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
207  | 
++$comment;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
208  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
209  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
210  | 
                    elsif ($pat eq "*)") {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
211  | 
                        if ($revealed_comment == 0) {
 | 
| 39350 | 212  | 
die "mlpp: too many comment closers.\n"  | 
| 
23442
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
213  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
214  | 
--$revealed_comment;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
215  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
216  | 
                    elsif ($pat eq "\"") {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
217  | 
print STDOUT $pat;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
218  | 
$state = "dquote";  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
219  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
220  | 
                    else {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
221  | 
die;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
222  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
223  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
224  | 
                else {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
225  | 
print_normal "$line\n";  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
226  | 
last;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
227  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
228  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
229  | 
            else {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
230  | 
die;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
231  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
232  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
233  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
234  | 
++$line_num;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
235  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
236  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
237  | 
    if ($state eq "quote") {
 | 
| 39350 | 238  | 
die "mlpp: EOF inside \` quote\n";  | 
| 
23442
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
239  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
240  | 
    elsif ($state eq "dquote") {
 | 
| 39350 | 241  | 
die "mlpp: EOF inside \" quote\n";  | 
| 
23442
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
242  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
243  | 
    elsif ($state eq "comment") {
 | 
| 39350 | 244  | 
die "mlpp: EOF inside comment\n";  | 
| 
23442
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
245  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
246  | 
    else {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
247  | 
($state eq "normal") or die;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
248  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
249  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
250  | 
close $INPUT;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
251  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
252  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
253  | 
while (0 < scalar @ARGV) {
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
254  | 
my $filename = shift @ARGV;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
255  | 
process_file $filename;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
256  | 
}  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
257  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
258  | 
__END__  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
259  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
260  | 
=pod  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
261  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
262  | 
=head1 NAME  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
263  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
264  | 
mlpp - preprocesses SML files for compilation  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
265  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
266  | 
=head1 SYNOPSIS  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
267  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
268  | 
mlpp [-h] [-c compiler] [-r TAG] sml-file ... > preprocessed-sml-file  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
269  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
270  | 
=head1 ARGUMENTS  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
271  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
272  | 
The recognized flags are described below:  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
273  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
274  | 
=over 2  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
275  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
276  | 
=item B<-h>  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
277  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
278  | 
Produce this documentation.  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
279  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
280  | 
=item B<-c compiler>  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
281  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
282  | 
Select the SML compiler that will be used.  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
283  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
284  | 
=item B<-r TAG-REGEX>  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
285  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
286  | 
Remove all comment brackets tagged like this: (*TAG revealed-code *)  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
287  | 
where the TAG-REGEX matches the TAG.  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
288  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
289  | 
=back  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
290  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
291  | 
=head1 DESCRIPTION  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
292  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
293  | 
Concatenates the input list of SML source files into a single file  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
294  | 
ready to be compiled, by expanding quotations and antiquotations, and  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
295  | 
concatenating into a single file.  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
296  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
297  | 
=head1 BUGS  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
298  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
299  | 
Waiting to rear their ugly heads.  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
300  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
301  | 
=head1 AUTHORS  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
302  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
303  | 
Joe Hurd <joe@gilith.com>  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
304  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
305  | 
=head1 SEE ALSO  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
306  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
307  | 
Perl(1).  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
308  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
309  | 
=cut  |