jEdit unresponsive when running Assistant command from the context menu

[kappelmann]

Using 72160e2 jEdit freezes when using commands from the context menu ("Explain Error", "Find Theorems", "Tidy", etc.). It seems to recover once the Assistant is finished processing the command.

I suppose this is not expected behaviour since jEdit did not freeze in earlier commits (up to and including 91a421b).

Here's the Isabelle/Q server output for one such problem instance:

Isabelle/Q Server Output:
==================================================
[08:29:59] Log cleared
[08:30:14] MCP: 08:30:14.351 [RECV] {"jsonrpc":"2.0","id":"assistant-30","method":"ping"}
[08:30:14] MCP: 08:30:14.351 [SEND] {"jsonrpc":"2.0","id":"assistant-30","result":{"status":"ok","timestamp":1773217814351}}
[08:30:45] MCP: 08:30:17.220 [RECV] {"jsonrpc":"2.0","id":"assistant-31","method":"tools/call","params":{"name":"resolve_command_target","arguments":{"command_selection":"file_offset","path":"/Users/kevin/Programming/isabelle/AutoCorrode/isabelle-assistant/Scratch.thy","offset":80}}}
[08:30:45] MCP client connected
[08:30:45] MCP: 08:30:24.224 [RECV] {"jsonrpc":"2.0","id":"assistant-31","method":"tools/call","params":{"name":"resolve_command_target","arguments":{"command_selection":"file_offset","path":"/Users/kevin/Programming/isabelle/AutoCorrode/isabelle-assistant/Scratch.thy","offset":80}}}
[08:30:45] MCP client connected
[08:30:45] MCP: 08:30:31.227 [RECV] {"jsonrpc":"2.0","id":"assistant-33","method":"ping"}
[08:30:45] MCP: 08:30:31.229 [SEND] {"jsonrpc":"2.0","id":"assistant-33","result":{"status":"ok","timestamp":1773217831228}}
[08:30:45] MCP: 08:30:31.230 [RECV] {"jsonrpc":"2.0","id":"assistant-32","method":"tools/call","params":{"name":"get_context_info","arguments":{"command_selection":"file_offset","path":"/Users/kevin/Programming/isabelle/AutoCorrode/isabelle-assistant/Scratch.thy","offset":80}}}
[08:30:45] MCP client connected
[08:30:45] MCP: 08:30:38.233 [RECV] {"jsonrpc":"2.0","id":"assistant-32","method":"tools/call","params":{"name":"get_context_info","arguments":{"command_selection":"file_offset","path":"/Users/kevin/Programming/isabelle/AutoCorrode/isabelle-assistant/Scratch.thy","offset":80}}}
[08:30:45] MCP: 08:30:45.267 [SEND] {"jsonrpc":"2.0","id":"assistant-31","result":{"content":[{"type":"text","text":"{\"selection\":{\"command_selection\":\"file_offset\",\"path\":\"/Users/kevin/Programming/isabelle/AutoCorrode/isabelle-assistant/Scratch.thy\",\"req...[598 chars total]..."source\":\"fun add :: ‹nat ⇒ nat ⇒ nat› where\\n  ‹add 0 n = n›\\n| ‹add (Suc m) n = Suc (add m n)›\",\"node_path\":\"/Users/kevin/Programming/isabelle/AutoCorrode/isabelle-assistant/Scratch.thy\",\"keyword\":\"fun\",\"id\":-140,\"length\":84}}"}]}}
[08:30:45] MCP client connected
[08:30:45] MCP: 08:30:45.270 [SEND] {"jsonrpc":"2.0","id":"assistant-31","result":{"content":[{"type":"text","text":"{\"selection\":{\"command_selection\":\"file_offset\",\"path\":\"/Users/kevin/Programming/isabelle/AutoCorrode/isabelle-assistant/Scratch.thy\",\"req...[598 chars total]..."source\":\"fun add :: ‹nat ⇒ nat ⇒ nat› where\\n  ‹add 0 n = n›\\n| ‹add (Suc m) n = Suc (add m n)›\",\"node_path\":\"/Users/kevin/Programming/isabelle/AutoCorrode/isabelle-assistant/Scratch.thy\",\"keyword\":\"fun\",\"id\":-140,\"length\":84}}"}]}}
[08:30:45] MCP client connected
[08:30:45] MCP: 08:30:45.270 [SEND] {"jsonrpc":"2.0","id":"assistant-32","result":{"content":[{"type":"text","text":"{\"in_proof_context\":false,\"has_goal\":false,\"goal\":{\"goal_text\":\"\",\"num_subgoals\":0,\"has_goal\":false,\"free_vars\":[],\"constants\":[]},...[746 chars total]...hy\",\"keyword\":\"fun\",\"id\":-140,\"length\":84},\"selection\":{\"command_selection\":\"file_offset\",\"path\":\"/Users/kevin/Programming/isabelle/AutoCorrode/isabelle-assistant/Scratch.thy\",\"requested_offset\":80,\"normalized_offset\":80}}"}]}}
[08:30:45] MCP: 08:30:45.270 [SEND] {"jsonrpc":"2.0","id":"assistant-32","result":{"content":[{"type":"text","text":"{\"in_proof_context\":false,\"has_goal\":false,\"goal\":{\"goal_text\":\"\",\"num_subgoals\":0,\"has_goal\":false,\"free_vars\":[],\"constants\":[]},...[746 chars total]...hy\",\"keyword\":\"fun\",\"id\":-140,\"length\":84},\"selection\":{\"command_selection\":\"file_offset\",\"path\":\"/Users/kevin/Programming/isabelle/AutoCorrode/isabelle-assistant/Scratch.thy\",\"requested_offset\":80,\"normalized_offset\":80}}"}]}}
[08:30:45] MCP client connected
[08:30:45] MCP client disconnected
[08:30:45] MCP client connected
[08:30:45] MCP: 08:30:45.278 [RECV] {"jsonrpc":"2.0","id":"assistant-34","method":"tools/call","params":{"name":"get_proof_context","arguments":{"command_selection":"file_offset","path":"/Users/kevin/Programming/isabelle/AutoCorrode/isabelle-assistant/Scratch.thy","offset":167}}}
[08:30:45] MCP: 08:30:45.533 [SEND] {"jsonrpc":"2.0","id":"assistant-34","result":{"content":[{"type":"text","text":"{\"success\":true,\"has_context\":true,\"context\":\"No facts in scope.\",\"timed_out\":false,\"command\":{\"end_offset\":169,\"start_offset\":164,\"...[662 chars total]...":5},\"selection\":{\"command_selection\":\"file_offset\",\"path\":\"/Users/kevin/Programming/isabelle/AutoCorrode/isabelle-assistant/Scratch.thy\",\"requested_offset\":167,\"normalized_offset\":167},\"message\":\"Query completed successfully\"}"}]}}
[08:30:45] MCP: 08:30:45.544 [RECV] {"jsonrpc":"2.0","id":"assistant-35","method":"tools/call","params":{"name":"get_context_info","arguments":{"command_selection":"file_offset","path":"/Users/kevin/Programming/isabelle/AutoCorrode/isabelle-assistant/Scratch.thy","offset":167}}}
[08:30:45] MCP: 08:30:45.550 [SEND] {"jsonrpc":"2.0","id":"assistant-35","result":{"content":[{"type":"text","text":"{\"in_proof_context\":false,\"has_goal\":false,\"goal\":{\"goal_text\":\"\",\"num_subgoals\":0,\"has_goal\":false,\"free_vars\":[],\"constants\":[]},...[672 chars total]....thy\",\"keyword\":\"\",\"id\":-217,\"length\":5},\"selection\":{\"command_selection\":\"file_offset\",\"path\":\"/Users/kevin/Programming/isabelle/AutoCorrode/isabelle-assistant/Scratch.thy\",\"requested_offset\":167,\"normalized_offset\":167}}"}]}}
[08:30:46] MCP: 08:30:46.235 [RECV] {"jsonrpc":"2.0","id":"assistant-36","method":"ping"}
[08:30:46] MCP: 08:30:46.236 [SEND] {"jsonrpc":"2.0","id":"assistant-36","result":{"status":"ok","timestamp":1773217846236}}
[08:31:01] MCP: 08:31:01.241 [RECV] {"jsonrpc":"2.0","id":"assistant-37","method":"ping"}
[08:31:01] MCP: 08:31:01.242 [SEND] {"jsonrpc":"2.0","id":"assistant-37","result":{"status":"ok","timestamp":1773217861242}}

