# HG changeset patch
# User wenzelm
# Date 1629744274 -7200
# Node ID a8b032dede5c6eec4b5604c90a5b32aab8f750b6
# Parent  b707145300458b9f36c44271961f594540afc9e4
treat Symbol.eof as in ML (but: presently unused);

diff -r b70714530045 -r a8b032dede5c src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Mon Aug 23 20:40:22 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Mon Aug 23 20:44:34 2021 +0200
@@ -402,11 +402,13 @@
 {-# LANGUAGE OverloadedStrings #-}
 
 module Isabelle.Symbol (
+  Symbol, eof, is_eof, not_eof,
+
   is_ascii_letter, is_ascii_digit, is_ascii_hex, is_ascii_quasi,
   is_ascii_blank, is_ascii_line_terminator, is_ascii_letdig,
   is_ascii_identifier,
 
-  Symbol, explode
+  explode
 )
 where
 
@@ -415,6 +417,18 @@
 import Isabelle.Bytes (Bytes)
 
 
+{- type -}
+
+type Symbol = Bytes
+
+eof :: Symbol
+eof = ""
+
+is_eof, not_eof :: Symbol -> Bool
+is_eof = Bytes.null
+not_eof = not . is_eof
+
+
 {- ASCII characters -}
 
 is_ascii_letter :: Char -> Bool
@@ -445,8 +459,6 @@
 
 {- explode symbols: ASCII, UTF8, named -}
 
-type Symbol = Bytes
-
 is_utf8 :: Word8 -> Bool
 is_utf8 b = b >= 128
 
@@ -1256,10 +1268,10 @@
 
 count_column :: Symbol -> Int -> Int
 count_column "\n" column = if_valid column 1
-count_column _ column = if_valid column (column + 1)
+count_column s column = if Symbol.not_eof s then if_valid column (column + 1) else column
 
 count_offset :: Symbol -> Int -> Int
-count_offset _ offset = if_valid offset (offset + 1)
+count_offset s offset = if Symbol.not_eof s then if_valid offset (offset + 1) else offset
 
 symbol :: Symbol -> T -> T
 symbol s pos =