]> matita.cs.unibo.it Git - helm.git/blob - helm/graphs/tools/mk_html.pl
incomplete proof completed
[helm.git] / helm / graphs / tools / mk_html.pl
1 #!/usr/bin/perl
2
3 use URI::Escape;
4
5 print <<EOT;
6 <?xml version="1.0"?>
7 <html xmlns="http://www.w3.org/1999/xhtml" xmlns:subst="http://www.cs.unibo.it/helm/subst">
8  <head>
9   <title>Graph</title>
10  </head>
11  <body bgcolor="white" onLoad="window.focus()">
12   <script>
13    var draw_graphURL = "<subst:draw_graphURL/>";
14 <![CDATA[
15    document.write('<img border="false" src="' + draw_graphURL + 'get_gif?pid=$ARGV[0]" usemap="#graphe">');
16 ]]>
17   </script>
18   <map name="graphe">
19 EOT
20
21 my $count = 0;
22
23 while (<STDIN>) {
24  $count++;
25  my (undef,$point1,$point2,$uri) = split;
26  my ($point1x,$point1y) = split /,/,$point1;
27  my ($point2x,$point2y) = split /,/,$point2;
28  $point1y = substr($point1y,0,-1);
29  $point2y = substr($point2y,0,-1);
30  $point1x = substr($point1x,1);
31  $point2x = substr($point2x,1);
32
33  print <<EOT;
34    <area shape="rect" href="$uri" coords="$point1x,$point2y,$point2x,$point1y" />
35 EOT
36 }
37
38 print <<EOT;
39    </map>
40   <script>
41 <![CDATA[
42    document.write('</img>');
43 ]]>
44   </script>
45  </body>
46 </html>
47 EOT