]> matita.cs.unibo.it Git - helm.git/blob - helm/on-line/html/library/index.html
...
[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         '&draw_graphURL=' + getParam2('draw_graphURL') +
27         '&uri_set_queueURL=' + getParam2('uri_set_queueURL') +
28         '&UNICODEvsSYMBOL=' + getParam2('UNICODEvsSYMBOL');
29   var escaped_control_frame_URL = escape(control_frame_URL);
30   document.write('<frame src="' +
31         getParam2('processorURL') + 'apply' +
32         '?keys=RT' +
33         '&param.topurl=' + topurl +
34         '&xmluri=' + escaped_control_frame_URL + '" name="control"/>');
35   document.write('<frameset cols="50%,50%" border="0" scrolling="no">');
36   document.write('<frameset rows="11%,*" border="0" scrolling="no">');
37   document.write('<frame src="' +
38         getParam2('processorURL') + 'apply' +
39         '?keys=GP' +
40         //'&xmluri=' + location.protocol + "//" + location.host + chopSlash(location.pathname) + "/header.html" +
41         '&xmluri=' + topurl + '/html/library/header.html' +
42         '&param.uri=' + getParam2('theoryuri') + 
43         '" name="theoryheader"/>');
44   document.write('<frame src="' +
45         getParam2('processorURL') + 'apply' +
46         '?keys=L2H' +
47         '&xmluri=' + escape(getParam2('getterURL') + 'ls?format=xml&baseuri=' + getParam2('theoryuri')) +
48         '&param.keys=L2H' +
49         '&param.uri=' + getParam2('theoryuri') +
50         '&param.getterURL=' + getParam2('getterURL') +
51         '&param.draw_graphURL=' + getParam2('draw_graphURL') +
52         '&param.uri_set_queueURL='+getParam2('uri_set_queueURL') +
53         '&param.UNICODEvsSYMBOL=' + getParam2('UNICODEvsSYMBOL') +
54         '&param.target=theory' +
55         //'&param.interfaceURL=' + location.protocol + "//" + location.host + chopSlash(chopSlash(chopSlash(location.pathname))) + 
56         '&param.interfaceURL=' + topurl +
57         '" name="theoryresult"/>');
58   document.write('</frameset>');
59   document.write('<frameset rows="11%,*" border="0" scrolling="no">');
60   document.write('<frame src="' +
61         getParam2('processorURL') + 'apply' +
62         '?keys=GP' +
63         //'&xmluri=' + location.protocol + "//" + location.host + chopSlash(location.pathname) + "/header.html" +
64         '&xmluri=' + topurl + '/html/library/header.html' +
65         '&param.uri=' + getParam2('cicuri') + 
66         '" name="cicheader"/>');
67   document.write('<frame src="' +
68         getParam2('processorURL') + 'apply' +
69         '?keys=L2H' +
70         '&xmluri=' + escape(getParam2('getterURL') + 'ls?format=xml&baseuri=' + getParam2('cicuri')) +
71         '&param.keys=L2H' +
72         '&param.uri=' + getParam2('cicuri') +
73         '&param.getterURL=' + getParam2('getterURL') +
74         '&param.draw_graphURL=' + getParam2('draw_graphURL') +
75         '&param.uri_set_queueURL='+getParam2('uri_set_queueURL') +
76         '&param.UNICODEvsSYMBOL=' + getParam2('UNICODEvsSYMBOL') +
77         '&param.target=cic' +
78         //'&param.interfaceURL=' + location.protocol + "//" + location.host + chopSlash(chopSlash(chopSlash(location.pathname))) +
79         '&param.interfaceURL=' + topurl +
80         '" name="cicresult"/>');
81   document.write('</frameset>');
82   document.write('</frameset>');
83   document.write('</frameset>');
84 ]]>
85 </script>
86
87 </html>