From f55e456c84b615e1cbe9e9968fc27aeb1dd0ad37 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 29 Feb 2016 13:59:06 -0800
Subject: [PATCH] chore(*): remove remaining references to by+ and begin+

---
 src/emacs/lean-syntax.el             | 8 +-------
 src/frontends/lean/builtin_exprs.cpp | 2 +-
 src/frontends/lean/token_table.cpp   | 4 ++--
 src/vim/syntax/lean.vim              | 2 +-
 4 files changed, 5 insertions(+), 11 deletions(-)

diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index 8c564c37ca..21d693c07d 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -9,7 +9,7 @@
 
 (defconst lean-keywords1
   '("import" "prelude" "tactic_hint" "protected" "private" "noncomputable" "definition" "renaming"
-    "hiding" "exposing" "parameter" "parameters" "begin" "begin+" "proof" "qed" "conjecture" "constant" "constants"
+    "hiding" "exposing" "parameter" "parameters" "begin" "proof" "qed" "conjecture" "constant" "constants"
     "hypothesis" "lemma" "corollary" "variable" "variables" "premise" "premises" "theory"
     "print" "theorem" "proposition" "example" "abbreviation" "abstract"
     "open" "as" "export" "override" "axiom" "axioms" "inductive" "with" "structure" "record" "universe" "universes"
@@ -26,11 +26,6 @@
   "lean keywords ending with 'word' (not symbol)")
 (defconst lean-keywords1-regexp
   (eval `(rx word-start (or ,@lean-keywords1) word-end)))
-(defconst lean-keywords2
-  '("by+" "begin+")
-  "lean keywords ending with 'symbol'")
-(defconst lean-keywords2-regexp
-  (eval `(rx word-start (or ,@lean-keywords2) symbol-end)))
 (defconst lean-constants
   '("#" "@" "!" "->" "∼" "↔" "/" "==" "=" ":=" "<->" "/\\" "\\/" "∧" "∨"
     "≠" "<" ">" "≤" "≥" "¬" "<=" ">=" "⁻¹" "⬝" "▸" "+" "*" "-" "/" "λ"
@@ -170,7 +165,6 @@
      (,(rx (or "∘if")) . 'font-lock-constant-face)
      ;; Keywords
      ("\\(set_option\\)[ \t]*\\([^ \t\n]*\\)" (2 'font-lock-constant-face))
-     (,lean-keywords2-regexp . 'font-lock-keyword-face)
      (,lean-keywords1-regexp . 'font-lock-keyword-face)
      (,(rx word-start (group "example") ".") (1 'font-lock-keyword-face))
      (,(rx (or "∎")) . 'font-lock-keyword-face)
diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 9d863b0ab5..15bb28b70a 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -568,7 +568,7 @@ static expr parse_obtain(parser & p, unsigned, expr const *, pos_info const & po
     // When from_term is not just a constant or local constant, we compile obtain as:
     //
     //   have H : _, from from_term,
-    //   (by+ exact (obtain ps, from H, goal_term)) H
+    //   (by exact (obtain ps, from H, goal_term)) H
     //
     // Motivation, we want "from_term" (and its type) to be elaborated before processing the
     // obtain-expression
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 599cfd49d5..e7feb250ce 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -90,7 +90,7 @@ static char const * g_decreasing_unicode = "↓";
 void init_token_table(token_table & t) {
     pair<char const *, unsigned> builtin[] =
         {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"at", 0}, {"have", 0}, {"assert", 0}, {"suppose", 0}, {"show", 0}, {"suffices", 0}, {"obtain", 0},
-         {"if", 0}, {"then", 0}, {"else", 0}, {"by", 0}, {"by+", 0}, {"hiding", 0}, {"replacing", 0}, {"renaming", 0},
+         {"if", 0}, {"then", 0}, {"else", 0}, {"by", 0}, {"hiding", 0}, {"replacing", 0}, {"renaming", 0},
          {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
          {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec},
          {"{|", g_max_prec}, {"|}", 0}, {"(:", g_max_prec}, {":)", 0},
@@ -99,7 +99,7 @@ void init_token_table(token_table & t) {
          {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {"xrewrite", 0}, {"krewrite", 0},
          {"esimp", 0}, {"fold", 0}, {"unfold", 0}, {"note", 0}, {"with_options", 0}, {"with_attributes", 0}, {"with_attrs", 0},
          {"generalize", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", 0}, {"#tactic", 0},
-         {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"begin+", g_max_prec}, {"abstract", g_max_prec},
+         {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"abstract", g_max_prec},
          {"proof", g_max_prec}, {"qed", 0}, {"@@", g_max_prec}, {"@", g_max_prec},
          {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec},
          {"?(", g_max_prec}, {"⌞", g_max_prec}, {"⌟", 0}, {"match", 0},
diff --git a/src/vim/syntax/lean.vim b/src/vim/syntax/lean.vim
index 625af61b45..ec1ff6ce2a 100644
--- a/src/vim/syntax/lean.vim
+++ b/src/vim/syntax/lean.vim
@@ -24,7 +24,7 @@ syn case match
 " keywords
 syn keyword leanKeyword import prelude tactic_hint protected private noncomputable
 syn keyword leanKeyword definition renaming hiding exposing parameter parameters
-syn keyword leanKeyword begin "begin+" proof qed conjecture constant constants hypothesis lemma
+syn keyword leanKeyword begin proof qed conjecture constant constants hypothesis lemma
 syn keyword leanKeyword corollary variable variables premise premises theory print theorem proposition
 syn keyword leanKeyword example abbreviation abstract open as export override axiom axioms inductive
 syn keyword leanKeyword with structure record universe universes alias help environment options