diff --git a/qt/CMakeLists.txt b/qt/CMakeLists.txt index 54b54fe..b7dfd15 100644 --- a/qt/CMakeLists.txt +++ b/qt/CMakeLists.txt @@ -8,7 +8,7 @@ set(CMAKE_CXX_STANDARD 17) set(CMAKE_CXX_STANDARD_REQUIRED ON) add_compile_definitions(WITH_CMAKE) -find_package(Qt6 REQUIRED COMPONENTS Quick Widgets QuickControls2 LinguistTools) +find_package(Qt6 REQUIRED COMPONENTS Quick Widgets QuickControls2 LinguistTools PrintSupport) find_package(LibXml2 REQUIRED) find_package(Intl REQUIRED) set(Qt6_FIND_VERSION_MIN 6.0) @@ -110,6 +110,7 @@ target_link_libraries(aris-qt PRIVATE Qt6::Quick PRIVATE Qt6::Widgets PRIVATE Qt6::QuickControls2 + PRIVATE Qt6::PrintSupport PUBLIC LibXml2::LibXml2 PRIVATE Intl::Intl ) diff --git a/qt/DrawerTools.qml b/qt/DrawerTools.qml index 35cd864..e94c931 100644 --- a/qt/DrawerTools.qml +++ b/qt/DrawerTools.qml @@ -86,7 +86,7 @@ ToolBar { fileModified = false } else - saveAsID.open() + saveFormatPickerID.open() menuOptions.close() } @@ -98,14 +98,8 @@ ToolBar { icon.color: darkMode ? "white" : "black" onClicked: { - - if (Qt.platform.os === "wasm") - cConnector.wasmSaveProof(theData, theGoals) - else - saveAsID.open() - fileModified = false - menuOptions.close() + saveFormatPickerID.open() } } diff --git a/qt/ProofArea.qml b/qt/ProofArea.qml index e47d28b..a53d81b 100644 --- a/qt/ProofArea.qml +++ b/qt/ProofArea.qml @@ -275,6 +275,29 @@ Item { } } + // Ctrl+Shift+M / Meta+Shift+M — add a comment line. + Shortcut { + sequences: ["Ctrl+Shift+M", "Meta+Shift+M"] + context: Qt.ApplicationShortcut + onActivated: { + var cur = listView.currentIndex + if (cur < 0) { + cConnector.evalText = "⚠ " + qsTr("No line selected.") + return + } + var insertIndex = cur + 1 + var curInd = proofModel.data(proofModel.index(cur, 0), 262) + theData.insertLine(insertIndex, insertIndex + 1, "", "comment", + false, false, false, curInd, [-1]) + proofModel.updateLines() + proofModel.updateRefs(insertIndex, true) + listView.currentIndex = insertIndex + fileModified = true + cConnector.evalText = "Evaluate Proof" + proofModel.clearErrors() + } + } + // Ctrl+Delete / Cmd+Delete / Cmd+Backspace — remove the currently focused line. // Cmd+Backspace covers compact Mac keyboards that lack a physical Delete key. // If it is the very last line, resets to a blank premise so the UI never @@ -489,6 +512,24 @@ Item { } } + // Add Comment below + Action { + text: qsTr("Add Comment Below") + onTriggered: { + var myIdx = rootProofArea.contextMenuTargetIdx + if (myIdx < 0) return + var curInd = proofModel.data(proofModel.index(myIdx, 0), 262) + theData.insertLine(myIdx + 1, myIdx + 2, "", "comment", + false, false, false, curInd, [-1]) + proofModel.updateLines() + proofModel.updateRefs(myIdx + 1, true) + listView.currentIndex = myIdx + 1 + fileModified = true + cConnector.evalText = "Evaluate Proof" + proofModel.clearErrors() + } + } + MenuSeparator {} // Remove line @@ -640,6 +681,12 @@ Item { delegate: proofLineID highlight: highlightID + // Disable auto-scroll-to-current so the user can freely scroll + // the proof after zooming. Without this, forceLayout() (called on + // zoom) causes the ListView to re-pin the view onto the focused line, + // making it impossible to scroll away from it. + highlightFollowsCurrentItem: false + currentIndex: -1 Layout.fillWidth: true @@ -647,11 +694,45 @@ Item { spacing: scaledSpacing ScrollBar.vertical: ScrollBar {} + // ── Smooth scroll settings ──────────────────────────────────── + // Pre-render one viewport-height of delegates above and below the + // visible area so fast scrolling never stalls on delegate creation. + cacheBuffer: height + + // Lower deceleration → longer, floatier flick glide (touch/drag). + // Higher max velocity → fast swipes feel uncapped. + flickDeceleration: 600 // default 1500 + maximumFlickVelocity: 4000 // default 2500 + + // Snap content to integer pixel boundaries — eliminates sub-pixel + // shimmer during scroll. + pixelAligned: true + onCurrentItemChanged: { if (currentItem && currentItem.focusTextField) currentItem.focusTextField() + // Scroll only enough to make the newly-selected line visible. + // ListView.Contain = no-op if already in view; minimal scroll otherwise. + if (currentIndex >= 0) + positionViewAtIndex(currentIndex, ListView.Contain) + } + + // When zoom changes, delegate heights and spacings change via bindings, + // but the ListView's internal position cache goes stale. A deferred + // forceLayout() recomputes every item's pixel offset so contentHeight + // and the ScrollBar stay correct. + Connections { + target: rootID + function onZoomFactorChanged() { + Qt.callLater(function() { listView.forceLayout() }) + } } } + + + + + } Component { @@ -675,7 +756,7 @@ Item { property string type: model.type property int indexx: model.index property bool vis: type === "premise" || type === "subproof" - || type === "sf" + || type === "sf" || type === "comment" // These delegate-level ints mirror the ProofModel roles. // They must live here (not inside a ComboBox) because inside a ComboBox, // `model` refers to the combo's own string-array model, NOT the row data. @@ -779,6 +860,7 @@ Item { // Line Number Button Button { id: lineNumberID + visible: type !== "comment" Layout.preferredHeight: theTextID.height // Content-aware width: at least as tall as it is wide (square), @@ -852,9 +934,10 @@ Item { TextField { id: theTextID - color: darkMode ? "white" : "black" + color: type === "comment" ? (darkMode ? "#808080" : "#888888") : (darkMode ? "white" : "black") height: scaledFontSize + scaledSpacing font.pointSize: scaledFontSize + font.italic: type === "comment" Layout.fillWidth: true Keys.onPressed: (event) => { @@ -895,13 +978,15 @@ Item { id: backRectID border.width: 1 border.color: { + if (type === "comment") + return darkMode ? "#2A2A1E" : "#FFFDE7" if (cConnector.evalText === "Evaluate Proof") return darkMode ? "white" : "black" if (model.errMsg !== "") return "red" return "springgreen" } - color: textFieldColor + color: type === "comment" ? (darkMode ? "#2A2A1E" : "#FFFDE7") : textFieldColor } //placeholderText: indexx === 0 ? qsTr("Start Typing here..."): "" @@ -1063,6 +1148,7 @@ Item { font.pointSize: scaledFontSize // Short form when zoomed in (>150%) so label stays compact text: { + if (model.type === "comment") return "//" if (zoomFactor > 1.5) { if (model.type === "premise") return "P" if (model.type === "subproof") return "SP" @@ -1329,6 +1415,20 @@ Item { } } + Action { + text: qsTr("Add Comment") + onTriggered: { + theData.insertLine(index + 1, index + 2, "", + "comment", false, false, + false, model.ind, [-1]) + proofModel.updateLines() + proofModel.updateRefs(index + 1, true) + listView.currentIndex = index + 1 + cConnector.evalText = "Evaluate Proof" + proofModel.clearErrors() + } + } + Action { text: type === "premise" ? qsTr("Convert to Conclusion") : qsTr("Convert to Premise") diff --git a/qt/aris-qt.pro b/qt/aris-qt.pro index 3317887..2196e4d 100644 --- a/qt/aris-qt.pro +++ b/qt/aris-qt.pro @@ -1,4 +1,5 @@ QT += quick widgets quickcontrols2 +!wasm: QT += printsupport CONFIG += lrelease embed_translations diff --git a/qt/auxconnector.cpp b/qt/auxconnector.cpp index 5536502..d2d841f 100644 --- a/qt/auxconnector.cpp +++ b/qt/auxconnector.cpp @@ -26,6 +26,13 @@ #include #include #include +#include +#include +#include +#include +#ifndef Q_OS_WASM +#include +#endif #ifndef Q_OS_WASM #include @@ -436,12 +443,18 @@ static QString proofLineToText(const ProofLine &pl, int depth, const QString &pr QString rule; if (pl.pSubStart) rule = "(subproof start)"; + else if (pl.pType == QLatin1String("comment")) + rule = ""; else if (!pl.pType.isEmpty() && pl.pType != "choose") rule = pl.pType + (refs.isEmpty() ? "" : ": " + refs); // Compose: " ┌─ 3. P → Q [→ Elim: 1, 2]" QString formula = pl.pText.isEmpty() ? "(empty)" : pl.pText; - QString left = indent + lineNum + ". " + formula; + if (pl.pType == QLatin1String("comment")) formula = "// " + pl.pText; + + QString left = (pl.pType == QLatin1String("comment")) ? + (indent + " " + formula) : + (indent + lineNum + ". " + formula); QString ruleTag = rule.isEmpty() ? "" : " [" + rule + "]"; // Pad the formula area to a fixed column so rule tags align. @@ -566,6 +579,12 @@ void auxConnector::exportMarkdown(const QString &name, const ProofData *pd) out << "| | " << nbsp << "*subproof end* | | |\n"; continue; } + if (pl.pType == QLatin1String("comment")) { + QString commentText = pl.pText; + commentText.replace("|", "\\|"); + out << "| | " << nbsp << "*// " << commentText << "* | | |\n"; + continue; + } // Regular line. QString lineNum = QString::number(pl.pLine); @@ -610,3 +629,231 @@ void auxConnector::wasmExportMarkdown(const ProofData *pd) } QFile::remove("aris_export_tmp.md"); } + +// --------------------------------------------------------------------------- +// Shared helper: build a QTextDocument representation of the proof. +// Used by both exportDocx and exportPdf so formatting is identical. +// --------------------------------------------------------------------------- +static QTextDocument *buildProofDocument(const ProofData *pd) +{ + QTextDocument *doc = new QTextDocument(); + QTextCursor cur(doc); + + // ---- Title ---- + QTextCharFormat titleFmt; + titleFmt.setFontWeight(QFont::Bold); + titleFmt.setFontPointSize(16); + cur.insertText(QStringLiteral("Proof"), titleFmt); + + QTextCharFormat normalFmt; + normalFmt.setFontPointSize(11); + cur.insertBlock(); + cur.insertText(QString(), normalFmt); + + const QVector &lines = pd->lines(); + const int n = lines.size(); + + // ---- Table ---- + // Columns: # | Formula | Rule | Refs + QTextTableFormat tableFmt; + tableFmt.setHeaderRowCount(1); + tableFmt.setCellPadding(4); + tableFmt.setCellSpacing(0); + tableFmt.setBorderStyle(QTextFrameFormat::BorderStyle_Solid); + tableFmt.setBorder(1); + tableFmt.setWidth(QTextLength(QTextLength::PercentageLength, 100)); + + // Column widths: 5% | 55% | 25% | 15% + QVector colWidths; + colWidths << QTextLength(QTextLength::PercentageLength, 5) + << QTextLength(QTextLength::PercentageLength, 55) + << QTextLength(QTextLength::PercentageLength, 25) + << QTextLength(QTextLength::PercentageLength, 15); + tableFmt.setColumnWidthConstraints(colWidths); + + QTextTable *table = cur.insertTable(n + 1, 4, tableFmt); + + // Header row + QTextCharFormat hdrFmt; + hdrFmt.setFontWeight(QFont::Bold); + const QStringList headers = { QStringLiteral("#"), + QStringLiteral("Formula"), + QStringLiteral("Rule"), + QStringLiteral("Refs") }; + for (int c = 0; c < 4; ++c) { + QTextCursor cell = table->cellAt(0, c).firstCursorPosition(); + cell.insertText(headers.at(c), hdrFmt); + } + + // Data rows + for (int i = 0; i < n; ++i) { + const ProofLine &pl = lines.at(i); + int depth = pl.pInd / 20; + + // Indentation prefix (em-space per depth level) + QString indent = QString(QChar(0x2003)).repeated(depth); // EM SPACE + + // Formula cell + QString formula; + if (pl.pSubStart) + formula = indent + QStringLiteral("\u250c\u2500 subproof"); // ┌─ + else if (pl.pSubEnd) + formula = indent + QStringLiteral("\u2514\u2500"); // └─ + else if (pl.pType == QLatin1String("comment")) + formula = indent + QStringLiteral("// ") + pl.pText; + else + formula = indent + (pl.pText.isEmpty() ? QStringLiteral("(empty)") : pl.pText); + + // Rule + QString rule; + if (!pl.pSubStart && !pl.pSubEnd && pl.pType != QLatin1String("comment")) { + rule = (pl.pType == QLatin1String("premise")) ? QStringLiteral("premise") : pl.pType; + if (rule == QLatin1String("choose")) rule = QString(); + } + + // Refs + QStringList refStrs; + for (int r : pl.pRefs) + if (r != -1) refStrs << QString::number(r); + QString refs = refStrs.join(QStringLiteral(", ")); + + auto insertCell = [&](int col, const QString &txt, bool italic = false) { + QTextCursor c = table->cellAt(i + 1, col).firstCursorPosition(); + QTextCharFormat f = normalFmt; + if (italic) f.setFontItalic(true); + if (pl.pType == QLatin1String("comment")) f.setForeground(QColor(128, 128, 128)); + c.insertText(txt, f); + }; + + insertCell(0, pl.pSubStart || pl.pSubEnd || pl.pType == QLatin1String("comment") ? QString() : QString::number(pl.pLine)); + insertCell(1, formula, pl.pType == QLatin1String("comment")); + insertCell(2, rule); + insertCell(3, refs); + } + + // Footer note + cur = doc->rootFrame()->lastCursorPosition(); + cur.insertBlock(); + QTextCharFormat footerFmt; + footerFmt.setFontItalic(true); + footerFmt.setFontPointSize(9); + cur.insertText(QStringLiteral("Generated by GNU Aris"), footerFmt); + + return doc; +} + +// --------------------------------------------------------------------------- +// ODT export +// --------------------------------------------------------------------------- + +/* Exports the proof to an OpenDocument Text (.odt) file. + * Uses QTextDocumentWriter with the "odf" format, which is built into Qt + * on all platforms — no extra plugin is required. + * input: + * name - absolute file path (may have "file://" prefix). + * pd - pointer to the ProofData object. + */ +void auxConnector::exportOdt(const QString &name, const ProofData *pd) +{ + QString path = name.startsWith(QLatin1String("file://")) ? name.mid(7) : name; + + // Ensure the path ends with .odt. + if (!path.endsWith(QLatin1String(".odt"), Qt::CaseInsensitive)) + path += QStringLiteral(".odt"); + + QScopedPointer doc(buildProofDocument(pd)); + + QTextDocumentWriter writer(path); + writer.setFormat("odf"); // built-in Qt format, always available + + if (!writer.write(doc.data())) { + emit errorOccurred(tr("ODT export failed: could not write to '%1'.").arg(path)); + qDebug() << "[ARIS] exportOdt: write failed for" << path; + return; + } + + qDebug() << "[ARIS] exportOdt: wrote" << path; +} + +/* Exports the proof to an ODT file (WebAssembly). + * Writes to a temp file then triggers a browser download. + */ +void auxConnector::wasmExportOdt(const ProofData *pd) +{ + const QString tmp = QStringLiteral("aris_export_tmp.odt"); + exportOdt(tmp, pd); + QFile file(tmp); + if (file.open(QIODevice::ReadOnly)) { + QFileDialog::saveFileContent(file.readAll(), QStringLiteral("proof.odt")); + file.close(); + } + QFile::remove(tmp); +} + + +// --------------------------------------------------------------------------- +// PDF export +// --------------------------------------------------------------------------- + +/* Exports the proof to a PDF file. + * Uses QPrinter in PdfFormat mode together with QTextDocument::print(). + * Not available in WASM builds (QPrinter / PrintSupport is absent from + * the Qt WASM SDK); on WASM a clear error is emitted instead. + * input: + * name - absolute file path (may have "file://" prefix). + * pd - pointer to the ProofData object. + */ +void auxConnector::exportPdf(const QString &name, const ProofData *pd) +{ +#ifdef Q_OS_WASM + Q_UNUSED(name) + Q_UNUSED(pd) + emit errorOccurred(tr("PDF export is not available on your device.")); +#else + QString path = name.startsWith(QLatin1String("file://")) ? name.mid(7) : name; + + if (!path.endsWith(QLatin1String(".pdf"), Qt::CaseInsensitive)) + path += QStringLiteral(".pdf"); + + QPrinter printer(QPrinter::PrinterResolution); + printer.setOutputFormat(QPrinter::PdfFormat); + printer.setOutputFileName(path); + printer.setPageSize(QPageSize(QPageSize::A4)); + printer.setPageOrientation(QPageLayout::Portrait); + + QScopedPointer doc(buildProofDocument(pd)); + doc->print(&printer); + + // QPrinter::PdfFormat always succeeds unless the path is unwritable. + // Verify the file was actually created. + if (!QFile::exists(path)) { + emit errorOccurred(tr("PDF export failed: could not write to '%1'.").arg(path)); + qDebug() << "[ARIS] exportPdf: file not found after print for" << path; + return; + } + + qDebug() << "[ARIS] exportPdf: wrote" << path; +#endif +} + +/* Exports the proof to a PDF file (WebAssembly). + * QPrinter is unavailable in WASM; emit a user-facing error. + * On desktop this path is never reached (wasmExportPdf is only + * called from the WASM branch of the QML format picker). + */ +void auxConnector::wasmExportPdf(const ProofData *pd) +{ +#ifdef Q_OS_WASM + Q_UNUSED(pd) + emit errorOccurred(tr("PDF export is not available in the browser version.")); +#else + const QString tmp = QStringLiteral("aris_export_tmp.pdf"); + exportPdf(tmp, pd); + QFile file(tmp); + if (file.open(QIODevice::ReadOnly)) { + QFileDialog::saveFileContent(file.readAll(), QStringLiteral("proof.pdf")); + file.close(); + } + QFile::remove(tmp); +#endif +} diff --git a/qt/auxconnector.h b/qt/auxconnector.h index 3100825..793829e 100644 --- a/qt/auxconnector.h +++ b/qt/auxconnector.h @@ -39,6 +39,14 @@ class auxConnector : public QObject Q_INVOKABLE void exportMarkdown(const QString &name, const ProofData *pd); Q_INVOKABLE void wasmExportMarkdown(const ProofData *pd); + // ODT export (desktop + WASM) + Q_INVOKABLE void exportOdt(const QString &name, const ProofData *pd); + Q_INVOKABLE void wasmExportOdt(const ProofData *pd); + + // PDF export (desktop + WASM) + Q_INVOKABLE void exportPdf(const QString &name, const ProofData *pd); + Q_INVOKABLE void wasmExportPdf(const ProofData *pd); + Q_INVOKABLE void importProof(const QString &name, ProofData *pd, const Connector *c, ProofModel *pm); Q_INVOKABLE void wasmImportProof(ProofData *pd, const Connector *c, ProofModel *pm); Q_INVOKABLE void importProofWithMode(const QString &name, ProofData *pd, const Connector *c, ProofModel *pm, int mode); diff --git a/qt/connector.cpp b/qt/connector.cpp index 0b8862a..4e527dc 100644 --- a/qt/connector.cpp +++ b/qt/connector.cpp @@ -36,6 +36,7 @@ #include #include #include +#include #ifdef Q_OS_WASM #include @@ -259,6 +260,9 @@ void Connector::genProof(const ProofData *toBeEval) for (int i = 0; i < snap.size(); i++) { const ProofLine &pl = snap.at(i); // const-ref into the snapshot — zero copies + if (pl.pType == QLatin1String("comment")) + continue; // Skip comments entirely so the C-engine doesn't see them + int *ind = (int *) calloc(m_indices[i].size(), sizeof(int)); short *temp_refs = (short *) calloc(pl.pRefs.size(), sizeof(short)); @@ -295,12 +299,24 @@ void Connector::genProof(const ProofData *toBeEval) conn = 0; } - // Assign references + // Map UI labels to logical line indices (1-based) for the C-engine evaluator + // because the engine treats refs as raw indices into its linked list! + QHash uiToLogical; + int logicalCounter = 1; + for (int i = 0; i < snap.size(); i++) { + if (snap.at(i).pType != QLatin1String("comment")) { + uiToLogical.insert(snap.at(i).pLine, logicalCounter++); + } + } + + // Assign references mapped to logical indices if (pl.pRefs.size() == 1) { temp_refs[0] = REF_END; } else { - for (int ii = 1; ii < pl.pRefs.size(); ii++) - temp_refs[ii - 1] = pl.pRefs.at(ii); + for (int ii = 1; ii < pl.pRefs.size(); ii++) { + int uiRef = pl.pRefs.at(ii); + temp_refs[ii - 1] = uiToLogical.value(uiRef, uiRef); // fallback to raw if not found + } temp_refs[pl.pRefs.size() - 1] = REF_END; } @@ -386,20 +402,24 @@ int Connector::evalProof(const ProofData *toBeEval, const GoalData *gls, ProofMo anyError = true; // Build "Line N · RuleName: " for inline display. - int lineNum = i + 1; - QString ruleName = reverseRulesMap.value(sd->rule, QStringLiteral("?")); + int lineNum = sd->line_num; + int uiRow = lineNum - 1; + // Rule names are translated under the "ProofArea" context, matching the + // qsTr() calls used for the same rule names in the rule dropdown (ProofArea.qml). + QString ruleEnglish = reverseRulesMap.value(sd->rule, QStringLiteral("?")); + QString ruleName = QCoreApplication::translate("ProofArea", ruleEnglish.toUtf8().constData()); QString message = QString::fromUtf8(cur_ret); - QString fullMsg = QStringLiteral("Line %1 · %2: %3") + QString fullMsg = tr("Line %1 · %2: %3") .arg(lineNum) .arg(ruleName) .arg(message); // Write error text directly into the model row (0-based). - pm->setData(pm->index(i, 0), fullMsg, ProofModel::ErrorRole); + pm->setData(pm->index(uiRow, 0), fullMsg, ProofModel::ErrorRole); qDebug() << "[eval] Error line" << lineNum << "(" << ruleName << ") -" << message; } else { - qDebug() << "[eval] Line" << i + 1 << ": Correct!"; + qDebug() << "[eval] Line" << sd->line_num << ": Correct!"; } ev_itr = ev_itr->next; @@ -435,6 +455,25 @@ void Connector::saveProof(const QString &name, const ProofData *toBeSaved, const if (aio_save(cProof,(const char *) file_name) == 0) { qDebug() << "File Saved Successfully"; + // Append comments as a UI-only data block inside the XML + QFile file(localName); + if (file.open(QIODevice::ReadWrite | QIODevice::Text)) { + QString content = file.readAll(); + QString commentsXml; + for (int i = 0; i < toBeSaved->lines().size(); ++i) { + const ProofLine &pl = toBeSaved->lines().at(i); + if (pl.pType == QLatin1String("comment")) { + commentsXml += QString(" \n") + .arg(i).arg(pl.pText.toHtmlEscaped()).arg(pl.pInd); + } + } + if (!commentsXml.isEmpty()) { + content.replace("", "\n" + commentsXml + "\n"); + file.resize(0); + file.write(content.toUtf8()); + } + file.close(); + } } else { m_lastError = tr("File save failed for path: %1").arg(localName); qDebug() << m_lastError; @@ -513,6 +552,25 @@ void Connector::openProof(const QString &name, ProofData *openTo, GoalData *gls) d = sd->depth; } + // Load comments from the UI-only data block + QFile file(localName); + if (file.open(QIODevice::ReadOnly | QIODevice::Text)) { + QString content = QString::fromUtf8(file.readAll()); + file.close(); + + QRegularExpression re(""); + QRegularExpressionMatchIterator matchIt = re.globalMatch(content); + while (matchIt.hasNext()) { + QRegularExpressionMatch match = matchIt.next(); + int idx = match.captured(1).toInt(); + QString t = match.captured(2); + t.replace("<", "<").replace(">", ">").replace("&", "&").replace(""", "\"").replace("'", "'"); + int ind = match.captured(3).toInt(); + QList dummyRefs = {-1}; + openTo->insertLine(idx, idx+1, t.toUtf8().constData(), "comment", false, false, false, ind, dummyRefs, -1, -1); + } + } + int g = gls->glines().size(); for (int i = 0; i < g; i++) gls->removegLineAt(0); diff --git a/qt/main.qml b/qt/main.qml index 8aa54df..2507dde 100644 --- a/qt/main.qml +++ b/qt/main.qml @@ -463,6 +463,44 @@ ApplicationWindow { } } + // Save As — OpenDocument Text (.odt) + FileDialog { + id: saveOdtID + + property bool closeOnSave: false + + nameFilters: ["OpenDocument Text files (*.odt)"] + title: "Save As ODT (.odt)" + fileMode: FileDialog.SaveFile + defaultSuffix: "odt" + onAccepted: { + auxConnector.exportOdt(selectedFile, theData) + if (closeOnSave) { + closeOnSave = false + rootID.close() + } + } + } + + // Save As — PDF (.pdf) + FileDialog { + id: savePdfID + + property bool closeOnSave: false + + nameFilters: ["PDF files (*.pdf)"] + title: "Save As PDF (.pdf)" + fileMode: FileDialog.SaveFile + defaultSuffix: "pdf" + onAccepted: { + auxConnector.exportPdf(selectedFile, theData) + if (closeOnSave) { + closeOnSave = false + rootID.close() + } + } + } + FontDialog { id: fontDialogID @@ -531,17 +569,19 @@ ApplicationWindow { standardButtons: MessageDialog.Save | MessageDialog.Discard | MessageDialog.Cancel onAccepted: { - if (Qt.platform.os === "wasm") - cConnector.wasmSaveProof(theData, theGoals); - else if (fileExists) - cConnector.saveProof(filename, theData, theGoals); - else { - saveAsID.closeOnSave = true - saveAsID.open(); - return + if (fileExists) { + // Re-save the existing .tle file on every platform + if (Qt.platform.os === "wasm") + cConnector.wasmSaveProof(theData, theGoals); + else + cConnector.saveProof(filename, theData, theGoals); + fileModified = false + rootID.close(); + } else { + // New / unsaved proof — let the user choose the format first + saveFormatPickerID.closeOnSave = true + saveFormatPickerID.open(); } - fileModified = false - rootID.close(); } onDiscarded: { fileModified = false; @@ -790,6 +830,122 @@ ApplicationWindow { } } + // Save As format picker — same style as importBehaviorID / exportFormatID. + // Shown whenever the user clicks "Save As" (or saves a new unsaved file). + Dialog { + id: saveFormatPickerID + + // When true the window should close after the save completes + // (forwarded from the unsaved-changes dialog path). + property bool closeOnSave: false + + width: Math.min(rootID.width * 0.42, 460) + anchors.centerIn: parent + + parent: Overlay.overlay + modal: true + closePolicy: Popup.CloseOnEscape + padding: 20 + + Overlay.modal: Rectangle { + color: darkMode ? "#66121212" : "#66CFCFCF" + } + + background: Rectangle { + radius: 12 + color: darkMode ? "#1F1B24" : "white" + border.width: 1 + border.color: darkMode ? "#50485A" : "#D9D9D9" + } + + contentItem: ColumnLayout { + width: saveFormatPickerID.availableWidth + spacing: 20 + + Label { + Layout.fillWidth: true + horizontalAlignment: Text.AlignHCenter + wrapMode: Text.WordWrap + text: qsTr("Choose save format") + color: darkMode ? "white" : "black" + font.bold: true + font.pointSize: thefont.pointSize + 1 + } + + RowLayout { + Layout.fillWidth: true + spacing: 14 + + // ---- Aris (.tle) ---- + Button { + text: qsTr("Aris (.tle)") + Layout.fillWidth: true + palette { + button: darkMode ? "#2A2631" : "white" + buttonText: darkMode ? "white" : "black" + } + onClicked: { + var close = saveFormatPickerID.closeOnSave + saveFormatPickerID.closeOnSave = false + saveFormatPickerID.close() + if (Qt.platform.os === "wasm") { + cConnector.wasmSaveProof(theData, theGoals) + fileModified = false + if (close) rootID.close() + } else { + saveAsID.closeOnSave = close + Qt.callLater(function() { saveAsID.open() }) + } + } + } + + // ---- ODT (.odt) ---- + Button { + text: qsTr("ODT (.odt)") + Layout.fillWidth: true + palette { + button: darkMode ? "#2A2631" : "white" + buttonText: darkMode ? "white" : "black" + } + onClicked: { + var close = saveFormatPickerID.closeOnSave + saveFormatPickerID.closeOnSave = false + saveFormatPickerID.close() + if (Qt.platform.os === "wasm") { + auxConnector.wasmExportOdt(theData) + if (close) rootID.close() + } else { + saveOdtID.closeOnSave = close + Qt.callLater(function() { saveOdtID.open() }) + } + } + } + + // ---- PDF (.pdf) ---- + Button { + text: qsTr("PDF (.pdf)") + Layout.fillWidth: true + palette { + button: darkMode ? "#2A2631" : "white" + buttonText: darkMode ? "white" : "black" + } + onClicked: { + var close = saveFormatPickerID.closeOnSave + saveFormatPickerID.closeOnSave = false + saveFormatPickerID.close() + if (Qt.platform.os === "wasm") { + auxConnector.wasmExportPdf(theData) + if (close) rootID.close() + } else { + savePdfID.closeOnSave = close + Qt.callLater(function() { savePdfID.open() }) + } + } + } + } + } + } + GoalModel { id: goalDataID glines: theGoals diff --git a/qt/proofmodel.cpp b/qt/proofmodel.cpp index 711e7cc..6c4cd09 100644 --- a/qt/proofmodel.cpp +++ b/qt/proofmodel.cpp @@ -289,30 +289,42 @@ void ProofModel::updateLines() // Update relevant reference roles after insertion and/or removal of a proof line void ProofModel::updateRefs(int ln, bool op) { + qDebug() << "[ProofModel] updateRefs called with ln =" << ln << "op =" << op; for (int i = ln+1; i < mLines->lines().size(); i++){ QList refs = mLines->lines().at(i).pRefs; + bool changed = false; for (int ii = 1; ii < refs.size(); ii++){ - if (op){ - if (refs[ii] >= (ln+1)) + if (refs[ii] >= (ln+1)) { + qDebug() << "[ProofModel] row" << i << "incrementing ref" << refs[ii] << "to" << refs[ii] + 1; refs[ii]++; - + changed = true; + } } else{ - if (refs[ii] == (ln + 1)) + if (refs[ii] == (ln + 1)) { + qDebug() << "[ProofModel] row" << i << "removing ref" << refs[ii]; refs.removeAt(ii); - else if (refs[ii] > (ln + 1)) + changed = true; + ii--; // Adjust index after removal + } + else if (refs[ii] > (ln + 1)) { + qDebug() << "[ProofModel] row" << i << "decrementing ref" << refs[ii] << "to" << refs[ii] - 1; refs[ii]--; - + changed = true; + } } } - QList ret; - for (int x: refs) - ret.append(x); - setData(index(i,0),ret,RefsRole); + + if (changed) { + QList ret; + for (int x: refs) + ret.append(x); + setData(index(i,0),ret,RefsRole); + qDebug() << "[ProofModel] setData called for row" << i << "new refs:" << ret; + } } - } // Clear all inline error messages in the model (called before each evaluation). diff --git a/src/process-main.c b/src/process-main.c index eb8616f..8c1564b 100644 --- a/src/process-main.c +++ b/src/process-main.c @@ -60,5 +60,5 @@ process (unsigned char * conc, vec_t * prems, const char * rule, vec_t * vars, if (strncmp (misc, NOT_MINE, 28)) return misc; - return "Rule not recognized."; + return _("Rule not recognized."); } diff --git a/src/proof.c b/src/proof.c index 005baf8..fb6c8b2 100644 --- a/src/proof.c +++ b/src/proof.c @@ -150,7 +150,14 @@ eval_proof (list_t * everything, vec_t * rets, int verbose) everything); if (!ret_chk) + { + /* Record the failure on this line before bailing out: callers size + their per-line display off of rets, so a line with no entry at + all reads as "not flagged" instead of "could not be checked". */ + if (rets) + vec_str_add_obj (rets, (unsigned char *) _("Internal error: this line could not be evaluated (out of memory).")); return AEC_MEM; + } if (verbose) { diff --git a/src/sexpr-process-bool.c b/src/sexpr-process-bool.c index 4820932..d096e11 100644 --- a/src/sexpr-process-bool.c +++ b/src/sexpr-process-bool.c @@ -98,7 +98,7 @@ proc_bi (unsigned char * prem, unsigned char * conc) { si--; if (si < 0) - return _("Boolean Identity Error: Expected simplification or expansion with True/False constants."); + return _("Boolean Identity Error: The difference must be enclosed by a connective, not at the very start of the sentence."); } else if (si > 0 && (!strncmp (sh_sen + si - 1, S_AND, S_CL) @@ -133,7 +133,7 @@ proc_bi (unsigned char * prem, unsigned char * conc) return NULL; if (li < 0) - return _("Boolean Identity Error: Expected simplification or expansion with True/False constants."); + return _("Boolean Identity Error: Could not align the longer sentence's structure with the point of difference."); if (si < 0) { @@ -144,7 +144,7 @@ proc_bi (unsigned char * prem, unsigned char * conc) } if (ln_sen[li] != '(') - return _("Boolean Identity Error: Expected simplification or expansion with True/False constants."); + return _("Boolean Identity Error: The longer sentence must have a connective at the point of difference."); int tmp_pos; unsigned char * tmp_str; @@ -232,7 +232,7 @@ with a disjunction."); if (ret_str == NO_DIFFERENCE || ret_str == CORRECT) return CORRECT; - return _("Boolean Identity Error: Expected simplification or expansion with True/False constants."); + return _("Boolean Identity Error: Simplifying or expanding the True/False constant does not produce a sentence matching the other line."); } char * diff --git a/src/sexpr-process-quant.c b/src/sexpr-process-quant.c index 83b76b8..47b3e53 100644 --- a/src/sexpr-process-quant.c +++ b/src/sexpr-process-quant.c @@ -413,7 +413,7 @@ proc_nq (unsigned char * prem, unsigned char * conc) if (ln_sen[i] != '(' && strncmp (ln_sen + i - 1, S_UNV, S_CL) && strncmp (ln_sen + i - 1, S_EXL, S_CL) && !islower (ln_sen[i])) { - return _("Null Quantifier constructed incorrectly."); + return _("Null Quantifier Error: The point of difference must be a quantifier with no free occurrences of its variable."); } if (ln_sen[i] == '(') @@ -445,7 +445,7 @@ proc_nq (unsigned char * prem, unsigned char * conc) return NULL; if (!tmp_str) - return _("Null Quantifier constructed incorrectly."); + return _("Null Quantifier Error: Could not find a matching connective enclosing the quantifier."); } else { @@ -508,7 +508,7 @@ proc_nq (unsigned char * prem, unsigned char * conc) if (ret_str == NO_DIFFERENCE || ret_str == CORRECT) return CORRECT; - return _("Null Quantifier constructed incorrectly."); + return _("Null Quantifier Error: Removing the quantifier does not produce a sentence matching the other line."); } char * @@ -544,14 +544,14 @@ proc_pr (unsigned char * prem, unsigned char * conc) int tmp_pos; if (i == 0) - return _("Prenex constructed incorrectly."); + return _("Prenex Error: The quantifier must be preceded by a connective for it to be moved."); tmp_pos = parse_parens (sh_sen, i - 1, &tmp_str); if (tmp_pos == AEC_MEM) return NULL; if (!tmp_str) - return _("Prenex constructed incorrectly."); + return _("Prenex Error: Could not find a matching connective enclosing the quantifier."); unsigned char * scope, * var, quant[S_CL + 1]; int v_len; @@ -560,7 +560,7 @@ proc_pr (unsigned char * prem, unsigned char * conc) if (!scope) return NULL; if (scope[0] == '\0') - return _("Prenex constructed incorrectly."); + return _("Prenex Error: The quantifier's scope must not be empty."); v_len = strlen (var); free (tmp_str); @@ -707,7 +707,7 @@ proc_pr (unsigned char * prem, unsigned char * conc) if (ret_str == NO_DIFFERENCE || ret_str == CORRECT) return CORRECT; - return _("Prenex constructed incorrectly."); + return _("Prenex Error: Moving the quantifier does not produce a sentence matching the other line."); } char * @@ -774,7 +774,7 @@ proc_fv (unsigned char * prem_0, unsigned char * prem_1, unsigned char * conc) if (ret_0 == 0 || ret_1 == 0) return CORRECT; - return _("Free Variable substitution constructed incorrectly."); + return _("Free Variable Substitution Error: Neither premise's substitution matches the conclusion."); } else if (first_0) { @@ -799,5 +799,5 @@ proc_fv (unsigned char * prem_0, unsigned char * prem_1, unsigned char * conc) if (ret == 0) return CORRECT; - return _("Free Variable Substitution constructed incorrectly."); + return _("Free Variable Substitution Error: The substitution does not match the conclusion."); }