jEdit unresponsive when running Assistant command from the context menu
- Dominant language
- Isabelle
- Stars
- 105
- Forks
- 27
- Avg merge
- 12h 45m
- Merged PRs (30d)
- 7
Description
Using 72160e202330fc050732f40648ec16b7628bee15 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 91a421b16a3d68561d6afba4f5f3307eb0fd79b1).
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): No facts in scope.
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
```
Contributor guide
Research direction
Reproduce the freeze in jEdit by running Assistant commands such as “Explain Error,” “Find Theorems,” or “Tidy” from the context menu at the reported commit. Start with the Isabelle/Q Server and MCP request flow shown in the issue, comparing behavior with commit 91a421b16a3d68561d6afba4f5f3307eb0fd79b1. Done means the context menu no longer makes jEdit unresponsive while processing the command.
Written by the indexing model from the issue text.
Assessment
- Domain
- desktop, tooling
- Issue type
- Bug
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Stale
- Clarity
- Needs clarification
- Newbie friendliness
- 35/100