From 49ba33e552ebe03482bd613e8264d88dbec2b040 Mon Sep 17 00:00:00 2001
From: Alex J Best <alex.j.best@gmail.com>
Date: Sun, 9 Jan 2022 16:18:24 +0000
Subject: [PATCH] feat(vscode): add a snippet for inserting a module docstring
 template (#11312)

We already have a vscode snippet for adding copyright headers, this PR adds a similar one to generate a default module docstring with many of the common sections stubbed out.

By default it takes the filename, converts underscores to spaces and capitalizes each word to create the title, as this seems a sensible default. But otherwise all text is a static default example following the documentation style page to make it easier to remember the various recommended secitons.

To test do `ctrl+shift+p` to open the command pallette, type insert snippet, enter, and type module and it should show up.

See also #3186
---
 .vscode/module-docstring.code-snippets | 35 ++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)
 create mode 100644 .vscode/module-docstring.code-snippets

diff --git a/.vscode/module-docstring.code-snippets b/.vscode/module-docstring.code-snippets
new file mode 100644
index 0000000000000..9d1ed00c162b4
--- /dev/null
+++ b/.vscode/module-docstring.code-snippets
@@ -0,0 +1,35 @@
+{
+	"Module docstring for mathlib": {
+		"scope": "lean",
+		"prefix": "module docstring",
+		"body": [
+			"/-!",
+      "# ${TM_FILENAME_BASE/([^_]*)(_?)/${1:/capitalize}${2:+ }/g}",
+			"",
+			"## Main definitions",
+			"",
+			"* `foo_bar`",
+			"",
+			"## Main statements",
+			"",
+			"* `foo_bar_unique`",
+			"",
+			"## Notation",
+			"",
+			"",
+			"",
+			"## Implementation details",
+			"",
+			"",
+			"",
+			"## References",
+			"",
+			"* [F. Bar, *Quuxes*][bibkey]",
+			"",
+			"## Tags",
+			"",
+			"Foobars, barfoos",
+			"-/",
+			"",
+		]},
+}