src/Pure/ML/ml_compiler.ML
changeset 62800 7ac100f86863
parent 62668 360d3464919c
child 62821 48c24d0b6d85
equal deleted inserted replaced
62799:46e6f91c4da1 62800:7ac100f86863
    36 
    36 
    37 
    37 
    38 (* parse trees *)
    38 (* parse trees *)
    39 
    39 
    40 fun breakpoint_position loc =
    40 fun breakpoint_position loc =
    41   let val pos = Position.reset_range (Exn_Properties.position_of_location loc) in
    41   let val pos = Position.no_range_position (Exn_Properties.position_of_location loc) in
    42     (case Position.offset_of pos of
    42     (case Position.offset_of pos of
    43       NONE => pos
    43       NONE => pos
    44     | SOME 1 => pos
    44     | SOME 1 => pos
    45     | SOME j =>
    45     | SOME j =>
    46         Position.properties_of pos
    46         Position.properties_of pos