X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fon-line%2Fjavascript%2Fhelmjsmenu.js;fp=helm%2Fon-line%2Fjavascript%2Fhelmjsmenu.js;h=0000000000000000000000000000000000000000;hb=e108abe5c0b4eb841c4ad332229a6c0e57e70079;hp=0d765431551dfa06f88e24c1114b6f398c014c2a;hpb=1456c337a60f6677ee742ff7891d43fc382359a9;p=helm.git

diff --git a/helm/on-line/javascript/helmjsmenu.js b/helm/on-line/javascript/helmjsmenu.js
deleted file mode 100644
index 0d7654315..000000000
--- a/helm/on-line/javascript/helmjsmenu.js
+++ /dev/null
@@ -1,58 +0,0 @@
-// Global variables.
-var HJMmenu;
-
-function initializeMenu() {
-   HJMmenu =
-      document.getElementById ?
-         // A DOM browser
-         document.getElementById("HJMmenu").style
-      :  // Probably Netscape Navigator 4.0
-         document.HJMmenu;
-   HJMmenu.visibility="hidden";
-}
-
-function showMenu() {
-   HJMmenu.visibility="visible";
-}
-
-function hideMenu() {
-   HJMmenu.visibility="hidden";
-}
-
-function moveMenu(x,y) {
- var y2 = y - 25;
- var x2 = x - 25;
- if (document.getElementById) {
-   // Not Netscape Navigator 4.0
-   HJMmenu.left = x2 + "px";
-   HJMmenu.top  = y2 + "px";
- } else {
-   // Probably Netscape Navigator 4.0
-   HJMmenu.left = x2;
-   HJMmenu.top  = y2;
- }
-}
-
-function getX(event) {
-   if(!event.pageX)
-      // Probably Internet Explorer
-      return event.clientX + document.body.scrollLeft;
-   else
-      // Probably Netscape Navigator
-      return event.pageX;
-}
-
-function getY(event) {
-   if(!event.pageY)
-      // Probably Internet Explorer
-      return event.clientY + document.body.scrollTop;
-   else
-      // Probably Netscape Navigator
-      return event.pageY;
-}
-
-if (!document.getElementById) {
-   // Probably Netscape Navigator
-   document.captureEvents(Event.MOUSEDOWN);
-   document.onmousedown = hideMenu;
-}