# HG changeset patch
# User wenzelm
# Date 1526286165 -7200
# Node ID e3dd94d04eeea832ddd953f72dc4bbf7c0252676
# Parent  6e40f5d4393672854da4b284760f36b91c3ee121
more explicit type Thy_Output.segment;

diff -r 6e40f5d43936 -r e3dd94d04eee src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon May 14 09:39:27 2018 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon May 14 10:22:45 2018 +0200
@@ -267,8 +267,7 @@
       fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
         (Keyword.add_keywords (#keywords header) Keyword.empty_keywords);
 
-    val toks = Token.explode keywords text_pos text;
-    val spans = Outer_Syntax.parse_spans toks;
+    val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text);
     val elements = Thy_Syntax.parse_elements keywords spans;
 
     fun init () =
@@ -282,15 +281,15 @@
 
     fun present () =
       let
-        val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
+        val segments = (spans ~~ maps Toplevel.join_results results)
+          |> map (fn (span, (tr, st')) => {span = span, tr = tr, result_state = st'});
         val _ = apply_presentation thy;
       in
-        if exists (Toplevel.is_skipped_proof o #2) res then ()
+        if exists (Toplevel.is_skipped_proof o #result_state) segments then ()
         else
-          let val body = Thy_Output.present_thy thy res toks;
+          let val body = Thy_Output.present_thy thy segments;
           in if document then Present.theory_output text_pos thy body else () end
       end;
-
   in (thy, present, size text) end;
 
 
diff -r 6e40f5d43936 -r e3dd94d04eee src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon May 14 09:39:27 2018 +0200
+++ b/src/Pure/Thy/thy_output.ML	Mon May 14 10:22:45 2018 +0200
@@ -10,8 +10,8 @@
   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
-  val present_thy: theory -> (Toplevel.transition * Toplevel.state) list ->
-    Token.T list -> Latex.text list
+  type segment = {span: Command_Span.span, tr: Toplevel.transition, result_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
@@ -338,7 +338,9 @@
 
 in
 
-fun present_thy thy command_results toks =
+type segment = {span: Command_Span.span, tr: Toplevel.transition, result_state: Toplevel.state};
+
+fun present_thy thy (segments: segment list) =
   let
     val keywords = Thy_Header.get_keywords thy;
 
@@ -404,13 +406,18 @@
       >> (fn (((toks1, (cmd, tok2)), toks3), tok4) =>
           make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4))));
 
-    val spans = toks
+    val spans = segments
+      |> maps (Command_Span.content o #span)
       |> drop_suffix Token.is_space
       |> Source.of_list
       |> 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));
+
 
     (* present commands *)
 
@@ -421,11 +428,11 @@
         (present_span thy keywords document_tags span st st');
 
     fun present _ [] = I
-      | present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest;
+      | present st ((span, (tr, st')) :: rest) = present_command tr span st st' #> present st' rest;
   in
     if length command_results = length spans then
       ((NONE, []), NONE, true, [], (I, I))
-      |> present Toplevel.toplevel (command_results ~~ spans)
+      |> present Toplevel.toplevel (spans ~~ command_results)
       |> present_trailer
       |> rev
     else error "Messed-up outer syntax for presentation"