src/Pure/General/position.ML
changeset 69348 f0aef5e337a2
parent 68858 e1796b8ddbae
child 70498 de75eea6ffc8
equal deleted inserted replaced
69347:54b95d2ec040 69348:f0aef5e337a2
   236         (SOME i, NONE) => (" ", "(line " ^ Value.print_int i ^ ")")
   236         (SOME i, NONE) => (" ", "(line " ^ Value.print_int i ^ ")")
   237       | (SOME i, SOME name) => (" ", "(line " ^ Value.print_int i ^ " of " ^ quote name ^ ")")
   237       | (SOME i, SOME name) => (" ", "(line " ^ Value.print_int i ^ " of " ^ quote name ^ ")")
   238       | (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")")
   238       | (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")")
   239       | _ => if is_reported pos then ("", "\092<^here>") else ("", ""));
   239       | _ => if is_reported pos then ("", "\092<^here>") else ("", ""));
   240   in
   240   in
   241     if null props then ""
   241     if s2 = "" then ""
   242     else s1 ^ Markup.markup (Markup.properties props Markup.position) s2
   242     else s1 ^ Markup.markup (Markup.properties props Markup.position) s2
   243   end;
   243   end;
   244 
   244 
   245 val here_list = implode o map here;
   245 val here_list = implode o map here;
   246 
   246