Various I/Q and IC2 improvements#259
Merged
Merged
Conversation
hanno-becker
commented
Jul 15, 2026
hanno-becker
commented
Collaborator
- Builds on IC2: Separate check into update / evaluate / stop steps #258
hanno-becker
force-pushed
the
iq_ic2_improvements
branch
from
12caa9c to
dc0f3d6
Compare
Extended_Query_Operation no longer depends on jEdit's Editor. It takes (session: Session, host: Extended_Query_Operation.Host), where Host abstracts the editor-specific capabilities a query needs — overlay insert/remove, flush, dispatch. The overlay-query lifecycle runs on the generic Session API, so it works for the live PIDE session and a headless Headless.Session alike. The caret-driven apply_query and GUI locate_query are dropped; callers resolve the target command and drive apply_query_at_command. The jEdit Host (IQ_Editor_Host, backed by PIDE.editor) is shared by both I/Q call sites; the dockable reimplements caret resolution and hyperlink locally. Extended_Query_Operation.scala is symlinked into ic2/src for later headless use. Inserting the overlay makes its command visible (Thy_Syntax.command_perspective folds overlay-bearing commands into the visible set), so the print function runs even for a command processed but never scrolled into view. Building on that: add a `state` query to the explore MCP tool (print_state, a core query function), and augment get_command_info's results_text with the proof state from a print_state query instead of only the passive command_results read. Signed-off-by: Hanno Becker <[email protected]>
SessionTools.goalState no longer reads proof state passively from per-command STATE messages. It queries it ON DEMAND via a print_state Extended_Query_- Operation fired at the command, then runs analyzeGoalMessages over the result. This removes the need to force show_states / editor_output_state in the daemon (dropped): we no longer emit a STATE message for every evaluated command, and goal state is now available regardless of whether one was ever produced. Inserting the query's overlay makes the command visible, so print_state runs even for a headless session with an empty perspective. New session-generic pieces in SessionTools (shared by IC2 and, later, I/Q): Session_Query_Host, an Extended_Query_Operation.Host pushing overlay edits via session.update (no editor), and queryProofState, which fires the query and blocks for the instance-tagged result. get_state_at / get_context_info / get_command_info are unchanged at the call site — they go through goalState. Signed-off-by: Hanno Becker <[email protected]>
- state_at_returns_goal: get_state_at at a proof command returns real goal text + subgoal count via the print_state query, and has_goal:false at a definition. - state_at_never_visible: a freshly-checked, never-viewed theory's deep proof command still yields its goal — proving the query recovers state where the removed show_states / passive read would have found nothing (headless nodes are never visible; the query's overlay makes the command visible). Signed-off-by: Hanno Becker <[email protected]>
resolveNode's "exists but is not a loaded session node (check it first...)" was misleading for a theory built into the session HEAP: it is fully available, just not a live document node, and "check it first" is useless advice for it. Distinguish the cases: if the file resolves (via resources.find_theory) to a theory that resources.loaded_theory confirms is in the heap image, say so — its per-command state isn't in the live document, so per-command queries don't apply. Otherwise keep the "check it first / outside the session" message. Adds query_heap_theory_message covering get_diagnostics on a heap theory. Signed-off-by: Hanno Becker <[email protected]>
Previously, when a check failed the error message was only delivered as a live Event.Error to currently-attached subscribers (check attach / MCP). A detached poll via `isabelle ic2 check status` saw only "failed reason=errors" with no indication of WHERE or WHY it failed, because statusJson carried only numeric per-node counts. Fix: latch the first Event.Error on the Job (in `fan`) so the location (theory, file, line) and message text are retained independently of subscriber presence. Expose this as an `error` object in statusJson, and render it in the CLI `check status` output. Signed-off-by: Hanno Becker <[email protected]>
cancelFrontier previously used is_finished (which excludes failed commands: !failed && touched && forks==0 && runs==0) to determine the edit frontier. This caused failed commands to be re-edited away during the first-error stop, destroying their error diagnostics from the document — making query diagnostics / document-info report 0 errors even though the check failed. Fix: use maybe_consolidated (touched && forks==0 && runs==0) instead, which treats failed commands as settled. The cancel-via-edit now cuts only from the first genuinely-still-in-flight command, preserving failed commands and their error markup in the document for subsequent diagnostic queries. Signed-off-by: Hanno Becker <[email protected]>
hanno-becker
force-pushed
the
iq_ic2_improvements
branch
from
dc0f3d6 to
df8b137
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.