Simplify `juvix html`

[janmasrovira]

juvix html has (too) many options. I believe many of them were introduced to facilitate integration with VSCode. We should somehow make the cli interface simpler and either adapt the VSCode plugin or drop direct support for it.

juvix html --help:

Usage: juvix html [--non-recursive] [--only-source] [--only-code]
                  [--theme THEME] [--output-dir OUTPUT_DIR] [--no-footer]
                  [--no-path] [--ext ARG] [--strip-prefix ARG]
                  [--folder-structure] [--prefix-assets ARG] [--prefix-url ARG]
                  [--prefix-id ARG] [--open] [JUVIX_FILE|JUVIX_MARKDOWN_FILE]

  Generate HTML for a Juvix file

Available options:
  --non-recursive          Do not process imported modules recursively
  --only-source            Generate only Html for the source code with syntax
                           highlighting
  --only-code              If --only-source is enabled, only generate the code
                           without the header and footer
  --theme THEME            Theme for syntax highlighting. Dark themes: nord,
                           macchiato. Light themes: ayu (default: ayu)
  --output-dir OUTPUT_DIR  Html output directory (default: html)
  --no-footer              Remove HTML Juvix footer
  --no-path                Remove the path from all hyperlinks
  --ext ARG                File extension for the generated HTML files
                           (default: ".html")
  --strip-prefix ARG       Strip the given prefix from the hyperlinks. This has
                           no effect if --no-path is enabled. It has precedence
                           over --prefix-url (default: "")
  --folder-structure       Generate HTML following the module's folder structure
  --prefix-assets ARG      Prefix used for assets's source path (default: "")
  --prefix-url ARG         Prefix used for inner Juvix hyperlinks (default: "")
  --prefix-id ARG          Prefix used for HTML element IDs (default: "")
  --open                   Open the documentation after generating it
  JUVIX_FILE|JUVIX_MARKDOWN_FILE
                           Path to a .juvix, .juvix.md file
  -h,--help                Show this help text

[jonaprieto]

Some of these flags are used when using the Juvix MkDocs plugin, for example, --folder-structure, --prefix-url to make the links work when processing, as far as I remember.

[paulcadman]

Let's move this command to juvix dev mkdocs-html and make a simpler interface for juvix html. Then update juvix-mkdocs to use the new command. juvix-docs would have to switch to a newer version of juvix-mkdocs before we can do this.