Merge branch 'develop' into cocoalib-2024

sagemath · Oct 31, 2024 · d733689 · d733689
2 parents a0a4ce6 + 1b3f398
commit d733689
Show file tree

Hide file tree

Showing 3,109 changed files with 92,638 additions and 86,018 deletions.
diff --git a/.ci/create-changes-html.sh b/.ci/create-changes-html.sh
@@ -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
@@ -24,74 +25,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
diff --git a/.ci/retrofit-worktree.sh b/.ci/retrofit-worktree.sh
@@ -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)
diff --git a/.ci/set_labels_by_changes.sh b/.ci/set_labels_by_changes.sh