src/Pure/Thy/thy_output.ML

 sig
   val output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text list
   val check_comments: Proof.context -> Symbol_Pos.T list -> unit
   val output_token: Proof.context -> Token.T -> Latex.text list
   val output_source: Proof.context -> string -> Latex.text list
-  type segment = {span: Command_Span.span, tr: Toplevel.transition, result_state: Toplevel.state}
+  type segment = {span: Command_Span.span, command: Toplevel.transition, state: Toplevel.state}
   val present_thy: theory -> segment list -> Latex.text list
   val pretty_term: Proof.context -> term -> Pretty.T
   val pretty_thm: Proof.context -> thm -> Pretty.T
   val lines: Latex.text list -> Latex.text list
   val items: Latex.text list -> Latex.text list

   Scan.option ((Parse.$$$ "(" -- improper -- Parse.$$$ "in") |--
     Parse.!!! (improper |-- Parse.name --| (improper -- Parse.$$$ ")")));
 
 in
 
-type segment = {span: Command_Span.span, tr: Toplevel.transition, result_state: Toplevel.state};
+type segment = {span: Command_Span.span, command: Toplevel.transition, state: Toplevel.state};
 
 fun present_thy thy (segments: segment list) =
   let
     val keywords = Thy_Header.get_keywords thy;
 

       |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk tokens >> flat))
       |> Source.source stopper (Scan.error (Scan.bulk span))
       |> Source.exhaust;
 
     val command_results =
-      segments |> map_filter (fn {tr, result_state, ...} =>
-        if Toplevel.is_ignored tr then NONE else SOME (tr, result_state));
+      segments |> map_filter (fn {command, state, ...} =>
+        if Toplevel.is_ignored command then NONE else SOME (command, state));
 
 
     (* present commands *)
 
     val document_tags = space_explode "," (Options.default_string \<^system_option>\<open>document_tags\<close>);