src/Tools/Haskell/Haskell.thy

 
   bindingN, binding, entityN, entity, defN, refN,
 
   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,
 
   pathN, path, urlN, url, docN, doc,

 
 offsetN, end_offsetN :: Bytes
 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>
 
 positionN :: Bytes
 positionN = \<open>Markup.positionN\<close>
 position :: T
 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 -}
 
 make_def :: Bytes -> Bytes

   Position {
     _line :: Int,
     _column :: Int,
     _offset :: Int,
     _end_offset :: Int,
+    _label :: Bytes,
     _file :: Bytes,
     _id :: Bytes }
   deriving (Eq, Ord)
 
 valid, invalid :: Int -> Bool

 line_of = maybe_valid . _line
 column_of = maybe_valid . _column
 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
 
 id_of :: T -> Maybe Bytes
 id_of = proper_string . _id
 
 
 {- 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 }
 
 file :: Bytes -> T

 of_properties props =
   none {
     _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 }
 
 string_entry :: Bytes -> Bytes -> Properties.T
 string_entry k s = if Bytes.null s then [] else [(k, s)]

 properties_of :: T -> Properties.T
 properties_of pos =
   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)
 
 def_properties_of :: T -> Properties.T
 def_properties_of = properties_of #> map (first Markup.def_name)