clarified modules;
authorwenzelm
Sat, 01 Apr 2023 21:33:54 +0200
changeset 77778 99a18dcff010
parent 77777 13cee8c2ed8d
child 77779 1f990c8bb74c
clarified modules;
src/Pure/General/position.ML
src/Pure/PIDE/active.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 *)
 
--- 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, [])