# HG changeset patch
# User wenzelm
# Date 1629816165 -7200
# Node ID 2508ea6a9a11077435ac4b508ad0b034b0511513
# Parent  7652f8d29d105aed39b8d8e98b65ca7f839d5dc3
more Isabelle/Haskell operations;

diff -r 7652f8d29d10 -r 2508ea6a9a11 src/Tools/Haskell/Haskell.thy
--- 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