src/Pure/General/position.ML
changeset 42818 128cc195ced3
parent 42327 7c7cc7590eb3
child 43710 7270ae921cf2
equal deleted inserted replaced
42817:7e819eb7dabb 42818:128cc195ced3
   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;