]> matita.cs.unibo.it Git - helm.git/blob - helm/on-line/javascript/helmjsmenu.js
Bugfix in restore_from_channel, before this fix hashtable (which has uris as
[helm.git] / helm / on-line / javascript / helmjsmenu.js
1 // Global variables.
2 var HJMmenu;
3
4 function initializeMenu() {
5    HJMmenu =
6       document.getElementById ?
7          // A DOM browser
8          document.getElementById("HJMmenu").style
9       :  // Probably Netscape Navigator 4.0
10          document.HJMmenu;
11    HJMmenu.visibility="hidden";
12 }
13
14 function showMenu() {
15    HJMmenu.visibility="visible";
16 }
17
18 function hideMenu() {
19    HJMmenu.visibility="hidden";
20 }
21
22 function moveMenu(x,y) {
23  var y2 = y - 25;
24  var x2 = x - 25;
25  if (document.getElementById) {
26    // Not Netscape Navigator 4.0
27    HJMmenu.left = x2 + "px";
28    HJMmenu.top  = y2 + "px";
29  } else {
30    // Probably Netscape Navigator 4.0
31    HJMmenu.left = x2;
32    HJMmenu.top  = y2;
33  }
34 }
35
36 function getX(event) {
37    if(!event.pageX)
38       // Probably Internet Explorer
39       return event.clientX + document.body.scrollLeft;
40    else
41       // Probably Netscape Navigator
42       return event.pageX;
43 }
44
45 function getY(event) {
46    if(!event.pageY)
47       // Probably Internet Explorer
48       return event.clientY + document.body.scrollTop;
49    else
50       // Probably Netscape Navigator
51       return event.pageY;
52 }
53
54 if (!document.getElementById) {
55    // Probably Netscape Navigator
56    document.captureEvents(Event.MOUSEDOWN);
57    document.onmousedown = hideMenu;
58 }