Function pushStateStack

mini-code-edit/cm/mode/xquery/xquery.js:419–421

(state, newState)

  }
  
  function pushStateStack(state, newState) {
    state.stack.push(newState);
  }
  
  function popStateStack(state) {
    var popped = state.stack.pop();