more explicit type Thy_Output.segment;
authorwenzelm
Mon May 14 10:22:45 2018 +0200 (12 months ago)
changeset 68178e3dd94d04eee
parent 68177 6e40f5d43936
child 68179 da70c9e91135
more explicit type Thy_Output.segment;
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Thy/thy_info.ML	Mon May 14 09:39:27 2018 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Mon May 14 10:22:45 2018 +0200
     1.3 @@ -267,8 +267,7 @@
     1.4        fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
     1.5          (Keyword.add_keywords (#keywords header) Keyword.empty_keywords);
     1.6  
     1.7 -    val toks = Token.explode keywords text_pos text;
     1.8 -    val spans = Outer_Syntax.parse_spans toks;
     1.9 +    val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text);
    1.10      val elements = Thy_Syntax.parse_elements keywords spans;
    1.11  
    1.12      fun init () =
    1.13 @@ -282,15 +281,15 @@
    1.14  
    1.15      fun present () =
    1.16        let
    1.17 -        val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
    1.18 +        val segments = (spans ~~ maps Toplevel.join_results results)
    1.19 +          |> map (fn (span, (tr, st')) => {span = span, tr = tr, result_state = st'});
    1.20          val _ = apply_presentation thy;
    1.21        in
    1.22 -        if exists (Toplevel.is_skipped_proof o #2) res then ()
    1.23 +        if exists (Toplevel.is_skipped_proof o #result_state) segments then ()
    1.24          else
    1.25 -          let val body = Thy_Output.present_thy thy res toks;
    1.26 +          let val body = Thy_Output.present_thy thy segments;
    1.27            in if document then Present.theory_output text_pos thy body else () end
    1.28        end;
    1.29 -
    1.30    in (thy, present, size text) end;
    1.31  
    1.32  
     2.1 --- a/src/Pure/Thy/thy_output.ML	Mon May 14 09:39:27 2018 +0200
     2.2 +++ b/src/Pure/Thy/thy_output.ML	Mon May 14 10:22:45 2018 +0200
     2.3 @@ -10,8 +10,8 @@
     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 -  val present_thy: theory -> (Toplevel.transition * Toplevel.state) list ->
     2.8 -    Token.T list -> Latex.text list
     2.9 +  type segment = {span: Command_Span.span, tr: Toplevel.transition, result_state: Toplevel.state}
    2.10 +  val present_thy: theory -> segment list -> Latex.text list
    2.11    val pretty_term: Proof.context -> term -> Pretty.T
    2.12    val pretty_thm: Proof.context -> thm -> Pretty.T
    2.13    val lines: Latex.text list -> Latex.text list
    2.14 @@ -338,7 +338,9 @@
    2.15  
    2.16  in
    2.17  
    2.18 -fun present_thy thy command_results toks =
    2.19 +type segment = {span: Command_Span.span, tr: Toplevel.transition, result_state: Toplevel.state};
    2.20 +
    2.21 +fun present_thy thy (segments: segment list) =
    2.22    let
    2.23      val keywords = Thy_Header.get_keywords thy;
    2.24  
    2.25 @@ -404,13 +406,18 @@
    2.26        >> (fn (((toks1, (cmd, tok2)), toks3), tok4) =>
    2.27            make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4))));
    2.28  
    2.29 -    val spans = toks
    2.30 +    val spans = segments
    2.31 +      |> maps (Command_Span.content o #span)
    2.32        |> drop_suffix Token.is_space
    2.33        |> Source.of_list
    2.34        |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk tokens >> flat))
    2.35        |> Source.source stopper (Scan.error (Scan.bulk span))
    2.36        |> Source.exhaust;
    2.37  
    2.38 +    val command_results =
    2.39 +      segments |> map_filter (fn {tr, result_state, ...} =>
    2.40 +        if Toplevel.is_ignored tr then NONE else SOME (tr, result_state));
    2.41 +
    2.42  
    2.43      (* present commands *)
    2.44  
    2.45 @@ -421,11 +428,11 @@
    2.46          (present_span thy keywords document_tags span st st');
    2.47  
    2.48      fun present _ [] = I
    2.49 -      | present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest;
    2.50 +      | present st ((span, (tr, st')) :: rest) = present_command tr span st st' #> present st' rest;
    2.51    in
    2.52      if length command_results = length spans then
    2.53        ((NONE, []), NONE, true, [], (I, I))
    2.54 -      |> present Toplevel.toplevel (command_results ~~ spans)
    2.55 +      |> present Toplevel.toplevel (spans ~~ command_results)
    2.56        |> present_trailer
    2.57        |> rev
    2.58      else error "Messed-up outer syntax for presentation"