src/Pure/General/position.ML
changeset 26633 ff317b19e24e
parent 26052 7d5b3e34a735
child 26882 9e824d8f4512
equal deleted inserted replaced
26632:90c0b075c0d3 26633:ff317b19e24e
    44 fun line m = Pos (SOME (m, 1), []);
    44 fun line m = Pos (SOME (m, 1), []);
    45 fun file name = Pos (SOME (1, 1), [(Markup.fileN, name)]);
    45 fun file name = Pos (SOME (1, 1), [(Markup.fileN, name)]);
    46 val path = file o Path.implode o Path.expand;
    46 val path = file o Path.implode o Path.expand;
    47 
    47 
    48 fun advance "\n" (Pos (SOME (m, _), props)) = Pos (SOME (m + 1, 1), props)
    48 fun advance "\n" (Pos (SOME (m, _), props)) = Pos (SOME (m + 1, 1), props)
    49   | advance sym (pos as Pos (SOME (m, n), props)) =
    49   | advance s (pos as Pos (SOME (m, n), props)) =
    50       if Symbol.is_regular sym then Pos (SOME (m, n + 1), props) else pos
    50       if Symbol.is_regular s andalso not (Symbol.is_utf8_trailer s)
       
    51       then Pos (SOME (m, n + 1), props) else pos
    51   | advance _ pos = pos;
    52   | advance _ pos = pos;
    52 
    53 
    53 
    54 
    54 (* markup properties *)
    55 (* markup properties *)
    55 
    56