# HG changeset patch # User wenzelm # Date 1526306410 -7200 # Node ID fa3cf61121ee0bdf958770e11fb90c8ead229139 # Parent 34592bf86424290ea281a3efe26babe10bbd11cd tuned signature (see Command.eval_state); diff -r 34592bf86424 -r fa3cf61121ee src/Pure/Thy/thy_info.ML --- 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; diff -r 34592bf86424 -r fa3cf61121ee src/Pure/Thy/thy_output.ML --- 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 *)