From 0c08143a22134d6cc80593c9291210b060c93cf1 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Sun, 2 Feb 2020 10:40:25 -0500
Subject: [PATCH 1/3] Add fstar module

---
 init.example.el                |  1 +
 modules/lang/fstar/README.org  |  3 ++
 modules/lang/fstar/config.el   | 55 ++++++++++++++++++++++++++++++++++
 modules/lang/fstar/packages.el |  4 +++
 4 files changed, 63 insertions(+)
 create mode 100644 modules/lang/fstar/README.org
 create mode 100644 modules/lang/fstar/config.el
 create mode 100644 modules/lang/fstar/packages.el

diff --git a/init.example.el b/init.example.el
index 7fc2f63f9..7e970506d 100644
--- a/init.example.el
+++ b/init.example.el
@@ -121,6 +121,7 @@
        ;;ess               ; emacs speaks statistics
        ;;faust             ; dsp, but you get to keep your soul
        ;;fsharp           ; ML stands for Microsoft's Language
+       ;;fstar             ; (dependent) types and (monadic) effects and Z3
        ;;go                ; the hipster dialect
        ;;(haskell +dante)  ; a language that's lazier than I am
        ;;hy                ; readability of scheme w/ speed of python
diff --git a/modules/lang/fstar/README.org b/modules/lang/fstar/README.org
new file mode 100644
index 000000000..4f7c312b7
--- /dev/null
+++ b/modules/lang/fstar/README.org
@@ -0,0 +1,3 @@
+#+TITLE: :lang F*
+
+This module adds [[https://fstar-lang.org/][F*]] support, powered by [[https://github.com/FStarLang/fstar-mode.el][fstar-mode.el]].
diff --git a/modules/lang/fstar/config.el b/modules/lang/fstar/config.el
new file mode 100644
index 000000000..354d3d7b9
--- /dev/null
+++ b/modules/lang/fstar/config.el
@@ -0,0 +1,55 @@
+;;; lang/fstar/config.el -*- lexical-binding: t; -*-
+
+(after! fstar-mode
+  (set-lookup-handlers! 'fstar-mode
+    :definition #'fstar-jump-to-definition
+    :documentation #'fstar-doc-at-point-dwim)
+
+  (map! :map fstar-mode-map
+        :localleader
+        :desc "F* next" "]" #'fstar-subp-advance-next
+        :desc "F* go to point" "." #'fstar-subp-advance-or-retract-to-point
+        :desc "F* previous" "[" #'fstar-subp-retract-last
+        (:prefix ("p" . "proof")
+          :desc "go to point (lax)" "l" #'fstar-subp-advance-or-retract-to-point-lax
+          :desc "compile buffer (lax)" "b" #'fstar-subp-advance-to-point-max-lax
+          "q" #'fstar-subp-kill-one-or-many
+          "k" #'fstar-subp-kill-z3
+          "r" #'fstar-subp-reload-to-point)
+
+        (:prefix ("l" . "layout")
+          "c"  #'fstar-quit-windows
+          "o"  #'fstar-outline)
+
+        ;; Moving around
+        "'" #'fstar-jump-to-related-error
+        (:prefix ("j" . "jump")
+          "j" #'fstar-jump-to-definition
+          "f" #'fstar-jump-to-definition-other-frame
+          "w" #'fstar-jump-to-definition-other-window
+          "e" #'fstar-jump-to-related-error
+          "F" #'fstar-jump-to-related-error-other-frame
+          "W" #'fstar-jump-to-related-error-other-window
+          "d" #'fstar-visit-dependency
+          "a" #'fstar-visit-interface-or-implementation
+          :desc "jump to first unprocessed line" "u" #'fstar-subp-goto-beginning-of-unprocessed)
+
+        ;; Help !!!
+        (:prefix ("h" . "help")
+          "y" #'fstar-copy-help-at-point
+          "w" #'fstar-browse-wiki
+          "W" #'fstar-browse-wiki-in-browser
+          "o" #'fstar-list-options
+          "p" #'fstar-quick-peek)
+
+        (:prefix ("a" . "ask (queries)")
+          "a" #'fstar-print
+          "e" #'fstar-eval
+          "E" #'fstar-eval-custom
+          "s" #'fstar-search
+          "d" #'fstar-doc)
+
+        (:prefix ("i" . "insert")
+          "m" #'fstar-insert-match-dwim
+          "M" #'fstar-insert-match)
+        ))
diff --git a/modules/lang/fstar/packages.el b/modules/lang/fstar/packages.el
new file mode 100644
index 000000000..2916c38be
--- /dev/null
+++ b/modules/lang/fstar/packages.el
@@ -0,0 +1,4 @@
+;; -*- no-byte-compile: t; -*-
+;;; lang/fstar.el
+
+(package! fstar-mode)

From 34f205c4da3e1e2edbb31ccb1965eda88f07c498 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Sun, 2 Feb 2020 14:08:55 -0500
Subject: [PATCH 2/3] Address issues from code review

---
 docs/modules.org               |  1 +
 modules/lang/fstar/README.org  | 57 +++++++++++++++++++++++++++++++++-
 modules/lang/fstar/packages.el |  2 +-
 3 files changed, 58 insertions(+), 2 deletions(-)

diff --git a/docs/modules.org b/docs/modules.org
index 5ec4128e7..bd552174c 100644
--- a/docs/modules.org
+++ b/docs/modules.org
@@ -109,6 +109,7 @@ Modules that bring support for a language or group of languages to Emacs.
 + [[file:../modules/lang/ess/README.org][ess]] - TODO
 + [[file:../modules/lang/faust/README.org][faust]] - TODO
 + [[file:../modules/lang/fsharp/README.org][fsharp]] - TODO
++ [[file:../modules/lang/fstar/README.org][fstar]] - F* support
 + [[file:../modules/lang/go/README.org][go]] =+lsp= - TODO
 + [[file:../modules/lang/haskell/README.org][haskell]] =+dante +intero +lsp= - TODO
 + hy - TODO
diff --git a/modules/lang/fstar/README.org b/modules/lang/fstar/README.org
index 4f7c312b7..e40b253cc 100644
--- a/modules/lang/fstar/README.org
+++ b/modules/lang/fstar/README.org
@@ -1,3 +1,58 @@
-#+TITLE: :lang F*
+#+TITLE: :lang fstar
 
+#+TITLE:   lang/fstar
+#+DATE:    February 2, 2020
+#+SINCE:   2.0.10
+#+STARTUP: inlineimages nofold
+
+* Table of Contents :TOC_3:noexport:
+- [[#description][Description]]
+  - [[#maintainers][Maintainers]]
+  - [[#module-flags][Module Flags]]
+  - [[#plugins][Plugins]]
+- [[#prerequisites][Prerequisites]]
+  - [[#f][F*]]
+    - [[#macos][macOS]]
+    - [[#arch-linux][Arch Linux]]
+- [[#features][Features]]
+- [[#configuration][Configuration]]
+- [[#troubleshooting][Troubleshooting]]
+
+* Description
 This module adds [[https://fstar-lang.org/][F*]] support, powered by [[https://github.com/FStarLang/fstar-mode.el][fstar-mode.el]].
+
++ Syntax highlighting
++ Interactively process F* files one definition at a time
++ Query the running F* process to look up definitions, documentation, and
+  theorems
+
+** Maintainers
++ [[https://github.com/tchajed][@tchajed]] (Author)
+
+** Module Flags
+This module provides no flags.
+
+** Plugins
++ [[https://github.com/FStarLang/fstar-mode.el][fstar-mode]]
+
+* Prerequisites
+** F*
+While fstar-mode supports the latest release of F*, you may have a better
+experience installing a more recent version from source. See F*'s [[https://github.com/FStarLang/FStar/blob/master/INSTALL.md][INSTALL.md]].
+*** macOS
+#+BEGIN_SRC sh
+brew install fstar
+#+END_SRC
+*** Arch Linux
+Install ~fstar~ from the AUR:
+#+BEGIN_SRC sh
+yaourt -S fstar
+#+END_SRC
+
+* Features
+
+* Configuration
+
+* Troubleshooting
+If you're having trouble getting F* to start correctly, you may need to
+configure a few variables in fstar-mode; see its [[https://github.com/FStarLang/fstar-mode.el][README]] for more details.
diff --git a/modules/lang/fstar/packages.el b/modules/lang/fstar/packages.el
index 2916c38be..80c8aa533 100644
--- a/modules/lang/fstar/packages.el
+++ b/modules/lang/fstar/packages.el
@@ -1,4 +1,4 @@
 ;; -*- no-byte-compile: t; -*-
-;;; lang/fstar.el
+;;; lang/fstar/packages.el
 
 (package! fstar-mode)

From eabbae7e395787db0af04732a2689a2692d57aa9 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Fri, 7 Feb 2020 16:23:31 -0500
Subject: [PATCH 3/3] Remove redundant title

---
 modules/lang/fstar/README.org | 2 --
 1 file changed, 2 deletions(-)

diff --git a/modules/lang/fstar/README.org b/modules/lang/fstar/README.org
index e40b253cc..30b025eaa 100644
--- a/modules/lang/fstar/README.org
+++ b/modules/lang/fstar/README.org
@@ -1,5 +1,3 @@
-#+TITLE: :lang fstar
-
 #+TITLE:   lang/fstar
 #+DATE:    February 2, 2020
 #+SINCE:   2.0.10