 
 (defun fstar-setup-fontlock ()
   "Setup font-lock for use with F*."
-  (font-lock-add-keywords
-   nil `((,fstar-syntax-constants . 'font-lock-constant-face)
-         (,fstar-syntax-keywords  . 'font-lock-keyword-face)
-         (,fstar-syntax-builtins  . 'font-lock-builtin-face)
-         (,fstar-syntax-structure . 'tuareg-font-lock-governing-face)
-         ,@fstar-syntax-additional)))
-
-(define-derived-mode fstar-mode tuareg-mode "F✪"
+  (setq font-lock-defaults
+        `(((,fstar-syntax-constants . 'font-lock-constant-face)
+           (,fstar-syntax-types     . 'font-lock-type-face)
+           (,fstar-syntax-keywords  . 'font-lock-keyword-face)
+           (,fstar-syntax-builtins  . 'font-lock-builtin-face)
+           (,fstar-syntax-structure . 'fstar-structure-face)
+           ,@fstar-syntax-additional)
+          nil nil))
+  (font-lock-set-defaults))
+
+(defun fstar-setup-indentation ()
+  "Setup indentation for F*."
+  (setq-local indent-line-function #'fstar-indent)
+  (electric-indent-mode -1))
+
+(define-derived-mode fstar-mode prog-mode "F✪"
+  (fstar-setup-fontlock)
   (fstar-setup-prettify)
-  (fstar-setup-fontlock))
+  (fstar-setup-indentation)
+  (flycheck-mode))
 
 (add-to-list 'auto-mode-alist '("\\.fst\\'" . fstar-mode))
 


;; Copyright (C) 2015 Clément Pit--Claudel
;; Author: Clément Pit--Claudel <clement.pitclaudel@live.com>
;; URL: https://github.com/boogie-org/boogie-friends/

;; Keywords: convenience, languages

;; This file is not part of GNU Emacs.

;; Permission is hereby granted, free of charge, to any person obtaining a copy
;; of this software and associated documentation files (the "Software"), to deal
;; in the Software without restriction, including without limitation the rights
;; to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
;; copies of the Software, and to permit persons to whom the Software is
;; furnished to do so, subject to the following conditions:

;; The above copyright notice and this permission notice shall be included in all
;; copies or substantial portions of the Software.

;; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
;; IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
;; FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
;; AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
;; LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
;; OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
;; SOFTWARE.

;;; Commentary:



(add-to-list 'flycheck-checkers 'fstar)

;;; Prettify symbols

(defconst fstar-symbols-alist '(("exists" . ?∃) ("forall" . ?∀) ("fun" . ?λ)
                                ("nat" . ?ℕ) ("int" . ?ℤ)
                                ("True" . ?⊤) ("False" . ?⊥)
                                ("*" . ?×) ("~>" . ?↝)
                                ("<=" . ?≤) (">=" . ?≥) ("::" . ?⸬)
                                ("/\\" . ?∧) ("\\/" . ?∨) ("=!=" . ?≠)
                                ("&&" . ?∧) ("||" . ?∨) ("<>" . ?≠)
                                ("<==>" . ?⟺) ("==>" . ?⟹)
                                ("=>" . ?⇒) ("->" . ?→)
                                ("'a" . ?α) ("'b" . ?β) ("'c" . ?γ)
                                ("'d" . ?δ) ("'e" . ?η))
  "Fstar symbols.")

;;; font-lock
