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 = \Markup.offsetN\ end_offsetN = \Markup.end_offsetN\ -fileN, idN :: Bytes +labelN, fileN, idN :: Bytes +labelN = \Markup.labelN\ fileN = \Markup.fileN\ idN = \Markup.idN\ @@ -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)