Message handler: add quote_begin, quote_end commands

[tautschnig]

These will permit custom formatting of quoting for each message handler, and for a start introduce tags for XML. See #4875 for discussion.

Please review commit-by-commit.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

❌ Patch coverage is 39.58333% with 58 lines in your changes missing coverage. Please review.
✅ Project coverage is 80.54%. Comparing base (7c0ce54) to head (9e46e97).
⚠️ Report is 7 commits behind head on develop.

Files with missing lines	Patch %	Lines
src/goto-analyzer/taint_parser.cpp	0.00%	16 Missing ⚠️
src/util/ui_message.h	39.13%	14 Missing ⚠️
src/statement-list/statement_list_entry_point.cpp	0.00%	8 Missing ⚠️
src/ansi-c/c_typecheck_code.cpp	0.00%	4 Missing ⚠️
src/ansi-c/c_typecheck_base.cpp	0.00%	3 Missing ⚠️
src/solvers/strings/string_refinement.cpp	0.00%	3 Missing ⚠️
src/ansi-c/c_typecheck_expr.cpp	0.00%	2 Missing ⚠️
src/cpp/cpp_instantiate_template.cpp	0.00%	2 Missing ⚠️
src/cpp/cpp_typecheck_expr.cpp	0.00%	2 Missing ⚠️
src/cpp/cpp_typecheck_function.cpp	0.00%	2 Missing ⚠️
... and 1 more

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #5696      +/-   ##
===========================================
- Coverage    80.55%   80.54%   -0.02%     
===========================================
  Files         1707     1707              
  Lines       189051   189101      +50     
  Branches        73       73              
===========================================
+ Hits        152298   152315      +17     
- Misses       36753    36786      +33     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

[martin-cs]

Seems good. It would be nice if this also had the implementation of this for XML so that it was clear why it was valueable and no-one will accidentally 'simplify' it out.

[Copilot]

Pull request overview

This PR adds explicit quote delimiter commands to the messaging subsystem so message handlers can render quoted fragments consistently across UIs (plain/XML/JSON), and updates various diagnostics to use the new quote delimiters.

Changes:

• Introduce messaget::quote_begin / messaget::quote_end commands and map them in message handlers.
• Update many user-facing messages to use the new quote commands instead of hardcoded backticks/quotes.
• Update regression expectations to match the new quote rendering.

Reviewed changes

Copilot reviewed 24 out of 24 changed files in this pull request and generated 4 comments.

Show a summary per file

File	Description
src/util/ui_message.h	Intercepts new quote commands (and some styling commands) depending on UI mode before delegating to underlying handler
src/util/message.h	Declares new quote commands on messaget
src/util/message.cpp	Defines the new quote command values ('<' and '>')
src/util/cout_message.cpp	Renders quote commands in the console handler
src/statement-list/statement_list_entry_point.cpp	Uses quote commands in “main symbol …” diagnostics
src/solvers/strings/string_refinement.cpp	Uses quote commands in debug rendering of concretized strings
src/solvers/smt2/smt2_dec.cpp	Uses quote commands around returned solver error message text
src/linking/linking_diagnostics.cpp	Uses quote commands for symbol/module names in diagnostics
src/linking/linking.cpp	Uses quote commands for quoted variable name in warning
src/goto-cc/compile.cpp	Uses quote commands around deprecated flag names
src/goto-analyzer/taint_parser.cpp	Uses quote commands around JSON field/key values in diagnostics
src/cpp/cpp_typecheck_function.cpp	Uses quote commands in internal error message
src/cpp/cpp_typecheck_expr.cpp	Uses quote commands for “this” keyword
src/cpp/cpp_instantiate_template.cpp	Uses quote commands for “virtual” keyword
src/ansi-c/c_typecheck_expr.cpp	Uses quote commands around identifiers in error message
src/ansi-c/c_typecheck_code.cpp	Uses quote commands around “case” keyword in error message
src/ansi-c/c_typecheck_base.cpp	Uses quote commands for “extern” and symbol name in warning message
regression/goto-cc-file-local/old-flag-name/test.desc	Updates expected output for deprecated flag warning to use single quotes
jbmc/src/java_bytecode/java_class_loader_base.cpp	Uses quote commands around filesystem paths in warnings
jbmc/src/java_bytecode/java_bytecode_parser.cpp	Uses quote commands around class name in debug output
jbmc/regression/jbmc/lambda2/test.desc	Updates expected output to single-quote class name
jbmc/regression/jbmc/lambda1/test_goto_functions.desc	Updates expected output to single-quote class names
jbmc/regression/jbmc/classpath-invalid/test_path_warning.desc	Updates expected output to single-quote path
jbmc/regression/jbmc/classpath-invalid/test_jar_warning.desc	Updates expected output to single-quote path

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.