CODEX revised with following function: 1. GDS building, 2. different user group with different authority.

This commit is contained in:
2026-05-28 20:35:49 +08:00
parent e6e9e13cf2
commit 1215bf978a
25 changed files with 439 additions and 196 deletions
+10 -1
View File
@@ -3948,7 +3948,16 @@ ${bundlesBlock}`;
const warningText = result.warnings && result.warnings.length > 0
? ` (${result.warnings.length} warnings)`
: '';
addLog(`GDS built with ${result.engine}: ${result.path}${warningText}`);
if (result.download_url) {
const link = document.createElement('a');
link.href = result.download_url;
link.download = result.filename || `${currentProjectName}.gds`;
link.style.display = 'none';
document.body.appendChild(link);
link.click();
link.remove();
}
addLog(`GDS built with ${result.engine}: ${result.filename || result.path}${warningText}`);
} catch (err) {
addLog(`Build GDS network error: ${err.message}. Check that the Flask server is running from the same host and Python environment.`);
} finally {
+6
View File
@@ -608,6 +608,10 @@
<label>Credits</label>
<div class="profile-value" id="profile-credits">0</div>
</div>
<div class="profile-item">
<label>User Group</label>
<div class="profile-value" id="profile-group">-</div>
</div>
<div class="profile-item">
<label>Occupation</label>
<select id="profile-occupation"></select>
@@ -694,6 +698,7 @@
const profileUsername = document.getElementById('profile-username');
const profileCreated = document.getElementById('profile-created');
const profileCredits = document.getElementById('profile-credits');
const profileGroup = document.getElementById('profile-group');
const profileOccupation = document.getElementById('profile-occupation');
const themeToggle = document.getElementById('theme-toggle');
const logTerminal = document.getElementById('log-terminal');
@@ -733,6 +738,7 @@
profileUsername.textContent = profile.username;
profileCreated.textContent = profile.created_at || '-';
profileCredits.textContent = profile.credits ?? 0;
profileGroup.textContent = profile.user_group || 'user';
profileOccupation.innerHTML = '';
(profile.occupations || []).forEach(occupation => {
const option = document.createElement('option');