~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to doc/manual/xdata2html.pl

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
1
 
#!/usr/bin/env perl
2
 
 
3
 
# Xdoc to HTML Converter
4
 
# Copyright (C) 2014 David Rager (ragerdl@cs.utexas.edu)
5
 
#
6
 
# License: (An MIT/X11-style license)
7
 
#
8
 
#   Permission is hereby granted, free of charge, to any person obtaining a
9
 
#   copy of this software and associated documentation files (the "Software"),
10
 
#   to deal in the Software without restriction, including without limitation
11
 
#   the rights to use, copy, modify, merge, publish, distribute, sublicense,
12
 
#   and/or sell copies of the Software, and to permit persons to whom the
13
 
#   Software is furnished to do so, subject to the following conditions:
14
 
#
15
 
#   The above copyright notice and this permission notice shall be included in
16
 
#   all copies or substantial portions of the Software.
17
 
#
18
 
#   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
19
 
#   IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
20
 
#   FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
21
 
#   AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
22
 
#   LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
23
 
#   FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
24
 
#   DEALINGS IN THE SOFTWARE.
25
 
 
26
 
use warnings;
27
 
use strict;
28
 
use JSON::XS;
29
 
use XML::LibXML;
30
 
use XML::LibXSLT;
31
 
 
32
 
print <<END;
33
 
 
34
 
-------------------------------------------------------------------------------
35
 
 
36
 
xdata2html.pl: Convert xdata.js and xindex.js into HTML files so
37
 
               search engines can crawl our doucmentation.
38
 
 
39
 
   NOTE: Only those who are trying make their Xdoc manual accessible
40
 
         to search engines need to run this script.  Otherwise, they
41
 
         should just use index.html.
42
 
 
43
 
-------------------------------------------------------------------------------
44
 
 
45
 
END
46
 
 
47
 
print "; Converting xdata.js\n\n";
48
 
 
49
 
sub read_whole_file {
50
 
  my $filename = shift;
51
 
  open (my $fh, "<", $filename) or die("Can't open $filename: $!\n");
52
 
  local $/ = undef;
53
 
  my $ret = <$fh>;
54
 
  close($fh);
55
 
  return $ret;
56
 
}
57
 
 
58
 
sub wrap_xdoc_fragment {
59
 
        my $str = shift;
60
 
    my $wrap = "<!DOCTYPE xdoc [";
61
 
    $wrap .= "<!ENTITY mdash \"&#8212;\">";
62
 
    $wrap .= "<!ENTITY rarr \"&#8594;\">";
63
 
    $wrap .= "<!ENTITY nbsp \"&#160;\">";
64
 
    $wrap .= "]>";
65
 
    $wrap .= "<root>$str</root>";
66
 
    return $wrap;
67
 
}
68
 
 
69
 
if (! -f "xdata.js") {
70
 
    print "Error: xdata.js not found.\n";
71
 
    exit(1);
72
 
}
73
 
 
74
 
print "; Reading file\n";
75
 
 
76
 
my $xdatastr = read_whole_file("xdata.js");
77
 
print "; Checking xdata file\n";
78
 
 
79
 
my $json;
80
 
my $start = "var xdata = ";
81
 
if (length($start) < length($xdatastr)
82
 
    && substr($xdatastr, 0, length($start)) eq $start
83
 
    && substr($xdatastr, length($xdatastr)-1, 1) eq ";")
84
 
{
85
 
    my $stop = length($xdatastr) - length($start) - length(";");
86
 
    $json = substr($xdatastr, length($start), $stop);
87
 
}
88
 
else {
89
 
    print "Error: xdata.js does not have the expected format\n";
90
 
    exit(1);
91
 
}
92
 
 
93
 
print "; Parsing JSON data.\n";
94
 
my $xsd = new JSON::XS;
95
 
my $xdata = $xsd->decode($json);
96
 
if (!(ref($xdata) eq "HASH")) {
97
 
    print "Error: JSON object within xdata.js not a hash?\n";
98
 
    exit(1);
99
 
}
100
 
 
101
 
 
102
 
my $xindexstr = read_whole_file("xindex.js");
103
 
