Returns a typed representation of common Isabelle server results.

Recognizes session_start, session_build, and use_theories result shapes. Unknown shapes are returned unchanged.

Returns diagnostic messages from a task, result, or task notes.

This works for use_theories final results and for message-shaped task notes produced by async commands such as session_build and session_start.

Pass line: n, line: first..last, or line: [n, ...] to keep only diagnostics whose position has that source line. Pass offset: n to keep only diagnostics whose pos.offset..pos.end_offset range contains n. Pass file: path or file: [path, ...] to keep only diagnostics whose position has that file. Offsets are Isabelle symbol offsets from the beginning of the whole source file, not columns within the line.

Raw result maps return raw diagnostic maps; structured results return typed %IsabelleClient.Result.Message{} values.

Returns error messages from a task or result map.

This includes Isabelle's cumulative top-level "errors" list and node-level or note diagnostics whose kind is "error".

Returns typed exports from all theory nodes in a use_theories result.

Extracts the session_id from a session-start task or result map.

Returns user-facing message strings from a task, result map, or task notes.

Accepts the same :file, :line, and :offset filters as diagnostics/2.

Finds a typed theory node by node_name or theory_name.

Returns typed theory nodes from a use_theories result.

Decodes a session_build result or task, or returns nil for another shape.

Returns typed top-level error messages from a use_theories result.

Decodes a use_theories result or task, or returns nil for another shape.

Returns warning messages from a task or result map, with optional position filters.