# HG changeset patch
# User wenzelm
# Date 1697891807 -7200
# Node ID d3328c562307f6ced82cd26704756645664bebf1
# Parent  9473dd79e9c3c3c8d592a50eca7456277d3c4c39
more compact ML source;

diff -r 9473dd79e9c3 -r d3328c562307 src/Pure/General/position.ML
--- 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;
 
diff -r 9473dd79e9c3 -r d3328c562307 src/Pure/ML/ml_syntax.ML
--- a/src/Pure/ML/ml_syntax.ML	Sat Oct 21 12:02:23 2023 +0200
+++ b/src/Pure/ML/ml_syntax.ML	Sat Oct 21 14:36:47 2023 +0200
@@ -97,7 +97,11 @@
 val print_properties = print_list (print_pair print_string print_string);
 
 fun print_position pos =
-  "Position.of_properties " ^ print_properties (Position.properties_of pos);
+  let val {line, offset, end_offset, props = {label, file, id}} = Position.dest pos in
+    space_implode " "
+      ["Position.make0", print_int line, print_int offset, print_int end_offset,
+        print_string label, print_string file, print_string id]
+  end;
 
 fun print_range range =
   "Position.range_of_properties " ^ print_properties (Position.properties_of_range range);