Function pushToken

static/editor.md/lib/codemirror/mode/erlang/erlang.js:417–423

(state,token)

  }

  function pushToken(state,token) {

    if (!(token.type == "comment" || token.type == "whitespace")) {
      state.tokenStack = maybe_drop_pre(state.tokenStack,token);
      state.tokenStack = maybe_drop_post(state.tokenStack);
    }
  }

  function maybe_drop_pre(s,token) {
    var last = s.length-1;