X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fon-line%2Fjavascript%2Fprelude.js;h=83cff42bc5d2541db61bc284aaff3a50a0166093;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=69479641cd5af9ee32d8ae20aa3d678ee60df6d6;hpb=8c6ff8f373e6f65f553c05c93c537d3cb1670feb;p=helm.git diff --git a/helm/on-line/javascript/prelude.js b/helm/on-line/javascript/prelude.js index 69479641c..83cff42bc 100644 --- a/helm/on-line/javascript/prelude.js +++ b/helm/on-line/javascript/prelude.js @@ -27,6 +27,49 @@ function getInitialGetterURL() return getterURL; } +function getInitialProofCheckerURL() +{ + var search = top.location.search; + search = search.slice(1); + var args = search.split("&"); + var proofcheckerURL = "-1"; + for (var i = 0 ; i < args.length ; i++) { + var couple = args[i].split("="); + if (couple[0] == "proofcheckerURL") proofcheckerURL = couple[1]; + } + if (proofcheckerURL == "-1") + proofcheckerURL = getDefaultParam("proofcheckerURL"); + return proofcheckerURL; +} + +function getInitialDrawGraphURL() +{ + var search = top.location.search; + search = search.slice(1); + var args = search.split("&"); + var draw_graphURL = "-1"; + for (var i = 0 ; i < args.length ; i++) { + var couple = args[i].split("="); + if (couple[0] == "draw_graphURL") draw_graphURL = couple[1]; + } + if (draw_graphURL == "-1") draw_graphURL = getDefaultParam("draw_graphURL"); + return draw_graphURL; +} + +function getInitialURISetQueueURL() +{ + var search = top.location.search; + search = search.slice(1); + var args = search.split("&"); + var uri_set_queueURL = "-1"; + for (var i = 0 ; i < args.length ; i++) { + var couple = args[i].split("="); + if (couple[0] == "uri_set_queueURL") uri_set_queueURL = couple[1]; + } + if (uri_set_queueURL == "-1") uri_set_queueURL = getDefaultParam("uri_set_queueURL"); + return uri_set_queueURL; +} + function getInitialUNICODEvsSYMBOL() { var search = top.location.search; @@ -67,6 +110,21 @@ function getGetterURL() return document.getterURL.elements[0].value; } +function getProofCheckerURL() +{ + return document.proofcheckerURL.elements[0].value; +} + +function getDrawGraphURL() +{ + return document.draw_graphURL.elements[0].value; +} + +function getURISetQueueURL() +{ + return document.uri_set_queueURL.elements[0].value; +} + function getUNICODEvsSYMBOL() { if (document.UNICODEvsSYMBOL.radioUNICODEvsSYMBOL[0].checked) @@ -128,6 +186,9 @@ function refreshLinks() "&mode=" + mode + "&processorURL=" + getUwoboURL() + "&getterURL=" + getGetterURL() + + "&proofcheckerURL=" + getProofCheckerURL() + + "&draw_graphURL=" + getDrawGraphURL() + + "&uri_set_queueURL=" + getURISetQueueURL() + "&UNICODEvsSYMBOL=" + getUNICODEvsSYMBOL() ); } @@ -137,7 +198,7 @@ function selectUwoboURL(ss) if (ss.selectedIndex == 0) { document.uwoboURL.elements[0].value = ""; } else { - document.uwoboURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":8080/helm/servlet/uwobo/"; + document.uwoboURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":8081/helm/servlet/uwobo/"; } refreshLinks(); @@ -148,7 +209,40 @@ function selectGetterURL(ss) if (ss.selectedIndex == 0) { document.getterURL.elements[0].value = ""; } else { - document.getterURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":8081/"; + document.getterURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":48081/"; + } + + refreshLinks(); +} + +function selectProofCheckerURL(ss) +{ + if (ss.selectedIndex == 0) { + document.proofcheckerURL.elements[0].value = ""; + } else { + document.proofcheckerURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":48084/"; + } + + refreshLinks(); +} + +function selectDrawGraphURL(ss) +{ + if (ss.selectedIndex == 0) { + document.draw_graphURL.elements[0].value = ""; + } else { + document.draw_graphURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":48083/"; + } + + refreshLinks(); +} + +function selectURISetQueueURL(ss) +{ + if (ss.selectedIndex == 0) { + document.uri_set_queueURL.elements[0].value = ""; + } else { + document.uri_set_queueURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":48082/"; } refreshLinks();