diff -r c0bfa2aa6b68 -r 1dd29afaddda src/Pure/Thy/document_output.ML
--- a/src/Pure/Thy/document_output.ML	Sun Jun 01 15:35:28 2025 +0200
+++ b/src/Pure/Thy/document_output.ML	Sun Jun 01 16:43:09 2025 +0200
@@ -16,6 +16,8 @@
   type segment =
     {span: Command_Span.span, command: Toplevel.transition,
      prev_state: Toplevel.state, state: Toplevel.state}
+  val segment_eof: segment
+  val segment_stopper: segment Scan.stopper
   val present_thy: Options.T -> Keyword.keywords -> string -> segment list -> Latex.text
   val pretty_term: Proof.context -> term -> Pretty.T
   val pretty_thm: Proof.context -> thm -> Pretty.T
@@ -371,6 +373,14 @@
   {span: Command_Span.span, command: Toplevel.transition,
    prev_state: Toplevel.state, state: Toplevel.state};
 
+val segment_eof: segment =
+  {span = Command_Span.eof, command = Toplevel.empty,
+   prev_state = Toplevel.make_state NONE, state = Toplevel.make_state NONE};
+
+val segment_stopper =
+  Scan.stopper (K segment_eof) (Command_Span.is_eof o #span);
+
+
 local
 
 val markup_true = "\\isamarkuptrue%\n";