# HG changeset patch
# User wenzelm
# Date 1629652914 -7200
# Node ID ff3dbb2be9249836b5862ebe491b37b5f7c1b630
# Parent  86163ea20e77a2bb43560446f96e5e45ae7cacd9
tuned signature;

diff -r 86163ea20e77 -r ff3dbb2be924 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Sun Aug 22 17:52:27 2021 +0200
+++ b/src/Pure/Concurrent/future.ML	Sun Aug 22 19:21:54 2021 +0200
@@ -407,7 +407,7 @@
 
 fun error_message pos ((serial, msg), exec_id) =
   Position.setmp_thread_data pos (fn () =>
-    let val id = Position.get_id pos in
+    let val id = Position.id_of pos in
       if is_none id orelse is_none exec_id orelse id = exec_id
       then Output.error_message' (serial, msg) else ()
     end) ();
@@ -415,7 +415,7 @@
 fun identify_result pos res =
   res |> Exn.map_exn (fn exn =>
     let val exec_id =
-      (case Position.get_id pos of
+      (case Position.id_of pos of
         NONE => []
       | SOME id => [(Markup.exec_idN, id)])
     in Par_Exn.identify exec_id exn end);
diff -r 86163ea20e77 -r ff3dbb2be924 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Sun Aug 22 17:52:27 2021 +0200
+++ b/src/Pure/General/position.ML	Sun Aug 22 19:21:54 2021 +0200
@@ -16,6 +16,7 @@
   val offset_of: T -> int option
   val end_offset_of: T -> int option
   val file_of: T -> string option
+  val id_of: T -> string option
   val advance: Symbol.symbol -> T -> T
   val advance_offsets: int -> T -> T
   val distance_of: T * T -> int option
@@ -30,7 +31,6 @@
   val get_props: T -> Properties.T
   val id: string -> T
   val id_only: string -> T
-  val get_id: T -> string option
   val put_id: string -> T -> T
   val copy_id: T -> T -> T
   val id_properties_of: T -> Properties.T
@@ -94,16 +94,18 @@
 fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props};
 
 fun valid (i: int) = i > 0;
+fun maybe_valid i = if valid i then SOME i else NONE;
 fun if_valid i i' = if valid i then i' else i;
 
 
 (* fields *)
 
-fun line_of (Pos ((i, _, _), _)) = if valid i then SOME i else NONE;
-fun offset_of (Pos ((_, j, _), _)) = if valid j then SOME j else NONE;
-fun end_offset_of (Pos ((_, _, k), _)) = if valid k then SOME k else NONE;
+fun line_of (Pos ((i, _, _), _)) = maybe_valid i;
+fun offset_of (Pos ((_, j, _), _)) = maybe_valid j;
+fun end_offset_of (Pos ((_, _, k), _)) = maybe_valid k;
 
 fun file_of (Pos (_, props)) = Properties.get props Markup.fileN;
+fun id_of (Pos (_, props)) = Properties.get props Markup.idN;
 
 
 (* advance *)
@@ -154,14 +156,13 @@
 fun id id = Pos ((0, 1, 0), [(Markup.idN, id)]);
 fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
 
-fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
 fun put_id id (Pos (count, props)) = Pos (count, norm_props (Properties.put (Markup.idN, id) props));
-fun copy_id pos = (case get_id pos of NONE => I | SOME id => put_id id);
+fun copy_id pos = (case id_of pos of NONE => I | SOME id => put_id id);
 
-fun parse_id pos = Option.map Value.parse_int (get_id pos);
+fun parse_id pos = Option.map Value.parse_int (id_of pos);
 
 fun id_properties_of pos =
-  (case get_id pos of
+  (case id_of pos of
     SOME id => [(Markup.idN, id)]
   | NONE => []);
 
@@ -213,7 +214,7 @@
 
 (* reports *)
 
-fun is_reported pos = is_some (offset_of pos) andalso is_some (get_id pos);
+fun is_reported pos = is_some (offset_of pos) andalso is_some (id_of pos);
 fun is_reported_range pos = is_reported pos andalso is_some (end_offset_of pos);
 
 fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else "";
diff -r 86163ea20e77 -r ff3dbb2be924 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sun Aug 22 17:52:27 2021 +0200
+++ b/src/Pure/PIDE/command.ML	Sun Aug 22 19:21:54 2021 +0200
@@ -95,7 +95,7 @@
   let
     val file_pos =
       Position.file file_node |>
-      (case Position.get_id (Position.thread_data ()) of
+      (case Position.id_of (Position.thread_data ()) of
         NONE => I
       | SOME exec_id => Position.put_id exec_id);
   in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end
diff -r 86163ea20e77 -r ff3dbb2be924 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sun Aug 22 17:52:27 2021 +0200
+++ b/src/Pure/PIDE/document.ML	Sun Aug 22 19:21:54 2021 +0200
@@ -132,7 +132,7 @@
       if null errors then ()
       else
         cat_lines errors |>
-        (case Position.get_id (Position.thread_data ()) of
+        (case Position.id_of (Position.thread_data ()) of
           NONE => I
         | SOME id => Protocol_Message.command_positions_yxml id)
         |> error;
diff -r 86163ea20e77 -r ff3dbb2be924 src/Pure/Thy/export.ML
--- a/src/Pure/Thy/export.ML	Sun Aug 22 17:52:27 2021 +0200
+++ b/src/Pure/Thy/export.ML	Sun Aug 22 19:21:54 2021 +0200
@@ -36,7 +36,7 @@
 fun export_params ({theory = thy, binding, executable, compress, strict}: params) body =
  (report_export thy binding;
   (Output.try_protocol_message o Markup.export)
-   {id = Position.get_id (Position.thread_data ()),
+   {id = Position.id_of (Position.thread_data ()),
     serial = serial (),
     theory_name = Context.theory_long_name thy,
     name = Path.implode_binding (tap Path.proper_binding binding),