# HG changeset patch
# User wenzelm
# Date 1513179722 -3600
# Node ID 6be90977f882bed12f9e0ed4cb50afc78cec4e56
# Parent  1c0a6a95711401f35a4e9657196fbecf1d50dc29
avoid redundant positions;

diff -r 1c0a6a957114 -r 6be90977f882 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Wed Dec 13 16:18:40 2017 +0100
+++ b/src/Pure/Thy/latex.ML	Wed Dec 13 16:42:02 2017 +0100
@@ -57,12 +57,16 @@
 fun output_positions file_pos texts =
   let
     fun position (a, b) = enclose "%:%" "%:%" (a ^ "=" ^ b);
+    fun add_position p positions =
+      let val s = position (apply2 Value.print_int p)
+      in positions |> s <> hd positions ? cons s end;
+
     fun output (Text (s, pos)) (positions, line) =
           let
             val positions' =
               (case Position.line_of pos of
                 NONE => positions
-              | SOME l => position (apply2 Value.print_int (line, l)) :: positions);
+              | SOME l => add_position (line, l) positions);
             val line' = fold_string (fn c => fn n => if c = "\n" then n + 1 else n) s line;
           in (positions', line') end
       | output (Block body) res = fold output body res;