tuned signature (see Command.eval_state);
authorwenzelm
Mon May 14 16:00:10 2018 +0200 (12 months ago)
changeset 68182fa3cf61121ee
parent 68181 34592bf86424
child 68183 6560324b1e4d
tuned signature (see Command.eval_state);
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Thy/thy_info.ML	Mon May 14 14:30:13 2018 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Mon May 14 16:00:10 2018 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4  
     1.5  val _ =
     1.6    Theory.setup (add_presentation (fn {options, pos, segments} => fn thy =>
     1.7 -    if exists (Toplevel.is_skipped_proof o #result_state) segments then ()
     1.8 +    if exists (Toplevel.is_skipped_proof o #state) segments then ()
     1.9      else
    1.10        let
    1.11          val body = Thy_Output.present_thy thy segments;
    1.12 @@ -319,7 +319,7 @@
    1.13      fun present () =
    1.14        let
    1.15          val segments = (spans ~~ maps Toplevel.join_results results)
    1.16 -          |> map (fn (span, (tr, st')) => {span = span, tr = tr, result_state = st'});
    1.17 +          |> map (fn (span, (tr, st')) => {span = span, command = tr, state = st'});
    1.18          val context = {options = options, pos = text_pos, segments = segments};
    1.19        in apply_presentation context thy end;
    1.20    in (thy, present, size text) end;
     2.1 --- a/src/Pure/Thy/thy_output.ML	Mon May 14 14:30:13 2018 +0200
     2.2 +++ b/src/Pure/Thy/thy_output.ML	Mon May 14 16:00:10 2018 +0200
     2.3 @@ -10,7 +10,7 @@
     2.4    val check_comments: Proof.context -> Symbol_Pos.T list -> unit
     2.5    val output_token: Proof.context -> Token.T -> Latex.text list
     2.6    val output_source: Proof.context -> string -> Latex.text list
     2.7 -  type segment = {span: Command_Span.span, tr: Toplevel.transition, result_state: Toplevel.state}
     2.8 +  type segment = {span: Command_Span.span, command: Toplevel.transition, state: Toplevel.state}
     2.9    val present_thy: theory -> segment list -> Latex.text list
    2.10    val pretty_term: Proof.context -> term -> Pretty.T
    2.11    val pretty_thm: Proof.context -> thm -> Pretty.T
    2.12 @@ -338,7 +338,7 @@
    2.13  
    2.14  in
    2.15  
    2.16 -type segment = {span: Command_Span.span, tr: Toplevel.transition, result_state: Toplevel.state};
    2.17 +type segment = {span: Command_Span.span, command: Toplevel.transition, state: Toplevel.state};
    2.18  
    2.19  fun present_thy thy (segments: segment list) =
    2.20    let
    2.21 @@ -415,8 +415,8 @@
    2.22        |> Source.exhaust;
    2.23  
    2.24      val command_results =
    2.25 -      segments |> map_filter (fn {tr, result_state, ...} =>
    2.26 -        if Toplevel.is_ignored tr then NONE else SOME (tr, result_state));
    2.27 +      segments |> map_filter (fn {command, state, ...} =>
    2.28 +        if Toplevel.is_ignored command then NONE else SOME (command, state));
    2.29  
    2.30  
    2.31      (* present commands *)