src/Pure/PIDE/active.ML

--- a/src/Pure/PIDE/active.ML	Tue Aug 28 11:28:38 2018 +0200
+++ b/src/Pure/PIDE/active.ML	Tue Aug 28 11:40:11 2018 +0200
@@ -21,10 +21,7 @@
 
 (* active markup *)
 
-fun explicit_id () =
-  (case Position.get_id (Position.thread_data ()) of
-    SOME id => [(Markup.idN, id)]
-  | NONE => []);
+fun explicit_id () = Position.id_properties_of (Position.thread_data ());
 
 fun make_markup name {implicit, properties} =
   (name, [])