   `(when (fboundp 'cl-assert)
      (cl-assert ,@args)))
 
+(unless (featurep 'subr-x)
+  (defsubst string-trim-left (string)
+    "Remove leading whitespace from STRING."
+    (if (string-match "\\`[ \t\n\r]+" string)
+        (replace-match "" t t string)
+      string))
+  (defsubst string-trim-right (string)
+    "Remove trailing whitespace from STRING."
+    (if (string-match "[ \t\n\r]+\\'" string)
+        (replace-match "" t t string)
+      string))
+  (defsubst string-trim (string)
+    "Remove leading and trailing whitespace from STRING."
+    (string-trim-left (string-trim-right string))))
+
 ;;; Group
 
 (defgroup fstar nil


(defconst fstar-known-modules
  '((font-lock   . "Syntax highlighting")
    (prettify    . "Unicode math (e.g. display forall as ∀)")
    (indentation . "Indentation (based on control points)")
    (comments    . "Comment syntax and special comments ('(***', '(*+', etc.)")
    (flycheck    . "Real-time verification (good for small files)")
    (interactive . "Interactive verification (à la Proof-General)"))
  "Available components of F*-mode.")

(defcustom fstar-enabled-modules (mapcar #'car fstar-known-modules)

(defun fstar-setup-interactive ()
  "Setup interactive F* mode."
  (fstar-subp-refresh-keybindings fstar-interactive-keybinding-style)
  (when (featurep 'flycheck)
    (flycheck-mode -1)))

;;; Comment syntax

