]> matita.cs.unibo.it Git - helm.git/blob - helm/on-line/javascript/prelude.js
Version modified
[helm.git] / helm / on-line / javascript / prelude.js
1
2 function getInitialProcessorURL()
3 {
4   var search = top.location.search;
5   search = search.slice(1);
6   var args = search.split("&");
7   var processorURL = "-1";
8   for (var i = 0 ; i < args.length ; i++) {
9      var couple = args[i].split("=");
10      if (couple[0] == "processorURL") processorURL = couple[1];
11   }
12   if (processorURL == "-1") processorURL = getDefaultParam("processorURL");
13   return processorURL;
14 }
15
16 function getInitialGetterURL()
17 {
18   var search = top.location.search;
19   search = search.slice(1);
20   var args = search.split("&");
21   var getterURL = "-1";
22   for (var i = 0 ; i < args.length ; i++) {
23      var couple = args[i].split("=");
24      if (couple[0] == "getterURL") getterURL = couple[1];
25   }
26   if (getterURL == "-1") getterURL = getDefaultParam("getterURL");
27   return getterURL;
28 }
29
30 function getInitialUNICODEvsSYMBOL()
31 {
32   var search = top.location.search;
33   search = search.slice(1);
34   var args = search.split("&");
35   var UNICODEvsSYMBOL = "-1";
36   for (var i = 0 ; i < args.length ; i++) {
37      var couple = args[i].split("=");
38      if (couple[0] == "UNICODEvsSYMBOL") UNICODEvsSYMBOL = couple[1];
39   }
40   if (UNICODEvsSYMBOL == "-1") UNICODEvsSYMBOL = getDefaultParam("UNICODEvsSYMBOL");
41   return UNICODEvsSYMBOL;
42 }
43
44 function getInitialUNICODEvsSYMBOLsymbol()
45 {
46   if (getInitialUNICODEvsSYMBOL() == "symbol")
47    return "CHECKED";
48   else
49    return "";
50 }
51
52 function getInitialUNICODEvsSYMBOLunicode()
53 {
54   if (getInitialUNICODEvsSYMBOL() == "unicode")
55    return "CHECKED";
56   else
57    return "";
58 }
59
60 function getUwoboURL()
61 {
62   return document.uwoboURL.elements[0].value;
63 }
64
65 function getGetterURL()
66 {
67   return document.getterURL.elements[0].value;
68 }
69
70 function getUNICODEvsSYMBOL()
71 {
72   if (document.UNICODEvsSYMBOL.radioUNICODEvsSYMBOL[0].checked)
73    return document.UNICODEvsSYMBOL.radioUNICODEvsSYMBOL[0].value;
74   else
75    return document.UNICODEvsSYMBOL.radioUNICODEvsSYMBOL[1].value;
76 }
77
78 function chopSlash(url)
79 {
80   return url.slice(0,url.lastIndexOf('/'));
81 }
82
83 function refreshLinks()
84 {
85   var search = top.location.search;
86   search = search.slice(1);
87   var args = search.split("&");
88   var cicuri = "-1", theoryuri = "-1", mode = "-1";
89   for (var i = 0 ; i < args.length ; i++) {
90      var couple = args[i].split("=");
91      switch (couple[0]) {
92         case "cicuri"       : cicuri     =couple[1]; break;
93         case "theoryuri"    : theoryuri  =couple[1]; break;
94         case "mode"         : mode       =couple[1]; break;
95      }
96   }
97   if (cicuri == "-1") cicuri = getDefaultParam("cicuri");
98   if (theoryuri == "-1") theoryuri = getDefaultParam("theoryuri");
99   if (mode == "-1") mode = getDefaultParam("mode");
100
101   document.links[2].search = "?getterURL=" + getGetterURL();
102   
103   document.links[3].search = 
104     "?processorURL=" + getUwoboURL() +
105     "&getterURL=" + getGetterURL();
106
107   var topurl =
108    chopSlash(chopSlash(
109     document.location.protocol + '//' +
110     document.location.host +
111     document.location.pathname));
112   document.links[4].href =
113      getUwoboURL() + "apply" +
114       "?keys=RT" +
115       "&param.topurl=" + topurl +
116       "&xmluri=" +
117       escape(
118        topurl + "/html/library/index.html" +
119        "?cicuri=" + cicuri +
120        "&theoryuri=" + theoryuri +
121        "&mode=" + mode +
122        "&processorURL=" + getUwoboURL() +
123        "&getterURL=" + getGetterURL() +
124        "&UNICODEvsSYMBOL=" + getUNICODEvsSYMBOL()
125       );
126 }
127
128 function selectUwoboURL(ss)
129 {
130   if (ss.selectedIndex == 0) {
131     document.uwoboURL.elements[0].value = "";
132   } else {
133     document.uwoboURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":8080/helm/servlet/uwobo/";
134   }
135
136   refreshLinks();
137 }
138
139 function selectGetterURL(ss)
140 {
141   if (ss.selectedIndex == 0) {
142     document.getterURL.elements[0].value = "";
143   } else {
144     document.getterURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":8081/";
145   }
146
147   refreshLinks();
148 }