src/Pure/General/position.ML
changeset 70498 de75eea6ffc8
parent 69348 f0aef5e337a2
child 71465 910a081cca74
equal deleted inserted replaced
70497:8a19b92ec3d6 70498:de75eea6ffc8
   240   in
   240   in
   241     if s2 = "" 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 = map here #> distinct (op =) #> implode;
   246 
   246 
   247 
   247 
   248 (* range *)
   248 (* range *)
   249 
   249 
   250 type range = T * T;
   250 type range = T * T;