# HG changeset patch # User wenzelm # Date 1629810637 -7200 # Node ID 7652f8d29d105aed39b8d8e98b65ca7f839d5dc3 # Parent af81e4a307be6b8b239d457ac58bbe8eabf47070 clarified signature; diff -r af81e4a307be -r 7652f8d29d10 src/Tools/Haskell/Haskell.thy --- a/src/Tools/Haskell/Haskell.thy Tue Aug 24 14:56:55 2021 +0200 +++ b/src/Tools/Haskell/Haskell.thy Tue Aug 24 15:10:37 2021 +0200 @@ -1198,18 +1198,18 @@ See \<^file>\$ISABELLE_HOME/src/Pure/General/position.ML\. -} - {-# LANGUAGE OverloadedStrings #-} module Isabelle.Position ( T, line_of, column_of, offset_of, end_offset_of, file_of, id_of, start, none, put_file, file, file_only, put_id, symbol, symbol_explode, symbol_explode_string, shift_offsets, - of_properties, properties_of, def_properties_of, entity_markup, entity_properties_of, + of_properties, properties_of, def_properties_of, entity_markup, make_entity_markup, is_reported, is_reported_range, here, Range, no_range, no_range_position, range_position, range -) where +) +where import Data.Maybe (isJust, fromMaybe) import Data.Bifunctor (first) @@ -1359,10 +1359,13 @@ entity_markup kind (name, pos) = Markup.entity kind name |> Markup.properties (def_properties_of pos) -entity_properties_of :: Bool -> Int -> T -> Properties.T -entity_properties_of def serial pos = - if def then (Markup.defN, Value.print_int serial) : properties_of pos - else (Markup.refN, Value.print_int serial) : def_properties_of pos +make_entity_markup :: Bool -> Int -> Bytes -> (Bytes, T) -> Markup.T +make_entity_markup def serial kind (name, pos) = + let + props = + if def then (Markup.defN, Value.print_int serial) : properties_of pos + else (Markup.refN, Value.print_int serial) : def_properties_of pos + in Markup.entity kind name |> Markup.properties props {- reports -}