# HG changeset patch
# User wenzelm
# Date 1683743446 -7200
# Node ID ce6e3bc34343736df41ba360347c626bfe079dd0
# Parent  1a829342a2d3816f20a4a1048594ccfeceb309d2
more informative position information;

diff -r 1a829342a2d3 -r ce6e3bc34343 src/Pure/Concurrent/thread_position.ML
--- a/src/Pure/Concurrent/thread_position.ML	Wed May 10 19:30:17 2023 +0200
+++ b/src/Pure/Concurrent/thread_position.ML	Wed May 10 20:30:46 2023 +0200
@@ -6,7 +6,7 @@
 
 signature THREAD_POSITION =
 sig
-  type T = {line: int, offset: int, end_offset: int, props: {file: string, id: string}}
+  type T = {line: int, offset: int, end_offset: int, props: {label: string, file: string, id: string}}
   val none: T
   val get: unit -> T
   val setmp: T -> ('a -> 'b) -> 'a -> 'b
@@ -15,11 +15,11 @@
 structure Thread_Position: THREAD_POSITION =
 struct
 
-type T = {line: int, offset: int, end_offset: int, props: {file: string, id: string}};
+type T = {line: int, offset: int, end_offset: int, props: {label: string, file: string, id: string}};
 
 val var = Thread_Data.var () : T Thread_Data.var;
 
-val none: T = {line = 0, offset = 0, end_offset = 0, props = {file = "", id = ""}};
+val none: T = {line = 0, offset = 0, end_offset = 0, props = {label = "", file = "", id = ""}};
 
 fun get () = (case Thread_Data.get var of NONE => none | SOME pos => pos);
 fun setmp pos f x = Thread_Data.setmp var (if pos = none then NONE else SOME pos) f x;
diff -r 1a829342a2d3 -r ce6e3bc34343 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Wed May 10 19:30:17 2023 +0200
+++ b/src/Pure/General/position.ML	Wed May 10 20:30:46 2023 +0200
@@ -15,6 +15,7 @@
   val line_of: T -> int option
   val offset_of: T -> int option
   val end_offset_of: T -> int option
+  val label_of: T -> string option
   val file_of: T -> string option
   val id_of: T -> string option
   val symbol: Symbol.symbol -> T -> T
@@ -22,6 +23,7 @@
   val distance_of: T * T -> int option
   val none: T
   val start: T
+  val label: string -> T -> T
   val file_only: string -> T
   val file: string -> T
   val line_file_only: int -> string -> T
