treat Symbol.eof as in ML (but: presently unused);

--- 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 =