|
| 1 | +# Copyright 2018-2019 Espressif Systems (Shanghai) PTE LTD |
| 2 | +# |
| 3 | +# Licensed under the Apache License, Version 2.0 (the "License"); |
| 4 | +# you may not use this file except in compliance with the License. |
| 5 | +# You may obtain a copy of the License at |
| 6 | +# |
| 7 | +# http://www.apache.org/licenses/LICENSE-2.0 |
| 8 | +# |
| 9 | +# Unless required by applicable law or agreed to in writing, software |
| 10 | +# distributed under the License is distributed on an "AS IS" BASIS, |
| 11 | +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
| 12 | +# See the License for the specific language governing permissions and |
| 13 | +# limitations under the License. |
| 14 | +# |
| 15 | + |
| 16 | + |
| 17 | +# Mechanism to generate static HTML redirect pages in the output |
| 18 | +# |
| 19 | +# Uses redirect_template.html and the list of pages given in |
| 20 | +# conf.html_redirect_pages |
| 21 | +# |
| 22 | +# Adapted from ideas in https://tech.signavio.com/2017/managing-sphinx-redirects |
| 23 | +import os.path |
| 24 | + |
| 25 | +from sphinx.builders.html import StandaloneHTMLBuilder |
| 26 | + |
| 27 | +REDIRECT_TEMPLATE = """ |
| 28 | +<html> |
| 29 | + <head> |
| 30 | + <meta http-equiv="refresh" content="0; url=$NEWURL" /> |
| 31 | + <script> |
| 32 | + window.location.href = "$NEWURL" |
| 33 | + </script> |
| 34 | + </head> |
| 35 | + <body> |
| 36 | + <p>Page has moved <a href="$NEWURL">here</a>.</p> |
| 37 | + </body> |
| 38 | +</html> |
| 39 | +""" |
| 40 | + |
| 41 | + |
| 42 | +def setup(app): |
| 43 | + app.add_config_value('html_redirect_pages', [], 'html') |
| 44 | + app.connect('build-finished', create_redirect_pages) |
| 45 | + |
| 46 | + |
| 47 | +def create_redirect_pages(app, docname): |
| 48 | + if not isinstance(app.builder, StandaloneHTMLBuilder): |
| 49 | + return # only relevant for standalone HTML output |
| 50 | + |
| 51 | + for (old_url, new_url) in app.config.html_redirect_pages: |
| 52 | + print("Creating redirect %s to %s..." % (old_url, new_url)) |
| 53 | + if old_url.startswith('/'): |
| 54 | + print("Stripping leading / from URL in config file...") |
| 55 | + old_url = old_url[1:] |
| 56 | + |
| 57 | + new_url = app.builder.get_relative_uri(old_url, new_url) |
| 58 | + out_file = app.builder.get_outfilename(old_url) |
| 59 | + print("HTML file %s redirects to relative URL %s" % (out_file, new_url)) |
| 60 | + |
| 61 | + out_dir = os.path.dirname(out_file) |
| 62 | + if not os.path.exists(out_dir): |
| 63 | + os.makedirs(out_dir) |
| 64 | + |
| 65 | + content = REDIRECT_TEMPLATE.replace("$NEWURL", new_url) |
| 66 | + |
| 67 | + with open(out_file, "w") as rp: |
| 68 | + rp.write(content) |
0 commit comments