Function parse_Separator

cat-home/src/main/webapp/assets/js/editor/worker-xquery.js:3393–3398

()

  }

  function parse_Separator()
  {
    eventHandler.startNonterminal("Separator", e0);
    shift(54);                      // ';'
    eventHandler.endNonterminal("Separator", e0);
  }

  function parse_Setter()
  {