(function(mod) {
  if (typeof exports == "object" && typeof module == "object") // CommonJS
    mod(require("../../lib/codemirror"));
  else if (typeof define == "function" && define.amd) // AMD
    define(["../../lib/codemirror"], mod);
  else // Plain browser env
    mod(CodeMirror);
})(function(CodeMirror) {
  "use strict";

  CodeMirror.defineMode('coq', function(_config, parserConfig) {

    var vernacular = [
      'Add', 'All', 'Arguments', 'Axiom',
      'Bind',
      'Canonical', 'Check', 'Class', 'Close', 'Coercion', 'CoFixpoint',
      'CoInductive', 'Context', 'Contextual', 'Corollary',
      'Defined', 'Definition', 'Delimit',
      'Eval',
      'End', 'Example', 'Export',
      'Fact', 'Fixpoint',
      'Global', 'Goal', 'Graph',
      'Hint', 'Hypotheses', 'Hypothesis',
      'Implicit', 'Implicits', 'Import', 'Inductive', 'Infix', 'Instance',
      'Lemma', 'Let', 'Local', 'Ltac',
      'Module', 'Morphism',
      'Notation',
      'Open',
      'Parameter', 'Parameters', 'Prenex', 'Print', 'Printing', 'Program',
      'Projections', 'Proof',
      'Proposition',
      'Qed',
      'Record', 'Relation', 'Remark', 'Require', 'Reserved', 'Resolve', 'Rewrite',
      'Save', 'Scope', 'Search', 'Section', 'Set', 'Show', 'Strict', 'Structure',
      'Tactic', 'Theorem',
      'Unset',
      'Variable', 'Variables', 'View',
    ];

    var gallina = [
      'as',
      'cofix',
      'else', 'end', 'exists',
      'fix', 'for', 'forall',
      'if', 'in', 'is',
      'let',
      'match',
      'of',
      'return',
      'struct',
      'then',
      'when', 'with',
    ];

    var tactics = [
      'after', 'apply', 'assert', 'auto', 'autorewrite',
      'case', 'change', 'clear', 'compute', 'congruence', 'constructor',
      'cut', 'cutrewrite',
      'dependent', 'destruct',
      'eapply', 'eassumption', 'eauto', 'econstructor', 'elim',
      'field', 'firstorder', 'fold', 'fourier',
      'generalize',
      'hnf',
      'induction', 'injection', 'intro', 'intros', 'inversion',
      'left',
      'move',
      'pattern', 'pose',
      'refine', 'remember', 'rename', 'replace', 'revert', 'rewrite',
      'right', 'ring',
      'set', 'simpl', 'specialize', 'split', 'subst', 'symmetry',
      'transitivity', 'trivial',
      'unfold', 'unlock', 'using',
    ];

    var terminators = [
      'assumption',
      'contradiction',
      'discriminate',
      'exact',
      'omega',
      'reflexivity',
      'tauto',
    ];

    var admitters = [
      'admit',
      'Admitted',
    ];

    var words = {};
    vernacular.map(function(word){words[word] = 'builtin';});
    gallina.map(function(word){words[word] = 'keyword';});
    tactics.map(function(word){words[word] = 'tactic';});
    terminators.map(function(word){words[word] = 'terminator';});
    admitters.map(function(word){words[word] = 'keyword';});
    
//        'let': 'keyword',
//        'print_endline': 'builtin',
//        'true': 'atom',

    function tokenBase(stream, state) {
      // console.log('tokenBase', stream, state);
      var ch = stream.next();

      if (ch === '"') {
        state.tokenize = tokenString;
        return state.tokenize(stream, state);
      }

      if (ch === '(') {
        if (stream.eat('*')) {
          state.commentLevel++;
          state.tokenize = tokenComment;
          return state.tokenize(stream, state);
        }
      }

      if (ch === '~') {
        stream.eatWhile(/\w/);
        return 'variable-2';
      }

      if (ch === '`') {
        stream.eatWhile(/\w/);
        return 'quote';
      }

      if (/\d/.test(ch)) {
        stream.eatWhile(/[\d]/);
        /*
        if (stream.eat('.')) {
          stream.eatWhile(/[\d]/);
        }
        */
        return 'number';
      }

      if ( /[+\-*&%=<>!?|]/.test(ch)) {
        return 'operator';
      }

      stream.eatWhile(/\w/);
      var cur = stream.current();
      return words.hasOwnProperty(cur) ? words[cur] : 'variable';
    }

    function tokenString(stream, state) {
      // console.log('tokenString', stream, state);
      var next, end = false, escaped = false;
      while ((next = stream.next()) != null) {
        if (next === '"' && !escaped) {
          end = true;
          break;
        }
        escaped = !escaped && next === '\\';
      }
      if (end && !escaped) {
        state.tokenize = tokenBase;
      }
      return 'string';
    }

    function tokenComment(stream, state) {
      // console.log('tokenComment', stream, state);
      var prev, next;
      while(state.commentLevel > 0 && (next = stream.next()) != null) {
        if (prev === '(' && next === '*') state.commentLevel++;
        if (prev === '*' && next === ')') state.commentLevel--;
        prev = next;
      }
      if (state.commentLevel <= 0) {
        state.tokenize = tokenBase;
      }
      return 'comment';
    }

    return {
      startState: function() {
        return {tokenize: tokenBase, commentLevel: 0};
      },
      token: function(stream, state) {
        if (stream.eatSpace()) return null;
        return state.tokenize(stream, state);
      },
      blockCommentStart: "(*",
      blockCommentEnd: "*)",
      lineComment: null
    };
  });

  CodeMirror.defineMIME('text/x-coq', {
    name: 'coq',
  });

});

@@ -3010,81 +3010,153 @@
     
-// console.log('tokenBase', stream, state);%0A      var ch = stream.next();
+var ch = stream.next();%0A%0A      if(ch === '.') %7B%0A        state.tokenize = tokenStatementEnd;%0A        return state.tokenize(stream, state);%0A      %7D
 %0A%0A  
@@ -4096,60 +4096,8 @@
 ) %7B%0A
-      // console.log('tokenString', stream, state);%0A
     
@@ -4477,61 +4477,8 @@
 ) %7B%0A
-      // console.log('tokenComment', stream, state);%0A
     
@@ -4832,24 +4832,197 @@
 nt';%0A    %7D%0A%0A
+    function tokenStatementEnd(stream, state) %7B%0A      state.tokenize = tokenBase;%0A      if(stream.eol() %7C%7C stream.match(/%5Cs/, false))%0A        return 'statementend';%0A%0A    %7D%0A%0A
     return %7B
@@ -5393,16 +5393,16 @@
 coq', %7B%0A
+
     name
@@ -5408,17 +5408,16 @@
 e: 'coq'
-,
 %0A  %7D);%0A%0A

Add token for end of statement.