       fstar-search (fstar-subp-available-p)]
      ["Quick peek"
       fstar-quick-peek (fstar-subp-available-p)])
+    ("Literate F*"
+     ["Switch to reStructuredText mode"
+      fstar-literate-fst2rst])
     ("Utilities"
      ["Copy error message at point"
       fstar-copy-help-at-point])

  "Toggle between F* and reStructuredText."
  (interactive)
  (fstar-subp-kill)
  (setq-local fstar-literate--fst-name (buffer-name))
  (fstar-literate--toggle "--fst2rst" #'fstar-literate--rst-mode))

(defun fstar-literate-rst2fst ()
  "Toggle between reStructuredText and F*."
  (interactive)
  (fstar-literate--toggle "--rst2fst" #'fstar-mode))

(defun fstar-literate--marker-modification-hook (from to)
  "Handle backspace on literate comment marker.


;;; Literate F*

(defconst fstar-literate--point-marker
  "<<<\"P\"O\"I\"N\"T\">>>")

