# HG changeset patch
# User wenzelm
# Date 1606313522 -3600
# Node ID f1380c9f3806aef8c5175c6d151c1a64f5328f3f
# Parent  52d0b5fcb19d6a475a8304bf8ae396eb4a92b3a3
clarified signature;

diff -r 52d0b5fcb19d -r f1380c9f3806 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Wed Nov 25 13:51:28 2020 +0100
+++ b/src/Pure/General/position.ML	Wed Nov 25 15:12:02 2020 +0100
@@ -90,7 +90,7 @@
 
 fun norm_props (props: Properties.T) =
   maps (fn a => the_list (find_first (fn (b, _) => a = b) props))
-    Markup.position_properties';
+    [Markup.fileN, Markup.idN];
 
 fun make {line = i, offset = j, end_offset = k, props} = Pos ((i, j, k), norm_props props);
 fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props};
diff -r 52d0b5fcb19d -r f1380c9f3806 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Wed Nov 25 13:51:28 2020 +0100
+++ b/src/Pure/PIDE/markup.ML	Wed Nov 25 15:12:02 2020 +0100
@@ -59,7 +59,6 @@
   val end_offsetN: string
   val fileN: string
   val idN: string
-  val position_properties': string list
   val position_properties: string list
   val positionN: string val position: T
   val expressionN: string val expression: string -> T
@@ -380,8 +379,7 @@
 val fileN = "file";
 val idN = "id";
 
-val position_properties' = [fileN, idN];
-val position_properties = [lineN, offsetN, end_offsetN] @ position_properties';
+val position_properties = [lineN, offsetN, end_offsetN, fileN, idN];
 
 val (positionN, position) = markup_elem "position";