avoid redundant positions;
authorwenzelm
Wed Dec 13 16:42:02 2017 +0100 (17 months ago)
changeset 671956be90977f882
parent 67194 1c0a6a957114
child 67196 eb29f4868d14
avoid redundant positions;
src/Pure/Thy/latex.ML
     1.1 --- a/src/Pure/Thy/latex.ML	Wed Dec 13 16:18:40 2017 +0100
     1.2 +++ b/src/Pure/Thy/latex.ML	Wed Dec 13 16:42:02 2017 +0100
     1.3 @@ -57,12 +57,16 @@
     1.4  fun output_positions file_pos texts =
     1.5    let
     1.6      fun position (a, b) = enclose "%:%" "%:%" (a ^ "=" ^ b);
     1.7 +    fun add_position p positions =
     1.8 +      let val s = position (apply2 Value.print_int p)
     1.9 +      in positions |> s <> hd positions ? cons s end;
    1.10 +
    1.11      fun output (Text (s, pos)) (positions, line) =
    1.12            let
    1.13              val positions' =
    1.14                (case Position.line_of pos of
    1.15                  NONE => positions
    1.16 -              | SOME l => position (apply2 Value.print_int (line, l)) :: positions);
    1.17 +              | SOME l => add_position (line, l) positions);
    1.18              val line' = fold_string (fn c => fn n => if c = "\n" then n + 1 else n) s line;
    1.19            in (positions', line') end
    1.20        | output (Block body) res = fold output body res;