equal
deleted
inserted
replaced
175 val props = properties_of pos; |
175 val props = properties_of pos; |
176 val s = |
176 val s = |
177 (case (line_of pos, file_of pos) of |
177 (case (line_of pos, file_of pos) of |
178 (SOME i, NONE) => "(line " ^ string_of_int i ^ ")" |
178 (SOME i, NONE) => "(line " ^ string_of_int i ^ ")" |
179 | (SOME i, SOME name) => "(line " ^ string_of_int i ^ " of " ^ quote name ^ ")" |
179 | (SOME i, SOME name) => "(line " ^ string_of_int i ^ " of " ^ quote name ^ ")" |
|
180 | (NONE, SOME name) => "(" ^ quote name ^ ")" |
180 | _ => ""); |
181 | _ => ""); |
181 in |
182 in |
182 if null props then "" |
183 if null props then "" |
183 else (if s = "" then "" else " ") ^ Markup.markup (Markup.properties props Markup.position) s |
184 else (if s = "" then "" else " ") ^ Markup.markup (Markup.properties props Markup.position) s |
184 end; |
185 end; |