# HG changeset patch # User Mike Hansen # Date 1359046028 0 # Node ID e7977585b41795a1daaec1e6ef8f4fbed2eb0fda # Parent ea3e6391ceb450e8ce98614f96767a91f6244ff7 Fix it so that old URLs to the reference manual work diff --git a/doc/common/builder.py b/doc/common/builder.py --- a/doc/common/builder.py +++ b/doc/common/builder.py @@ -330,7 +330,8 @@ def html(self): """ After we've finished building the website index page, we copy - everything one directory up. + everything one directory up. Then, we walk the reference manual, + and add html files the """ DocBuilder.html(self) html_output_dir = self._output_dir('html') @@ -338,6 +339,68 @@ os.path.realpath(os.path.join(html_output_dir, '..')), ignore_errors=False) + self.create_html_redirects() + + def create_html_redirects(self): + """ + Writes a number of small HTML files of files which used to + exist before splitting the reference manual into multiple + documents. These just redirect to the correct file after the + splitting. + """ + # The simple html template which will cause a redirect to the + # correct file + html_template = """ + + """ + + reference_dir = os.path.abspath(os.path.join(self._output_dir('html'), + '..', 'reference')) + reference_builder = ReferenceBuilder('reference') + refdir = os.path.join(os.environ['SAGE_DOC'], 'en', 'reference') + for document in reference_builder.get_all_documents(refdir): + #path is the directory above reference dir + path = os.path.abspath(os.path.join(reference_dir, '..')) + + # the name of the subdocument + document_name = document.split('/')[1] + + # the sage directory within a subdocument, for example + # /path/to/.../output/html/en/reference/algebras/sage + sage_directory = os.path.join(path, document, 'sage') + + # Walk through all of the files in the sage_directory + for dirpath, dirnames, filenames in os.walk(sage_directory): + # a string like reference/algebras/sage/algebras + short_path = dirpath[len(path)+1:] + + # a string like sage/algebras + shorter_path = os.path.join(*short_path.split(os.sep)[2:]) + + #Make the shorter path directory + try: + os.makedirs(os.path.join(reference_dir, shorter_path)) + except OSError: + pass + + for filename in filenames: + if not filename.endswith('html'): + continue + + # the name of the html file we are going to create + redirect_filename = os.path.join(reference_dir, shorter_path, filename) + + # the number of levels up we need to use in the relative url + levels_up = len(os.path.split(shorter_path)) + + # the relative url that we will redirect to + redirect_url = "/".join(['..']*levels_up + [document_name, shorter_path, filename]) + + # write the html file which performs the redirect + with open(redirect_filename, 'w') as f: + f.write(html_template % redirect_url) + + def clean(self): """ When we clean the output for the website index, we need to