print "; Checking xindex file\n";
104
 
 
105
 
if (! -f "xindex.js") {
106
 
    print "Error: xindex.js not found.\n";
107
 
    exit(1);
108
 
}
109
 
 
110
 
$start = "var xindex = ";
111
 
if (length($start) < length($xindexstr)
112
 
    && substr($xindexstr, 0, length($start)) eq $start
113
 
    && substr($xindexstr, length($xindexstr)-1, 1) eq ";")
114
 
{
115
 
    my $stop = length($xindexstr) - length($start) - length(";");
116
 
    $json = substr($xindexstr, length($start), $stop);
117
 
}
118
 
else {
119
 
    print "Error: xindex.js does not have the expected format\n";
120
 
    exit(1);
121
 
}
122
 
 
123
 
print "; Parsing JSON index.\n";
124
 
my $xsi = new JSON::XS;
125
 
my $xindex = $xsi->decode($json);
126
 
if (!(ref($xindex) eq "ARRAY")) {
127
 
    print "Error: JSON object within xindex.js not a hash?\n";
128
 
    exit(1);
129
 
}
130
 
 
131
 
my %shorts = ();
132
 
my %human_readable_names = ();
133
 
foreach my $entry (@$xindex) {
134
 
        $shorts{$entry->[0]} = $entry->[4];
135
 
        $human_readable_names{$entry->[0]} = $entry->[1];
136
 
}
137
 
 
138
 
my $xml_parser  = XML::LibXML->new;
139
 
my $xslt_parser = XML::LibXSLT->new;
140
 
my $xsl = $xml_parser->parse_file("render-html.xsl");
141
 
my $stylesheet  = $xslt_parser->parse_stylesheet($xsl);
142
 
 
143
 
my $progress = 0;
144
 
while(my ($key,$val) = each %$xdata)
145
 
{
146
 
        my $filename = "HTML/$key.html";
147
 
        open (my $fh, ">", $filename) or die "Could not open $filename";
148
 
 
149
 
    my $enc = $xsd->encode($val);
150
 
        my $long = $val->[3];
151
 
        my $human_readable_name = $human_readable_names{$key};
152
 
        my $short = $shorts{$key};
153
 
        my $pagexml = "";
154
 
        $pagexml .= "<p>$short</p>\n";
155
 
        $pagexml .= "$long";
156
 
        $pagexml = wrap_xdoc_fragment($pagexml);
157
 
        my $xml = $xml_parser->parse_string($pagexml);
158
 
        my $results = "";
159
 
    $results = $stylesheet->transform($xml);
160
 
        my $output = $stylesheet->output_string($results);
161
 
 
162
 
 
163
 
        my $pagehtml .= "<html>\n<head>\n";
164
 
        $pagehtml .= "<meta charset=\"UTF-8\">\n";
165
 
        $pagehtml .= "<title>$human_readable_name</title>\n";
166
 
        # To debug this script, you may need to comment out the
167
 
        # javascript, since it causes the browser to immediately redirect.
168
 
        # Since it's javascript, this redirect should not be run by search
169
 
        # engines, allowing them to crawl this HTML page.
170
 
        $pagehtml .= "<script language=\"javascript\">\n";
171
 
        $pagehtml .= "<!--\n";
172
 
        $pagehtml .= "  location.replace(\"../index.html?topic=$key\");\n";
173
 
        $pagehtml .= "//-->\n";
174
 
        $pagehtml .= "</script>\n";
175
 
        $pagehtml .= "<link rel=\"stylesheet\" type=\"text/css\" href=\"../style.css\"/>\n";
176
 
    $pagehtml .= "</head>\n<body>\n\n<h3>";
177
 
    $pagehtml .= "$key";
178
 
        $pagehtml .= "</h3>\n\n";
179
 
        $pagehtml .= "$output";
180
 
        $pagehtml .= "</body>\n</html>\n";
181
 
 
182
 
        print $fh "$pagehtml";
183
 
 
184
 
        if ($progress % 500 == 0) {
185
 
                print "Done generating $progress HTML files\n";
186
 
        }
187
 
        $progress++;
188
 
}
189
 
 
190
 
print "; All done.\n\n";