--- a/src/Tools/Haskell/Haskell.thy Tue Aug 24 15:10:37 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy Tue Aug 24 16:42:45 2021 +0200
@@ -227,7 +227,7 @@
StringLike, STRING (..), TEXT (..), BYTES (..),
show_bytes, show_text,
- proper_string, quote, space_implode, commas, commas_quote, cat_lines,
+ proper_string, enclose, quote, space_implode, commas, commas_quote, cat_lines,
space_explode, split_lines, trim_line)
where
@@ -371,8 +371,11 @@
proper_string :: StringLike a => a -> Maybe a
proper_string s = if s == "" then Nothing else Just s
+enclose :: StringLike a => a -> a -> a -> a
+enclose lpar rpar str = lpar <> str <> rpar
+
quote :: StringLike a => a -> a
-quote s = "\"" <> s <> "\""
+quote = enclose "\"" "\""
space_implode :: StringLike a => a -> [a] -> a
space_implode s = mconcat . separate s
@@ -1202,7 +1205,7 @@
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,
+ start, none, put_file, file, file_only, put_id, id, id_only,
symbol, symbol_explode, symbol_explode_string, shift_offsets,
of_properties, properties_of, def_properties_of, entity_markup, make_entity_markup,
is_reported, is_reported_range, here,
@@ -1211,6 +1214,7 @@
)
where
+import Prelude hiding (id)
import Data.Maybe (isJust, fromMaybe)
import Data.Bifunctor (first)
import qualified Isabelle.Properties as Properties
@@ -1282,6 +1286,12 @@
put_id :: Bytes -> T -> T
put_id id pos = pos { _id = id }
+id :: Bytes -> T
+id id = put_id id start
+
+id_only :: Bytes -> T
+id_only id = put_id id none
+
{- count position -}
@@ -1958,7 +1968,7 @@
import qualified Isabelle.Bytes as Bytes
import Isabelle.Bytes (Bytes)
-import Isabelle.Library hiding (quote, separate, commas)
+import Isabelle.Library hiding (enclose, quote, separate, commas)
import qualified Isabelle.Buffer as Buffer
import qualified Isabelle.Markup as Markup
import qualified Isabelle.XML as XML