And here's the corresponding console output from the Isabelle/jEdit process

08:30:14 [pool-1-thread-5] [error] pool-1-thread-5: I/Q Server: Sending response of length 88 chars
08:30:14 [pool-1-thread-5] [error] pool-1-thread-5: I/Q Server: About to send 89 bytes
08:30:14 [pool-1-thread-5] [error] pool-1-thread-5: I/Q Server: Response sent and flushed (89 bytes)
08:30:14 [pool-1-thread-5] [error] pool-1-thread-5: I/Q Server: Writer status OK after sending response
08:30:24 [iq-mcp-accept-loop] [error] iq-mcp-accept-loop: MCP Client connected: /127.0.0.1:53935
08:30:24 [pool-1-thread-6] [error] pool-1-thread-6: MCP Client connected with buffer size: 65536 (no timeout)
08:30:31 [iq-mcp-accept-loop] [error] iq-mcp-accept-loop: MCP Client connected: /127.0.0.1:53938
08:30:31 [pool-1-thread-7] [error] pool-1-thread-7: MCP Client connected with buffer size: 65536 (no timeout)
08:30:31 [pool-1-thread-7] [error] pool-1-thread-7: I/Q Server: Sending response of length 88 chars
08:30:31 [pool-1-thread-7] [error] pool-1-thread-7: I/Q Server: About to send 89 bytes
08:30:31 [pool-1-thread-7] [error] pool-1-thread-7: I/Q Server: Response sent and flushed (89 bytes)
08:30:31 [pool-1-thread-7] [error] pool-1-thread-7: I/Q Server: Writer status OK after sending response
08:30:38 [iq-mcp-accept-loop] [error] iq-mcp-accept-loop: MCP Client connected: /127.0.0.1:53945
08:30:38 [pool-1-thread-8] [error] pool-1-thread-8: MCP Client connected with buffer size: 65536 (no timeout)
08:30:45 [pool-1-thread-5] [error] pool-1-thread-5: I/Q Server: Sending response of length 578 chars
08:30:45 [pool-1-thread-5] [error] pool-1-thread-5: I/Q Server: About to send 595 bytes
08:30:45 [pool-1-thread-5] [error] pool-1-thread-5: I/Q Server: Response sent and flushed (595 bytes)
08:30:45 [pool-1-thread-5] [error] pool-1-thread-5: I/Q Server: Writer status OK after sending response
08:30:45 [pool-1-thread-5] [error] pool-1-thread-5: MCP Client disconnected
08:30:45 [pool-1-thread-6] [error] pool-1-thread-6: I/Q Server: Sending response of length 578 chars
08:30:45 [pool-1-thread-6] [error] pool-1-thread-6: I/Q Server: About to send 595 bytes
08:30:45 [pool-1-thread-6] [error] pool-1-thread-6: I/Q Server: Response sent and flushed (595 bytes)
08:30:45 [pool-1-thread-6] [error] pool-1-thread-6: I/Q Server: Writer status OK after sending response
08:30:45 [pool-1-thread-6] [error] pool-1-thread-6: Error handling MCP client: Connection reset
08:30:45 [pool-1-thread-6] [error] pool-1-thread-6: MCP Client disconnected
08:30:45 [pool-1-thread-7] [error] pool-1-thread-7: I/Q Server: Sending response of length 726 chars
08:30:45 [pool-1-thread-8] [error] pool-1-thread-8: I/Q Server: Sending response of length 726 chars
08:30:45 [pool-1-thread-8] [error] pool-1-thread-8: I/Q Server: About to send 743 bytes
08:30:45 [pool-1-thread-7] [error] pool-1-thread-7: I/Q Server: About to send 743 bytes
08:30:45 [pool-1-thread-8] [error] pool-1-thread-8: I/Q Server: Response sent and flushed (743 bytes)
08:30:45 [pool-1-thread-8] [error] pool-1-thread-8: I/Q Server: Writer status OK after sending response
08:30:45 [pool-1-thread-7] [error] pool-1-thread-7: I/Q Server: Response sent and flushed (743 bytes)
08:30:45 [pool-1-thread-7] [error] pool-1-thread-7: I/Q Server: Writer status OK after sending response
08:30:45 [pool-1-thread-8] [error] pool-1-thread-8: Error handling MCP client: Connection reset
08:30:45 [pool-1-thread-7] [error] pool-1-thread-7: Error handling MCP client: Connection reset
08:30:45 [pool-1-thread-8] [error] pool-1-thread-8: MCP Client disconnected
08:30:45 [pool-1-thread-7] [error] pool-1-thread-7: MCP Client disconnected
08:30:45 [iq-mcp-accept-loop] [error] iq-mcp-accept-loop: MCP Client connected: /127.0.0.1:53946
08:30:45 [pool-1-thread-9] [error] pool-1-thread-9: MCP Client connected with buffer size: 65536 (no timeout)
08:30:45 [pool-1-thread-9] [error] pool-1-thread-9: I/Q Server: Starting query execution for isar_explore with arguments: List(print_context)
08:30:45 [AWT-EventQueue-0] [error] AWT-EventQueue-0: I/Q Server: Creating Extended_Query_Operation for isar_explore
08:30:45 [AWT-EventQueue-0] [error] AWT-EventQueue-0: I/Q Server: Activating operation and applying query
08:30:45 [AWT-EventQueue-0] [error] AWT-EventQueue-0: I/Q Server: Formatted args: List(print_context)
08:30:45 [AWT-EventQueue-0] [error] AWT-EventQueue-0: I/Q Server: outputCallback called with 0 XML trees
08:30:45 [AWT-EventQueue-0] [error] AWT-EventQueue-0: I/Q Server: Status changed to inactive
08:30:45 [AWT-EventQueue-0] [error] AWT-EventQueue-0: I/Q Server: Status changed to waiting
08:30:45 [pool-1-thread-9] [error] pool-1-thread-9: I/Q Server: Waiting for query completion (timeout: 30000ms)
08:30:45 [AWT-EventQueue-0] [error] AWT-EventQueue-0: I/Q Server: Status changed to running
08:30:45 [AWT-EventQueue-0] [error] AWT-EventQueue-0: I/Q Server: outputCallback called with 1 XML trees
08:30:45 [AWT-EventQueue-0] [error] AWT-EventQueue-0: I/Q Server: Received XML (Elem): <writeln_message>No facts in scope.</writeln_message>
08:30:45 [AWT-EventQueue-0] [error] AWT-EventQueue-0: I/Q Server: Status changed to finished
08:30:45 [AWT-EventQueue-0] [error] AWT-EventQueue-0: I/Q Server: Query completed, hasError=false
08:30:45 [pool-1-thread-9] [error] pool-1-thread-9: I/Q Server: Finished waiting after 248ms, isFinished=true
08:30:45 [pool-1-thread-9] [error] pool-1-thread-9: I/Q Server: Deactivating operation
08:30:45 [AWT-EventQueue-0] [error] AWT-EventQueue-0: I/Q Server: outputCallback called with 0 XML trees
08:30:45 [AWT-EventQueue-0] [error] AWT-EventQueue-0: I/Q Server: Status changed to inactive
08:30:45 [pool-1-thread-9] [error] pool-1-thread-9: I/Q Server: Getting results as string, xmlResults.size=1
08:30:45 [pool-1-thread-9] [error] pool-1-thread-9: I/Q Server: XML result types: Elem
08:30:45 [pool-1-thread-9] [error] pool-1-thread-9: I/Q Server: Extracted content: No facts in scope.
08:30:45 [pool-1-thread-9] [error] pool-1-thread-9: I/Q Server: Sending response of length 642 chars
08:30:45 [pool-1-thread-9] [error] pool-1-thread-9: I/Q Server: About to send 643 bytes
08:30:45 [pool-1-thread-9] [error] pool-1-thread-9: I/Q Server: Response sent and flushed (643 bytes)
08:30:45 [pool-1-thread-9] [error] pool-1-thread-9: I/Q Server: Writer status OK after sending response
08:30:45 [pool-1-thread-9] [error] pool-1-thread-9: I/Q Server: Sending response of length 652 chars
08:30:45 [pool-1-thread-9] [error] pool-1-thread-9: I/Q Server: About to send 653 bytes
08:30:45 [pool-1-thread-9] [error] pool-1-thread-9: I/Q Server: Response sent and flushed (653 bytes)
08:30:45 [pool-1-thread-9] [error] pool-1-thread-9: I/Q Server: Writer status OK after sending response
08:30:45 [Isabelle.assistant-tidy] [error] assistant-tidy: [Assistant] invokeStructuredChat - Model: global.anthropic.claude-opus-4-6-v1, Schema: return_code, Messages: 1
08:30:46 [pool-1-thread-9] [error] pool-1-thread-9: I/Q Server: Sending response of length 88 chars
08:30:46 [pool-1-thread-9] [error] pool-1-thread-9: I/Q Server: About to send 89 bytes
08:30:46 [pool-1-thread-9] [error] pool-1-thread-9: I/Q Server: Response sent and flushed (89 bytes)
08:30:46 [pool-1-thread-9] [error] pool-1-thread-9: I/Q Server: Writer status OK after sending response
08:30:48 [Isabelle.assistant-tidy] [error] assistant-tidy: [Assistant] invokeInContextStructured completed in 3423ms
08:31:01 [pool-1-thread-9] [error] pool-1-thread-9: I/Q Server: Sending response of length 88 chars
08:31:01 [pool-1-thread-9] [error] pool-1-thread-9: I/Q Server: About to send 89 bytes
08:31:01 [pool-1-thread-9] [error] pool-1-thread-9: I/Q Server: Response sent and flushed (89 bytes)
08:31:01 [pool-1-thread-9] [error] pool-1-thread-9: I/Q Server: Writer status OK after sending response
08:31:16 [pool-1-thread-9] [error] pool-1-thread-9: I/Q Server: Sending response of length 88 chars
08:31:16 [pool-1-thread-9] [error] pool-1-thread-9: I/Q Server: About to send 89 bytes
08:31:16 [pool-1-thread-9] [error] pool-1-thread-9: I/Q Server: Response sent and flushed (89 bytes)
08:31:16 [pool-1-thread-9] [error] pool-1-thread-9: I/Q Server: Writer status OK after sending response

[hanno-becker]

@kappelmann Thank you! Can you double-check that the issue exists on main as well? 57c513f should have fixed some freezing issue, but I don't know if it's your's.

[kappelmann]

Works again in 3c6212e - thanks!

[kappelmann]

My fault (I forgot to re-install the plugin after updating): the problem is still there in 3c6212e
Sorry @hanno-becker

[hanno-becker]

@dominic-mulligan-aws can you take a look? I suspect some command is unnecessarily forced to run in the GUI Thread.