// Le Javascript c'est à gerber.
function foc() {
  document.getElementById('tool').focus();
}