@@ -83,6 +85,7 @@
    (int_ord o apply2 (#line o dest) |||
     int_ord o apply2 (#offset o dest) |||
     int_ord o apply2 (#end_offset o dest) |||
+    fast_string_ord o apply2 (#label o #props o dest) |||
     fast_string_ord o apply2 (#file o #props o dest) |||
     fast_string_ord o apply2 (#id o #props o dest));
 
@@ -99,6 +102,7 @@
 val offset_of = maybe_valid o #offset o dest;
 val end_offset_of = maybe_valid o #end_offset o dest;
 
+fun label_of (Pos {props = {label, ...}, ...}) = if label = "" then NONE else SOME label;
 fun file_of (Pos {props = {file, ...}, ...}) = if file = "" then NONE else SOME file;
 fun id_of (Pos {props = {id, ...}, ...}) = if id = "" then NONE else SOME id;
 
@@ -131,20 +135,23 @@
 
 (* make position *)
 
-type props = {file: string, id: string};
+type props = {label: string, file: string, id: string};
 
-val no_props: props = {file = "", id = ""};
+val no_props: props = {label = "", file = "", id = ""};
 
 fun file_props name : props =
-  if name = "" then no_props else {file = name, id = ""};
+  if name = "" then no_props else {label = "", file = name, id = ""};
 
 fun id_props id : props =
-  if id = "" then no_props else {file = "", id = id};
+  if id = "" then no_props else {label = "", file = "", id = id};
 
 
 val none = Pos {line = 0, offset = 0, end_offset = 0, props = no_props};
 val start = Pos {line = 1, offset = 1, end_offset = 0, props = no_props};
 
+fun label label (Pos {line, offset, end_offset, props = {label = _, file, id}}) =
+  Pos {line = line, offset = offset, end_offset = end_offset,
+    props = {label = label, file = file, id = id}};
 
 fun file_only name = Pos {line = 0, offset = 0, end_offset = 0, props = file_props name};
 fun file name = Pos {line = 1, offset = 1, end_offset = 0, props = file_props name};
@@ -156,9 +163,10 @@
 fun id id = Pos {line = 0, offset = 1, end_offset = 0, props = id_props id};
 fun id_only id = Pos {line = 0, offset = 0, end_offset = 0, props = id_props id};
 
-fun put_id id' (pos as Pos {line, offset, end_offset, props = {file, id}}) =
+fun put_id id' (pos as Pos {line, offset, end_offset, props = {label, file, id}}) =
   if id = id' then pos
-  else Pos {line = line, offset = offset, end_offset = end_offset, props = {file = file, id = id'}};
+  else Pos {line = line, offset = offset, end_offset = end_offset,
+    props = {label = label, file = file, id = id'}};
 
 fun copy_id pos = (case id_of pos of NONE => I | SOME id => put_id id);
 
@@ -196,7 +204,8 @@
 fun of_props {line, offset, end_offset, props} =
   Pos {line = line, offset = offset, end_offset = end_offset,
     props =
-     {file = Properties.get_string props Markup.fileN,
+     {label = Properties.get_string props Markup.labelN,
+      file = Properties.get_string props Markup.fileN,
       id = Properties.get_string props Markup.idN}};
 
 fun of_properties props =
@@ -206,10 +215,11 @@
     end_offset = Properties.get_int props Markup.end_offsetN,
     props = props};
 
-fun properties_of (Pos {line, offset, end_offset, props = {file, id}}) =
+fun properties_of (Pos {line, offset, end_offset, props = {label, file, id}}) =
   Properties.make_int Markup.lineN line @
   Properties.make_int Markup.offsetN offset @
   Properties.make_int Markup.end_offsetN end_offset @
+  Properties.make_string Markup.labelN label @
   Properties.make_string Markup.fileN file @
   Properties.make_string Markup.idN id;
 
diff -r 1a829342a2d3 -r ce6e3bc34343 src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Wed May 10 19:30:17 2023 +0200
+++ b/src/Pure/General/position.scala	Wed May 10 20:30:46 2023 +0200
@@ -15,6 +15,7 @@
   val Line = new Properties.Int(Markup.LINE)
   val Offset = new Properties.Int(Markup.OFFSET)
   val End_Offset = new Properties.Int(Markup.END_OFFSET)
+  val Label = new Properties.String(Markup.LABEL)
   val File = new Properties.String(Markup.FILE)
   val Id = new Properties.Long(Markup.ID)
   val Id_String = new Properties.String(Markup.ID)
@@ -22,6 +23,7 @@
   val Def_Line = new Properties.Int(Markup.DEF_LINE)
   val Def_Offset = new Properties.Int(Markup.DEF_OFFSET)
   val Def_End_Offset = new Properties.Int(Markup.DEF_END_OFFSET)
+  val Def_Label = new Properties.String(Markup.DEF_LABEL)
   val Def_File = new Properties.String(Markup.DEF_FILE)
   val Def_Id = new Properties.Long(Markup.DEF_ID)
 
diff -r 1a829342a2d3 -r ce6e3bc34343 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed May 10 19:30:17 2023 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed May 10 20:30:46 2023 +0200
@@ -610,8 +610,8 @@
   let val put_id = Position.put_id (Document_ID.print id)
   in position (put_id pos) tr end;
 
-fun setmp_thread_position (Transition {pos, ...}) f x =
-  Position.setmp_thread_data pos f x;
+fun setmp_thread_position (Transition {pos, name, ...}) f x =
+  Position.setmp_thread_data (Position.label (Long_Name.qualify Markup.commandN name) pos) f x;
 
 
 (* apply transitions *)
diff -r 1a829342a2d3 -r ce6e3bc34343 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Wed May 10 19:30:17 2023 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Wed May 10 20:30:46 2023 +0200
@@ -166,7 +166,8 @@
     (* input *)
 
     val position_props =
-      filter (fn (a, _) => a = Markup.idN orelse a = Markup.fileN) (Position.properties_of pos);
+      filter (fn (a, _) => a = Markup.labelN orelse a = Markup.fileN orelse a = Markup.idN)
+        (Position.properties_of pos);
     val location_props = op ^ (YXML.output_markup (":", position_props));
 
     val {explode_token, ...} = ML_Env.operations opt_context (#environment flags);
diff -r 1a829342a2d3 -r ce6e3bc34343 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Wed May 10 19:30:17 2023 +0200
+++ b/src/Pure/PIDE/markup.ML	Wed May 10 20:30:46 2023 +0200
@@ -58,6 +58,7 @@
   val end_lineN: string
   val offsetN: string
   val end_offsetN: string
+  val labelN: string
   val fileN: string
   val idN: string
   val positionN: string val position: T
@@ -408,12 +409,13 @@
 val offsetN = "offset";
 val end_offsetN = "end_offset";
 
+val labelN = "label";
 val fileN = "file";
 val idN = "id";
 
 val (positionN, position) = markup_elem "position";
 
-val position_properties = [lineN, offsetN, end_offsetN, fileN, idN];
+val position_properties = [lineN, offsetN, end_offsetN, labelN, fileN, idN];
 fun position_property (entry: Properties.entry) = member (op =) position_properties (#1 entry);
 
 
diff -r 1a829342a2d3 -r ce6e3bc34343 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Wed May 10 19:30:17 2023 +0200
+++ b/src/Pure/PIDE/markup.scala	Wed May 10 20:30:46 2023 +0200
@@ -137,18 +137,20 @@
   val END_LINE = "line"
   val OFFSET = "offset"
   val END_OFFSET = "end_offset"
+  val LABEL = "label"
   val FILE = "file"
   val ID = "id"
 
   val DEF_LINE = "def_line"
   val DEF_OFFSET = "def_offset"
   val DEF_END_OFFSET = "def_end_offset"
+  val DEF_LABEL = "def_label"
   val DEF_FILE = "def_file"
   val DEF_ID = "def_id"
 
   val POSITION = "position"
 
-  val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
+  val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, LABEL, FILE, ID)
   def position_property(entry: Properties.Entry): Boolean = POSITION_PROPERTIES(entry._1)
 
 
@@ -156,7 +158,7 @@
 
   private val def_names: Map[String, String] =
     Map(LINE -> DEF_LINE, OFFSET -> DEF_OFFSET, END_OFFSET -> DEF_END_OFFSET,
-      FILE -> DEF_FILE, ID -> DEF_ID)
+      LABEL -> DEF_LABEL, FILE -> DEF_FILE, ID -> DEF_ID)
 
   def def_name(a: String): String = def_names.getOrElse(a, a + "def_")
 
diff -r 1a829342a2d3 -r ce6e3bc34343 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed May 10 19:30:17 2023 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed May 10 20:30:46 2023 +0200
@@ -44,7 +44,7 @@
     val props' = Position.properties_of (#adjust_pos context pos);
   in
     filter (fn (a, _) => a = Markup.offsetN orelse a = Markup.end_offsetN) props' @
-    filter (fn (a, _) => a = Markup.idN orelse a = Markup.fileN) props
+    filter (fn (a, _) => a = Markup.labelN orelse a = Markup.fileN orelse a = Markup.idN) props
   end;
 
 structure Presentation = Theory_Data
diff -r 1a829342a2d3 -r ce6e3bc34343 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Wed May 10 19:30:17 2023 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Wed May 10 20:30:46 2023 +0200
@@ -732,7 +732,7 @@
 
   completionN, completion, no_completionN, no_completion,
 
-  lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position,
+  lineN, end_lineN, offsetN, end_offsetN, labelN, fileN, idN, positionN, position,
   position_properties, def_name,
 
   expressionN, expression,
@@ -866,7 +866,8 @@
 offsetN = \<open>Markup.offsetN\<close>
 end_offsetN = \<open>Markup.end_offsetN\<close>
 
-fileN, idN :: Bytes
+labelN, fileN, idN :: Bytes
+labelN = \<open>Markup.labelN\<close>
 fileN = \<open>Markup.fileN\<close>
 idN = \<open>Markup.idN\<close>
 
@@ -876,7 +877,7 @@
 position = markup_elem positionN
 
 position_properties :: [Bytes]
-position_properties = [lineN, offsetN, end_offsetN, fileN, idN]
+position_properties = [lineN, offsetN, end_offsetN, labelN, fileN, idN]
 
 
 {- position "def" names -}
@@ -1283,6 +1284,7 @@
     _column :: Int,
     _offset :: Int,
     _end_offset :: Int,
+    _label :: Bytes,
     _file :: Bytes,
     _id :: Bytes }
   deriving (Eq, Ord)
@@ -1306,6 +1308,9 @@
 offset_of = maybe_valid . _offset
 end_offset_of = maybe_valid . _end_offset
 
+label_of :: T -> Maybe Bytes
+label_of = proper_string . _label
+
 file_of :: T -> Maybe Bytes
 file_of = proper_string . _file
 
@@ -1316,10 +1321,13 @@
 {- make position -}
 
 start :: T
-start = Position 1 1 1 0 Bytes.empty Bytes.empty
+start = Position 1 1 1 0 Bytes.empty Bytes.empty Bytes.empty
 
 none :: T
-none = Position 0 0 0 0 Bytes.empty Bytes.empty
+none = Position 0 0 0 0 Bytes.empty Bytes.empty Bytes.empty
+
+label :: Bytes -> T -> T
+label label pos = pos { _label = label }
 
 put_file :: Bytes -> T -> T
 put_file file pos = pos { _file = file }
@@ -1392,6 +1400,7 @@
     _line = get_int props Markup.lineN,
     _offset = get_int props Markup.offsetN,
     _end_offset = get_int props Markup.end_offsetN,
+    _label = get_string props Markup.labelN,
     _file = get_string props Markup.fileN,
     _id = get_string props Markup.idN }
 
@@ -1406,6 +1415,7 @@
   int_entry Markup.lineN (_line pos) ++
   int_entry Markup.offsetN (_offset pos) ++
   int_entry Markup.end_offsetN (_end_offset pos) ++
+  string_entry Markup.labelN (_label pos) ++
   string_entry Markup.fileN (_file pos) ++
   string_entry Markup.idN (_id pos)