doc: remove old vendorized marked module and replace with 0.8.2

This change is needed because in 1.8.3 we are going to introduce Markdown tables
in the documentation (#3873 and #3921), and the old marked version did not
support generating them.

Instead of committing the marked source code here, we live install from npm if
needed via the Makefile.

n.b.: at the time of this change, marked latest version is 1.0.0, released a few
      days ago. I am updating to the version immediately before that (0.8.2),
      because in 1.0.0 the hyperlinks in the Table of Contents do not work
      (probably a bug in that version).

Makefile

@@ -6,7 +6,14 @@ docassets = $(addprefix out/,$(wildcard doc/assets/*))
 VERSION = $(shell node -e "console.log( require('./src/package.json').version )")
 UNAME := $(shell uname -s)
 
-docs: $(outdoc_files) $(docassets)
+ensure_marked_is_installed:
+	set -eu; \
+	hash npm; \
+	if [ $(shell npm list --prefix bin/doc >/dev/null 2>/dev/null; echo $$?) -ne "0" ]; then \
+		npm ci --prefix=bin/doc; \
+	fi
+
+docs: ensure_marked_is_installed $(outdoc_files) $(docassets)
 
 out/doc/assets/%: doc/assets/%
 	mkdir -p $(@D)