Skip to content

Commit

Permalink
Merge branch 'develop' into independence_posets
Browse files Browse the repository at this point in the history
  • Loading branch information
@fchapoton
fchapoton authored Feb 21, 2025
2 parents 8bf6574 + 766c7a0 commit 28eda71
Show file tree
Hide file tree
Showing 3,762 changed files with 131,231 additions and 128,139 deletions.
The diff you're trying to view is too large. We only load the first 3000 changed files.
78 changes: 53 additions & 25 deletions .ci/create-changes-html.sh
View file
Original file line number Diff line number Diff line change
@@ -1,11 +1,12 @@
#!/bin/sh
if [ $# != 2 ]; then
echo >&2 "usage: $0 BASE_DOC_COMMIT DOC_REPO"
echo >&2 "creates CHANGES.html in the current directory"
echo >&2 "for the diffs of DOC_REPO against BASE_DOC_COMMIT"
echo >&2 "Usage: $0 DIFF_TEXT DOC_REPO"
echo >&2 "This script generates a CHANGES.html file in the current directory"
echo >&2 "and adds anchor targets in the documents within DOC_REPO"
echo >&2 "based on the diff hunks in the DIFF_TEXT file."
exit 1
fi
BASE_DOC_COMMIT="$1"
DIFF_TEXT="$1"
DOC_REPOSITORY="$2"

# Create CHANGES.html
Expand All @@ -15,6 +16,12 @@ echo '<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/highli
echo '<script src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.9.0/highlight.min.js"></script>' >> CHANGES.html
echo '<script>hljs.highlightAll();</script>' >> CHANGES.html
cat >> CHANGES.html << EOF
<style>
p.diff a:first-child {
font-weight: bold;
font-size: x-large;
}
</style>
<script>
document.addEventListener('DOMContentLoaded', () => {
// This URL is hardcoded in the file .github/workflows/doc-publish.yml.
Expand All @@ -24,74 +31,95 @@ const diffSite = 'https://pianomister.github.io/diffsite'
const diffParagraphs = document.querySelectorAll('p.diff');
diffParagraphs.forEach(paragraph => {
const rootURL = window.location.origin;
const docAnchor = paragraph.querySelector('a'); // first "a" element
const docAnchor = paragraph.querySelector('a');
const url = new URL(docAnchor.href);
const path = url.pathname;
const anchor = document.createElement('a');
anchor.href = diffSite + '/?url1=' + rootURL + path + '&url2=' + baseDocURL + path;
anchor.textContent = 'compare with the base';
anchor.setAttribute('target', '_blank');
paragraph.innerHTML += '&nbsp;&nbsp;';
paragraph.appendChild(anchor);
paragraph.innerHTML += '&nbsp;';
const hunkAnchors = paragraph.querySelectorAll('a.hunk');
hunkAnchors.forEach(hunkAnchor => {
const hunks = paragraph.parentNode.querySelectorAll('p.hunk');
hunks.forEach(hunk => {
const hunkAnchor = hunk.querySelector('a');
const url = new URL(hunkAnchor.href);
const path = url.pathname;
const pathHash = path + url.hash.replace('#', '%23');
const anchor = document.createElement('a');
anchor.href = diffSite + '/?url1=' + rootURL + pathHash + '&url2=' + baseDocURL + path;
anchor.textContent = hunkAnchor.textContent;
anchor.textContent = 'compare with the base';
anchor.setAttribute('target', '_blank');
paragraph.appendChild(anchor);
paragraph.innerHTML += '&nbsp;';
hunk.innerHTML += '&nbsp;&nbsp;';
hunk.appendChild(anchor);
});
});
});
</script>
EOF
echo '</head>' >> CHANGES.html
echo '<body>' >> CHANGES.html
(cd $DOC_REPOSITORY && git diff $BASE_DOC_COMMIT -- "*.html") > diff.txt
python3 - << EOF
import os, re, html
with open('diff.txt', 'r') as f:
from itertools import chain
with open('$DIFF_TEXT', 'r') as f:
diff_text = f.read()
diff_blocks = re.split(r'^(?=diff --git)', diff_text, flags=re.MULTILINE)
out_blocks = []
for block in diff_blocks:
match = re.search(r'^diff --git a/(.*) b/\1', block, flags=re.MULTILINE)
if match:
doc = match.group(1)
file_path = os.path.join('$DOC_REPOSITORY', doc)
path = match.group(1)
file_path = os.path.join('$DOC_REPOSITORY', path)
try:
with open(file_path, 'r') as file:
content = file.readlines()
except FileNotFoundError:
content = []
count = 0
hunks = []
hunk_lines = []
in_hunk = False
for line in block.splitlines():
if line.startswith('@@ -'):
if hunk_lines:
hunks.append('<pre><code class="language-diff">'
+ html.escape('\n'.join(hunk_lines)).strip()
+ '</code></pre>')
hunk_lines = []
search_result = re.search(r'@@ -(\d+),(\d+) \+(\d+),(\d+)', line)
if search_result:
line_number = int(search_result.group(3))
for i in range(line_number - 1, -1, -1):
if content[i].startswith('<'):
line_number = int(search_result.group(3)) - 1
span = int(search_result.group(4))
for i in chain(range(line_number, line_number + span), range(line_number - 1, -1, -1)):
try:
ln = content[i]
except IndexError:
continue
for idx, char in enumerate(ln):
if not char.isspace():
break
else:
idx = len(ln)
if ln.startswith('<', idx) and not ln.startswith('</', idx):
count += 1
content[i] = f'<span id="hunk{count}" style="visibility: hidden;"></span>' + content[i]
content[i] = ln[:idx] + f'<span id="hunk{count}" style="visibility: hidden;"></span>' + ln[idx:]
hunks.append(f'<p class="hunk"><a href="{path}#hunk{count}" class="hunk" target="_blank">hunk #{count}</a></p>')
break
hunk_lines.append(line)
if hunk_lines:
hunks.append('<pre><code class="language-diff">'
+ html.escape('\n'.join(hunk_lines)).strip()
+ '</code></pre>')
if content:
with open(file_path, 'w') as file:
file.writelines(content)
path = doc
hunks = '&nbsp;'.join(f'<a href="{path}#hunk{i+1}" class="hunk" target="_blank">#{i + 1}</a>' for i in range(count))
out_blocks.append(f'<p class="diff"><a href="{path}">{doc}</a>&nbsp;' + hunks + '&emsp;</p>'
+ '\n<pre><code class="language-diff">'
+ html.escape(block).strip() + '</code></pre>')
out_blocks.append(f'<div class="diff"><p class="diff"><a href="{path}">{path}</a></p>\n' + '\n'.join(hunks) + '\n</div>')
output_text = '\n'.join(out_blocks)
with open('diff.html', 'w') as f:
f.write(output_text)
EOF
cat diff.html >> CHANGES.html
echo '</body>' >> CHANGES.html
echo '</html>' >> CHANGES.html
rm diff.txt diff.html
rm diff.html
2 changes: 1 addition & 1 deletion .ci/retrofit-worktree.sh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,4 +43,4 @@ git worktree add --detach $WORKTREE_NAME
rm -rf $WORKTREE_DIRECTORY/.git && mv $WORKTREE_NAME/.git $WORKTREE_DIRECTORY/
rm -rf $WORKTREE_NAME && ln -s $WORKTREE_DIRECTORY $WORKTREE_NAME
if [ ! -f $WORKTREE_NAME/.gitignore ]; then cp .gitignore $WORKTREE_NAME/; fi
(cd $WORKTREE_NAME && git add -A && git commit --quiet --allow-empty -m "old" -a && git tag -f old && git checkout new && git status)
(cd $WORKTREE_NAME && git add -A && git commit --quiet --allow-empty -m "old" -a && git tag -f old && git checkout -f new && git clean -fd && git status)
71 changes: 0 additions & 71 deletions .ci/set_labels_by_changes.sh
View file

This file was deleted.

Loading

0 comments on commit 28eda71

Please sign in to comment.