]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/on-line/html/library/index.html
projects / helm.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
first moogle template checkin
[helm.git] / helm / on-line / html / library / index.html
diff --git a/helm/on-line/html/library/index.html b/helm/on-line/html/library/index.html
index 62d4b63a73cf445eeeba3a52ecdbc5a17119bb49..4f1be5faac96722d62bd4e524ea6e528284a63e0 100644 (file)
--- a/helm/on-line/html/library/index.html
+++ b/helm/on-line/html/library/index.html
@@ -1,63 +1,90 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
-"http://www.w3.org/TR/REC-html40/loose.dtd">
-<html>
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "DTD/xhtml1-strict.dtd">
+-->
+
+<html xmlns:subst="http://www.cs.unibo.it/helm/subst">
 <head>
- <script language="JavaScript" src="../../javascript/defaults.js"></script>
- <script language="JavaScript" src="../../javascript/utils.js"></script>
- <title>Index</script></title>
+<!-- Note: <subst:script/> are substitued by the stylesheet with <script />  -->
+<!-- after changing @src in the concatenation of the interface URL with @src -->
+<subst:script language="JavaScript" src="/javascript/defaults.js" />
+<subst:script language="JavaScript" src="/javascript/utils.js" />
+<title>Index</title>
 </head>
 <script>
