# HG changeset patch
# User wenzelm
# Date 1535449211 -7200
# Node ID 1a4fa494a4a8b07a2b091920f9f7fdfdc81a0d97
# Parent  7030922e91a11f19f85c19d0cbaf1830ca9f642f
tuned signature;

diff -r 7030922e91a1 -r 1a4fa494a4a8 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Tue Aug 28 11:28:38 2018 +0200
+++ b/src/Pure/General/position.ML	Tue Aug 28 11:40:11 2018 +0200
@@ -29,6 +29,7 @@
   val id_only: string -> T
   val get_id: T -> string option
   val put_id: string -> T -> T
+  val id_properties_of: T -> Properties.T
   val parse_id: T -> int option
   val adjust_offsets: (int -> int option) -> T -> T
   val of_properties: Properties.T -> T
@@ -144,6 +145,10 @@
 
 fun parse_id pos = Option.map Value.parse_int (get_id pos);
 
+fun id_properties_of pos =
+  (case get_id pos of
+    SOME id => [(Markup.idN, id)]
+  | NONE => []);
 
 fun adjust_offsets adjust (pos as Pos (_, props)) =
   (case parse_id pos of
diff -r 7030922e91a1 -r 1a4fa494a4a8 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, [])