]> matita.cs.unibo.it Git - helm.git/blob - helm/on-line/html/library/index.html
Many modifications to avoid JavaScript security rules of
[helm.git] / helm / on-line / html / library / index.html
1 <?xml version="1.0" encoding="UTF-8"?>
2 <!--
3 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "DTD/xhtml1-strict.dtd">
4 -->
5
6 <html xmlns:subst="http://www.cs.unibo.it/helm/subst">
7 <head>
8 <!-- Note: <subst:script/> are substitued by the stylesheet with <script />  -->
9 <!-- after changing @src in the concatenation of the interface URL with @src -->
10 <subst:script language="JavaScript" src="/javascript/defaults.js" />
11 <subst:script language="JavaScript" src="/javascript/utils.js" />
12 <title>Index</title>
13 </head>
14 <script>
15   var topurl = "<subst:topurl/>";
16 <![CDATA[
17   document.write('<frameset rows="18%,*" border="0" scrolling="no">');
18   var control_frame_URL=
19         topurl + '/html/library/control.html' +
20         '?topurl=' + topurl +
21         '&mode=' + getParam2('mode') +
22         '&cicuri=' + getParam2('cicuri') +
23         '&theoryuri=' + getParam2('theoryuri') +
24         '&processorURL=' + getParam2('processorURL') +
25         '&getterURL=' + getParam2('getterURL') +
26         '&UNICODEvsSYMBOL=' + getParam2('UNICODEvsSYMBOL');
27   var escaped_control_frame_URL = escape(control_frame_URL);
28   document.write('<frame src="' +
29         getParam2('processorURL') + 'apply' +
30         '?keys=RT' +
31         '&param.topurl=' + topurl +
32         '&xmluri=' + escaped_control_frame_URL + '" name="control"/>');
33   document.write('<frameset cols="50%,50%" border="0" scrolling="no">');
34   document.write('<frameset rows="11%,*" border="0" scrolling="no">');
35   document.write('<frame src="' +
36         getParam2('processorURL') + 'apply' +
37         '?keys=GP' +
38         //'&xmluri=' + location.protocol + "//" + location.host + chopSlash(location.pathname) + "/header.html" +
39         '&xmluri=' + topurl + '/html/library/header.html' +
40         '&param.uri=' + getParam2('theoryuri') + 
41         '" name="theoryheader"/>');
42   document.write('<frame src="' +
43         getParam2('processorURL') + 'apply' +
44         '?keys=L2H' +
45         '&xmluri=' + escape(getParam2('getterURL') + 'ls?format=xml&baseuri=' + getParam2('theoryuri')) +
46         '&param.keys=L2H' +
47         '&param.uri=' + getParam2('theoryuri') +
48         '&param.getterURL=' + getParam2('getterURL') +
49         '&param.UNICODEvsSYMBOL=' + getParam2('UNICODEvsSYMBOL') +
50         '&param.target=theory' +
51         //'&param.interfaceURL=' + location.protocol + "//" + location.host + chopSlash(chopSlash(chopSlash(location.pathname))) + 
52         '&param.interfaceURL=' + topurl +
53         '" name="theoryresult"/>');
54   document.write('</frameset>');
55   document.write('<frameset rows="11%,*" border="0" scrolling="no">');
56   document.write('<frame src="' +
57         getParam2('processorURL') + 'apply' +
58         '?keys=GP' +
59         //'&xmluri=' + location.protocol + "//" + location.host + chopSlash(location.pathname) + "/header.html" +
60         '&xmluri=' + topurl + '/html/library/header.html' +
61         '&param.uri=' + getParam2('cicuri') + 
62         '" name="cicheader"/>');
63   document.write('<frame src="' +
64         getParam2('processorURL') + 'apply' +
65         '?keys=L2H' +
66         '&xmluri=' + escape(getParam2('getterURL') + 'ls?format=xml&baseuri=' + getParam2('cicuri')) +
67         '&param.keys=L2H' +
68         '&param.uri=' + getParam2('cicuri') +
69         '&param.getterURL=' + getParam2('getterURL') +
70         '&param.UNICODEvsSYMBOL=' + getParam2('UNICODEvsSYMBOL') +
71         '&param.target=cic' +
72         //'&param.interfaceURL=' + location.protocol + "//" + location.host + chopSlash(chopSlash(chopSlash(location.pathname))) +
73         '&param.interfaceURL=' + topurl +
74         '" name="cicresult"/>');
75   document.write('</frameset>');
76   document.write('</frameset>');
77   document.write('</frameset>');
78 ]]>
79 </script>
80
81 </html>