+  var topurl = "<subst:topurl/>";
+<![CDATA[
   document.write('<frameset rows="18%,*" border="0" scrolling="no">');
-  document.write('<frame src="control.html' +
-       '?topurl=' + chopSlash(chopSlash(chopSlash(location.protocol + "//" + location.host + location.pathname))) +
-       '&mode=' + getParam('mode') +
-       '&cicuri=' + getParam('cicuri') +
-       '&theoryuri=' + getParam('theoryuri') +
-       '&processorURL=' + getParam('processorURL') +
-       '&getterURL=' + getParam('getterURL') +
-       '&UNICODEvsSYMBOL=' + getParam('UNICODEvsSYMBOL') +
-       '" name="control"/>');
+  var control_frame_URL=
+        topurl + '/html/library/control.html' +
+       '?topurl=' + topurl +
+       '&mode=' + getParam2('mode') +
+       '&cicuri=' + getParam2('cicuri') +
+       '&theoryuri=' + getParam2('theoryuri') +
+       '&processorURL=' + getParam2('processorURL') +
+       '&getterURL=' + getParam2('getterURL') +
+       '&proofcheckerURL=' + getParam2('proofcheckerURL') +
+       '&draw_graphURL=' + getParam2('draw_graphURL') +
+       '&uri_set_queueURL=' + getParam2('uri_set_queueURL') +
+       '&UNICODEvsSYMBOL=' + getParam2('UNICODEvsSYMBOL');
+  var escaped_control_frame_URL = escape(control_frame_URL);
+  document.write('<frame src="' +
+        getParam2('processorURL') + 'apply' +
+       '?keys=RT' +
+        '&param.topurl=' + topurl +
+        '&xmluri=' + escaped_control_frame_URL + '" name="control"/>');
   document.write('<frameset cols="50%,50%" border="0" scrolling="no">');
   document.write('<frameset rows="11%,*" border="0" scrolling="no">');
   document.write('<frame src="' +
-       getParam('processorURL') + 'apply' +
+       getParam2('processorURL') + 'apply' +
        '?keys=GP' +
-       '&xmluri=' + location.protocol + "//" + location.host + chopSlash(location.pathname) + "/header.html" +
-       '&param.uri=' + getParam('theoryuri') + 
+       //'&xmluri=' + location.protocol + "//" + location.host + chopSlash(location.pathname) + "/header.html" +
+       '&xmluri=' + topurl + '/html/library/header.html' +
+       '&param.uri=' + getParam2('theoryuri') + 
        '" name="theoryheader"/>');
   document.write('<frame src="' +
-       getParam('processorURL') + 'apply' +
+       getParam2('processorURL') + 'apply' +
        '?keys=L2H' +
-       '&xmluri=' + escape(getParam('getterURL') + 'ls?format=xml&baseuri=' + getParam('theoryuri')) +
+       '&xmluri=' + escape(getParam2('getterURL') + 'ls?format=xml&baseuri=' + getParam2('theoryuri')) +
         '&param.keys=L2H' +
-       '&param.uri=' + getParam('theoryuri') +
-       '&param.getterURL=' + getParam('getterURL') +
-       '&param.UNICODEvsSYMBOL=' + getParam('UNICODEvsSYMBOL') +
+       '&param.uri=' + getParam2('theoryuri') +
+       '&param.getterURL=' + getParam2('getterURL') +
+       '&param.proofcheckerURL=' + getParam2('proofcheckerURL') +
+       '&param.draw_graphURL=' + getParam2('draw_graphURL') +
+       '&param.uri_set_queueURL='+getParam2('uri_set_queueURL') +
+       '&param.UNICODEvsSYMBOL=' + getParam2('UNICODEvsSYMBOL') +
         '&param.target=theory' +
-       '&param.interfaceURL=' + location.protocol + "//" + location.host + chopSlash(chopSlash(chopSlash(location.pathname))) + 
+       //'&param.interfaceURL=' + location.protocol + "//" + location.host + chopSlash(chopSlash(chopSlash(location.pathname))) + 
+       '&param.interfaceURL=' + topurl +
        '" name="theoryresult"/>');
   document.write('</frameset>');
   document.write('<frameset rows="11%,*" border="0" scrolling="no">');
   document.write('<frame src="' +
-       getParam('processorURL') + 'apply' +
+       getParam2('processorURL') + 'apply' +
        '?keys=GP' +
-       '&xmluri=' + location.protocol + "//" + location.host + chopSlash(location.pathname) + "/header.html" +
-       '&param.uri=' + getParam('cicuri') + 
+       //'&xmluri=' + location.protocol + "//" + location.host + chopSlash(location.pathname) + "/header.html" +
+       '&xmluri=' + topurl + '/html/library/header.html' +
+       '&param.uri=' + getParam2('cicuri') + 
        '" name="cicheader"/>');
   document.write('<frame src="' +
-       getParam('processorURL') + 'apply' +
+       getParam2('processorURL') + 'apply' +
        '?keys=L2H' +
-       '&xmluri=' + escape(getParam('getterURL') + 'ls?format=xml&baseuri=' + getParam('cicuri')) +
+       '&xmluri=' + escape(getParam2('getterURL') + 'ls?format=xml&baseuri=' + getParam2('cicuri')) +
         '&param.keys=L2H' +
-       '&param.uri=' + getParam('cicuri') +
-       '&param.getterURL=' + getParam('getterURL') +
-       '&param.UNICODEvsSYMBOL=' + getParam('UNICODEvsSYMBOL') +
+       '&param.uri=' + getParam2('cicuri') +
+       '&param.getterURL=' + getParam2('getterURL') +
+       '&param.proofcheckerURL=' + getParam2('proofcheckerURL') +
+       '&param.draw_graphURL=' + getParam2('draw_graphURL') +
+       '&param.uri_set_queueURL='+getParam2('uri_set_queueURL') +
+       '&param.UNICODEvsSYMBOL=' + getParam2('UNICODEvsSYMBOL') +
         '&param.target=cic' +
-       '&param.interfaceURL=' + location.protocol + "//" + location.host + chopSlash(chopSlash(chopSlash(location.pathname))) +
+       //'&param.interfaceURL=' + location.protocol + "//" + location.host + chopSlash(chopSlash(chopSlash(location.pathname))) +
+       '&param.interfaceURL=' + topurl +
        '" name="cicresult"/>');
   document.write('</frameset>');
   document.write('</frameset>');
   document.write('</frameset>');
+]]>
 </script>
 
 </html>
Unnamed repository; edit this file 'description' to name the repository.