Skip to content

Commit 3b1c99d

Browse files
authoredSep 27, 2024
Merge branch 'develop' into pr/tobiasdiez/36524
2 parents 49dc635 + d1f99d1 commit 3b1c99d

File tree

3,572 files changed

+101103
-102356
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

3,572 files changed

+101103
-102356
lines changed
 

‎.ci/create-changes-html.sh

+50-28
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,14 @@
11
#!/bin/sh
22
if [ $# != 2 ]; then
3-
echo >&2 "usage: $0 BASE_DOC_COMMIT DOC_REPO"
4-
echo >&2 "creates CHANGES.html in the current directory"
5-
echo >&2 "for the diffs of DOC_REPO against BASE_DOC_COMMIT"
3+
echo >&2 "Usage: $0 DIFF_TEXT DOC_REPO"
4+
echo >&2 "This script generates a CHANGES.html file in the current directory"
5+
echo >&2 "and adds anchor targets in the documents within DOC_REPO"
6+
echo >&2 "based on the diff hunks in the DIFF_TEXT file."
67
exit 1
78
fi
8-
BASE_DOC_COMMIT="$1"
9+
DIFF_TEXT="$1"
910
DOC_REPOSITORY="$2"
1011

11-
# Wipe out chronic diffs between old doc and new doc
12-
(cd $DOC_REPOSITORY && find . -name "*.html" | xargs sed -i -e '\;<script type="application/vnd\.jupyter\.widget-state+json">;,\;</script>; d')
1312
# Create CHANGES.html
1413
echo '<html>' > CHANGES.html
1514
echo '<head>' >> CHANGES.html
@@ -19,79 +18,102 @@ echo '<script>hljs.highlightAll();</script>' >> CHANGES.html
1918
cat >> CHANGES.html << EOF
2019
<script>
2120
document.addEventListener('DOMContentLoaded', () => {
22-
const baseDocURL = 'https://sagemath.netlify.app'
21+
// This URL is hardcoded in the file .github/workflows/doc-publish.yml.
22+
// See NETLIFY_ALIAS of the "Deploy to Netlify" step.
23+
const baseDocURL = 'https://doc-develop--sagemath.netlify.app'
2324
const diffSite = 'https://pianomister.github.io/diffsite'
2425
const diffParagraphs = document.querySelectorAll('p.diff');
2526
diffParagraphs.forEach(paragraph => {
2627
const rootURL = window.location.origin;
27-
const docAnchor = paragraph.querySelector('a'); // first "a" element
28+
const docAnchor = paragraph.querySelector('a');
2829
const url = new URL(docAnchor.href);
2930
const path = url.pathname;
3031
const anchor = document.createElement('a');
3132
anchor.href = diffSite + '/?url1=' + rootURL + path + '&url2=' + baseDocURL + path;
3233
anchor.textContent = 'compare with the base';
3334
anchor.setAttribute('target', '_blank');
35+
paragraph.innerHTML += '&nbsp;&nbsp;';
3436
paragraph.appendChild(anchor);
35-
paragraph.innerHTML += '&nbsp;';
36-
const hunkAnchors = paragraph.querySelectorAll('a.hunk');
37-
hunkAnchors.forEach(hunkAnchor => {
37+
const hunks = paragraph.parentNode.querySelectorAll('p.hunk');
38+
hunks.forEach(hunk => {
39+
const hunkAnchor = hunk.querySelector('a');
3840
const url = new URL(hunkAnchor.href);
3941
const path = url.pathname;
4042
const pathHash = path + url.hash.replace('#', '%23');
4143
const anchor = document.createElement('a');
4244
anchor.href = diffSite + '/?url1=' + rootURL + pathHash + '&url2=' + baseDocURL + path;
43-
anchor.textContent = hunkAnchor.textContent;
45+
anchor.textContent = 'compare with the base';
4446
anchor.setAttribute('target', '_blank');
45-
paragraph.appendChild(anchor);
46-
paragraph.innerHTML += '&nbsp;';
47+
hunk.innerHTML += '&nbsp;&nbsp;';
48+
hunk.appendChild(anchor);
4749
});
4850
});
4951
});
5052
</script>
5153
EOF
5254
echo '</head>' >> CHANGES.html
5355
echo '<body>' >> CHANGES.html
54-
(cd $DOC_REPOSITORY && git diff $BASE_DOC_COMMIT -- "*.html") > diff.txt
5556
python3 - << EOF
5657
import os, re, html
57-
with open('diff.txt', 'r') as f:
58+
from itertools import chain
59+
with open('$DIFF_TEXT', 'r') as f:
5860
diff_text = f.read()
5961
diff_blocks = re.split(r'^(?=diff --git)', diff_text, flags=re.MULTILINE)
6062
out_blocks = []
6163
for block in diff_blocks:
6264
match = re.search(r'^diff --git a/(.*) b/\1', block, flags=re.MULTILINE)
6365
if match:
64-
doc = match.group(1)
65-
file_path = os.path.join('$DOC_REPOSITORY', doc)
66+
path = match.group(1)
67+
file_path = os.path.join('$DOC_REPOSITORY', path)
6668
try:
6769
with open(file_path, 'r') as file:
6870
content = file.readlines()
6971
except FileNotFoundError:
7072
content = []
7173
count = 0
74+
hunks = []
75+
hunk_lines = []
76+
in_hunk = False
7277
for line in block.splitlines():
7378
if line.startswith('@@ -'):
79+
if hunk_lines:
80+
hunks.append('<pre><code class="language-diff">'
81+
+ html.escape('\n'.join(hunk_lines)).strip()
82+
+ '</code></pre>')
83+
hunk_lines = []
7484
search_result = re.search(r'@@ -(\d+),(\d+) \+(\d+),(\d+)', line)
7585
if search_result:
76-
line_number = int(search_result.group(3))
77-
for i in range(line_number - 1, -1, -1):
78-
if content[i].startswith('<'):
86+
line_number = int(search_result.group(3)) - 1
87+
span = int(search_result.group(4))
88+
for i in chain(range(line_number, line_number + span), range(line_number - 1, -1, -1)):
89+
try:
90+
ln = content[i]
91+
except IndexError:
92+
continue
93+
for idx, char in enumerate(ln):
94+
if not char.isspace():
95+
break
96+
else:
97+
idx = len(ln)
98+
if ln.startswith('<', idx) and not ln.startswith('</', idx):
7999
count += 1
80-
content[i] = f'<span id="hunk{count}" style="visibility: hidden;"></span>' + content[i]
100+
content[i] = ln[:idx] + f'<span id="hunk{count}" style="visibility: hidden;"></span>' + ln[idx:]
101+
hunks.append(f'<p class="hunk"><a href="{path}#hunk{count}" class="hunk" target="_blank">hunk #{count}</a></p>')
81102
break
103+
hunk_lines.append(line)
104+
if hunk_lines:
105+
hunks.append('<pre><code class="language-diff">'
106+
+ html.escape('\n'.join(hunk_lines)).strip()
107+
+ '</code></pre>')
82108
if content:
83109
with open(file_path, 'w') as file:
84110
file.writelines(content)
85-
path = doc
86-
hunks = '&nbsp;'.join(f'<a href="{path}#hunk{i+1}" class="hunk" target="_blank">#{i + 1}</a>' for i in range(count))
87-
out_blocks.append(f'<p class="diff"><a href="{path}">{doc}</a>&nbsp;' + hunks + '&emsp;</p>'
88-
+ '\n<pre><code class="language-diff">'
89-
+ html.escape(block).strip() + '</code></pre>')
111+
out_blocks.append(f'<div class="diff"><p class="diff"><a href="{path}">{path}</a></p>\n' + '\n'.join(hunks) + '\n</div>')
90112
output_text = '\n'.join(out_blocks)
91113
with open('diff.html', 'w') as f:
92114
f.write(output_text)
93115
EOF
94116
cat diff.html >> CHANGES.html
95117
echo '</body>' >> CHANGES.html
96118
echo '</html>' >> CHANGES.html
97-
rm diff.txt diff.html
119+
rm diff.html

‎.ci/retrofit-worktree.sh

+3-2
Original file line numberDiff line numberDiff line change
@@ -23,9 +23,10 @@ set -x
2323
# If actions/checkout downloaded our source tree using the GitHub REST API
2424
# instead of with git (because do not have git installed in our image),
2525
# we first make the source tree a repo.
26-
if [ ! -d .git ]; then git init && git add -A && git commit --quiet -m "new"; fi
26+
if [ ! -d .git ]; then git init; fi
2727

28-
# Tag this state of the source tree "new". This is what we want to build and test.
28+
# Commit and tag this state of the source tree "new". This is what we want to build and test.
29+
git add -A && git commit --quiet --allow-empty -m "new"
2930
git tag -f new
3031

3132
# Our container image contains a source tree in $WORKTREE_DIRECTORY with a full build of Sage.

0 commit comments

Comments
 (0)
Please sign in to comment.