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

@@ -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",
+			"-/",
+			"",
+		]},
+}