doc: Add copy button to code blocks (#1604)

Add a Sphinx extension to show a copy button in the code blocks. The
text copied excludes the number of line and prompt characters in console
blocks.

.github/workflows/build-deploy-documentation.yml

@@ -25,18 +25,21 @@ jobs:
         with:
           submodules: recursive
 
-      #
-      # Build documentation installing first 'furo' theme dependencies
-      #
+      - name: Add sphinx dependencies
+        run: |
+          echo furo >> documentation/requirements.txt
+          echo sphinx-copybutton >> documentation/requirements.txt
 
-      - uses: ammaraskar/sphinx-action@master
+      - name: Build documentation
+        uses: ammaraskar/sphinx-action@master
         with:
-          pre-build-command: "echo furo >> documentation/requirements.txt"
           docs-folder: "documentation"
 
+      - name: Bypassing Jekyll on GH pages
+        run: |
+          sudo touch documentation/_build/html/.nojekyll
+
       - name: Deploy documents to GH pages
         uses: JamesIves/github-pages-deploy-action@v4
         with:
           folder: documentation/_build/html
-
-

.github/workflows/build-documentation.yml

@@ -25,12 +25,12 @@ jobs:
         with:
           submodules: recursive
 
-      #
-      # Build documentation installing first 'furo' theme dependencies
-      #
+      - name: Add sphinx dependencies
+        run: |
+          echo furo >> documentation/requirements.txt
+          echo sphinx-copybutton >> documentation/requirements.txt
 
-      - uses: ammaraskar/sphinx-action@master
+      - name: Build documentation
+        uses: ammaraskar/sphinx-action@master
         with:
-          pre-build-command: "echo furo >> documentation/requirements.txt"
-          docs-folder: "documentation"
-
+          docs-folder: "documentation"

documentation/README.rst

@@ -28,6 +28,11 @@ You may also need ``python-dateutil``.
 
     sudo pip3 install python-dateutil
 
+And ``sphinx-copybutton`` to show a copy button in code blocks::
+
+    sudo pip3 install sphinx-copybutton
+
+
 Building
 ========
 

documentation/source/conf.py

@@ -23,6 +23,7 @@
     'dylan.domain',
     'sphinx.ext.graphviz',
     'sphinx.ext.intersphinx',
+    'sphinx_copybutton',
 ]
 primary_domain = 'dylan'
 exclude_patterns = [
@@ -51,3 +52,9 @@
 html_title = 'Open Dylan'
 html_static_path = ['_static']
 html_favicon = '_static/favicon.ico'
+
+# -- Options for copybutton -------------------------------------------------
+# https://sphinx-copybutton.readthedocs.io/en/latest/use.html
+
+# Skip line numbers and prompt characters
+copybutton_exclude = '.linenos, .gp'