# HG changeset patch
# User wenzelm
# Date 1545393659 -3600
# Node ID ce85542368b974af62f4c54a50baa2ffa733c833
# Parent  18c58b0da0a92f5e1cb6df1bbdabc6ae5a8754a4
more Haskell operations;

diff -r 18c58b0da0a9 -r ce85542368b9 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Fri Dec 21 12:38:30 2018 +0100
+++ b/src/Pure/General/symbol.ML	Fri Dec 21 13:00:59 2018 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/General/symbol.ML
     Author:     Makarius
 
-Generalized characters with infinitely many named symbols.
+Isabelle text symbols.
 *)
 
 signature SYMBOL =
diff -r 18c58b0da0a9 -r ce85542368b9 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Fri Dec 21 12:38:30 2018 +0100
+++ b/src/Pure/General/symbol.scala	Fri Dec 21 13:00:59 2018 +0100
@@ -1,7 +1,7 @@
 /*  Title:      Pure/General/symbol.scala
     Author:     Makarius
 
-Detecting and recoding Isabelle symbols.
+Isabelle text symbols.
 */
 
 package isabelle
diff -r 18c58b0da0a9 -r ce85542368b9 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Fri Dec 21 12:38:30 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Fri Dec 21 13:00:59 2018 +0100
@@ -8,6 +8,44 @@
   imports Pure
 begin
 
+generate_file "Isabelle/Symbol.hs" = \<open>
+{-  Title:      Isabelle/Symbols.hs
+    Author:     Makarius
+    LICENSE:    BSD 3-clause (Isabelle)
+
+Isabelle text symbols.
+-}
+
+module Isabelle.Symbol where
+
+{- ASCII characters -}
+
+is_ascii_letter :: Char -> Bool
+is_ascii_letter c = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z'
+
+is_ascii_digit :: Char -> Bool
+is_ascii_digit c = '0' <= c && c <= '9'
+
+is_ascii_hex :: Char -> Bool
+is_ascii_hex c = '0' <= c && c <= '9' || 'A' <= c && c <= 'F' || 'a' <= c && c <= 'f'
+
+is_ascii_quasi :: Char -> Bool
+is_ascii_quasi c = c == '_' || c == '\''
+
+is_ascii_blank :: Char -> Bool
+is_ascii_blank c = c `elem` " \t\n\11\f\r"
+
+is_ascii_line_terminator :: Char -> Bool
+is_ascii_line_terminator c = c == '\r' || c == '\n'
+
+is_ascii_letdig :: Char -> Bool
+is_ascii_letdig c = is_ascii_letter c || is_ascii_digit c || is_ascii_quasi c
+
+is_ascii_identifier :: String -> Bool
+is_ascii_identifier s =
+  not (null s) && is_ascii_letter (head s) && all is_ascii_letdig s
+\<close>
+
 generate_file "Isabelle/Library.hs" = \<open>
 {-  Title:      Isabelle/Library.hs
     Author:     Makarius