Update design docs and CI to use the new offline tags.json functionality

Author: ychin

.github/workflows/ci.yaml

@@ -59,7 +59,7 @@ jobs:
           echo "Version string: $version_string"
 
           cd vimhelp
-          python3 scripts/h2h.py -i "$MACVIM_DIR/runtime/doc" -o ../build --project macvim --web-version --version "$version_string" --commit "$MACVIM_COMMIT"
+          python3 scripts/h2h.py -i "$MACVIM_DIR/runtime/doc" -o ../build --project macvim --web-version --output-tags-json --version "$version_string" --commit "$MACVIM_COMMIT"
 
       - name: Upload page artifact
         uses: actions/upload-pages-artifact@v1

notes/Design_Notes.md

@@ -6,6 +6,13 @@ Neovim's documentation generation tool (hosted at https://neovim.io/doc/user/) w
 
 There were other tools like vim-jp's https://github.com/vim-jp/vimdoc-en, but vimhelp seemed to be the most used and provided the features we need.
 
+## Offline functionality
+
+vimhelp was modified to export a tags.json file during build. This file embeds all the tags mapping which allows us to query which tag should map where, without needing to rely on a dynamic server like vimhelp.org uses.
+
+- We also generate a redirect.html page which has tags.json embedded, and it allows us to do client-side redirecting. If you go to `redirect.html?tag=showdefinition()`, it will look up the tag in JavaScript and redirect the page as need be. This allows us to make a permalink that will always point to the correct tag location even if the tag gets moved to another file later on. Only issue is that this relies on JavaScript being enabled (which some users may have disabled).
+- We also use tags.json to faciliate the "Go to keyword" search box, which on vimhelp.org is a server query. It works by downloading the JSON file and doing client-side matching in JS.
+
 ## CI
 
 Publish the documentation using GitHub pages for simplicity and so we don't have to run a server. Since everything is generated by vimhelp, we don't really need an intermediate step of pushing to a gh-pages branch first. Instead, GitHub has a newer feature that allows us to directly publish the page as an artifact and deploy from it, thus saving us from having to push to a gh-pages branch, which would actually have bogged down the repo by storing useless history.