# HG changeset patch
# User wenzelm
# Date 1680377634 -7200
# Node ID 99a18dcff0109d1c7abdc26ebb77b5547f2db9ee
# Parent  13cee8c2ed8dc8bcdb9346ad559a085b6eed8ccc
clarified modules;

diff -r 13cee8c2ed8d -r 99a18dcff010 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Sat Apr 01 21:25:24 2023 +0200
+++ b/src/Pure/General/position.ML	Sat Apr 01 21:33:54 2023 +0200
@@ -31,7 +31,6 @@
   val id_only: string -> T
   val put_id: string -> T -> T
   val copy_id: T -> T -> T
-  val id_properties_of: T -> Properties.T
   val parse_id: T -> int option
   val shift_offsets: {remove_id: bool} -> int -> T -> T
   val adjust_offsets: (int -> int option) -> T -> T
@@ -165,11 +164,6 @@
 
 fun parse_id pos = Option.map Value.parse_int (id_of pos);
 
-fun id_properties_of pos =
-  (case id_of pos of
-    SOME id => [(Markup.idN, id)]
-  | NONE => []);
-
 
 (* adjust offsets *)
 
diff -r 13cee8c2ed8d -r 99a18dcff010 src/Pure/PIDE/active.ML
--- a/src/Pure/PIDE/active.ML	Sat Apr 01 21:25:24 2023 +0200
+++ b/src/Pure/PIDE/active.ML	Sat Apr 01 21:33:54 2023 +0200
@@ -21,7 +21,10 @@
 
 (* active markup *)
 
-fun explicit_id () = Position.id_properties_of (Position.thread_data ());
+fun explicit_id () =
+  (case Position.id_of (Position.thread_data ()) of
+    SOME id => [(Markup.idN, id)]
+  | NONE => []);
 
 fun make_markup name {implicit, properties} =
   (name, [])