--- a/src/Pure/General/position.ML Sat Oct 21 12:02:23 2023 +0200
+++ b/src/Pure/General/position.ML Sat Oct 21 14:36:47 2023 +0200
@@ -10,6 +10,7 @@
sig
eqtype T
val ord: T ord
+ val make0: int -> int -> int -> string -> string -> string -> T
val make: Thread_Position.T -> T
val dest: T -> Thread_Position.T
val line_of: T -> int option
@@ -78,6 +79,10 @@
datatype T = Pos of Thread_Position.T;
+fun make0 line offset end_offset label file id =
+ Pos {line = line, offset = offset, end_offset = end_offset,
+ props = {label = label, file = file, id = id}};
+
val make = Pos;
fun dest (Pos args) = args;