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