# HG changeset patch
# User berghofe
# Date 1108138284 -3600
# Node ID b86d5c84a9a7bd521435197da29268c50fb2f2b7
# Parent  1b12557f720d3d8b0f635fe0666c344336f3cf77
Optimized present_tokens to produce fewer newlines when hiding proofs.

diff -r 1b12557f720d -r b86d5c84a9a7 src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Fri Feb 11 10:03:41 2005 +0100
+++ b/src/Pure/Isar/isar_output.ML	Fri Feb 11 17:11:24 2005 +0100
@@ -200,15 +200,17 @@
       T.is_kind T.Command tk andalso T.val_of tk mem !hidden_commands
   | is_hidden _ = false;
 
+fun filter_newlines toks = (case mapfilter
+    (fn (tk, i) => if is_newline tk then Some tk else None) toks of
+  [] => [] | [tk] => [tk] | _ :: toks' => toks');
+
 fun present_tokens lex (flag, toks) state state' =
   Buffer.add (case flag of None => "" | Some b => Latex.flag_markup b) o
    ((if !hide_commands andalso exists (is_hidden o fst) toks then []
+     else if !hide_commands andalso is_proof state then
+       if is_proof state' then [] else filter_newlines toks
      else mapfilter (fn (tk, i) =>
-       if i > ! interest_level then None
-       else if !hide_commands andalso is_proof state then
-         if not (is_proof state') andalso is_newline tk then Some tk
-         else None
-       else Some tk) toks)
+       if i > ! interest_level then None else Some tk) toks)
     |> map (apsnd (eval_antiquote lex state'))
     |> Latex.output_tokens
     |> Buffer.add);