I/R: Add Ir.init_with_header for keyword-aware theory init

[ike-mulder-aws]

A .thy file may declare new outer-syntax keywords in its header (theory T imports Main keywords "frobnicate" :: thy_decl begin). Ir.init has no way to declare such keywords on the new theory, so a subsequent ML step using
Outer_Syntax.local_theory @{command_keyword frobnicate} fails with "Bad outer syntax command". This blocks replaying any .thy that declares new keywords.

Add Ir.init_with_header taking a {clauses: string} record. The clauses text is the literal content between imports ... and begin in a .thy header — typically a keywords clause. We synthesize a fake header, parse it via Thy_Header.read, and chain Thy_Header.add_keywords on the freshly-built theory. The other valid header clause — abbrevs, declaring jEdit autocomplete abbreviations — is parsed-and-discarded by Isabelle itself (it has no ML-level effect), so extracting #keywords captures everything that matters at the theory level.

Ir.init becomes a one-line forwarder: no caller breakage. Segment specs are rejected when clauses is non-empty — recorded segments already carry their .thy's keywords.

Tests:

• test_register_keyword_fails_without_header: demonstrates the gap.
• test_init_with_header_succeeds_for_keyword: inverse, with the same ML step succeeding once keywords are declared at init time.
• test_init_with_header_empty_clauses_is_noop and test_init_with_header_rejects_segment.

Issue #, if available:

Description of changes:

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.