tuned signature (see Command.eval_state);

--- a/src/Pure/Thy/thy_info.ML	Mon May 14 14:30:13 2018 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon May 14 16:00:10 2018 +0200
@@ -51,7 +51,7 @@
 
 val _ =
   Theory.setup (add_presentation (fn {options, pos, segments} => fn thy =>
-    if exists (Toplevel.is_skipped_proof o #result_state) segments then ()
+    if exists (Toplevel.is_skipped_proof o #state) segments then ()
     else
       let
         val body = Thy_Output.present_thy thy segments;
@@ -319,7 +319,7 @@
     fun present () =
       let
         val segments = (spans ~~ maps Toplevel.join_results results)
-          |> map (fn (span, (tr, st')) => {span = span, tr = tr, result_state = st'});
+          |> map (fn (span, (tr, st')) => {span = span, command = tr, state = st'});
         val context = {options = options, pos = text_pos, segments = segments};
       in apply_presentation context thy end;
   in (thy, present, size text) end;

--- a/src/Pure/Thy/thy_output.ML	Mon May 14 14:30:13 2018 +0200
+++ b/src/Pure/Thy/thy_output.ML	Mon May 14 16:00:10 2018 +0200
@@ -10,7 +10,7 @@
   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
@@ -338,7 +338,7 @@
 
 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
@@ -415,8 +415,8 @@
       |> 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 *)