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)