<commit_before>(*  Title:      Pure/General/symbol.ML
    ID:         $Id$
    Author:     <NAME>, <NAME>
    License:    GPL (GNU GENERAL PUBLIC LICENSE)

Generalized characters with infinitely many named symbols.
*)

signature SYMBOL =
sig
  type symbol
  val space: symbol
  val spaces: int -> symbol
  val sync: symbol
  val is_sync: symbol -> bool
  val not_sync: symbol -> bool
  val malformed: symbol
  val eof: symbol
  val is_eof: symbol -> bool
  val not_eof: symbol -> bool
  val stopper: symbol * (symbol -> bool)
  val is_ascii: symbol -> bool
  val is_letter: symbol -> bool
  val is_digit: symbol -> bool
  val is_quasi: symbol -> bool
  val is_quasi_letter: symbol -> bool
  val is_letdig: symbol -> bool
  val is_blank: symbol -> bool
  val is_identifier: symbol -> bool
  val is_symbolic: symbol -> bool
  val is_printable: symbol -> bool
  val length: symbol list -> int
  val strip_blanks: string -> string
  val beginning: symbol list -> string
  val scan_id: string list -> string * string list
  val scan: string list -> symbol * string list
  val scanner: string -> (symbol list -> 'a * symbol list) -> symbol list -> 'a
  val source: bool -> (string, 'a) Source.source ->
    (symbol, (string, 'a) Source.source) Source.source
  val explode: string -> symbol list
  val bump_string: string -> string
  val default_indent: string * int -> string
  val add_mode: string -> (string -> string * real) * (string * int -> string) -> unit
  val symbolsN: string
  val xsymbolsN: string
  val plain_output: string -> string
  val output: string -> string
  val output_width: string -> string * real
  val indent: string * int -> string
end;

structure Symbol: SYMBOL =
struct


(** generalized characters **)

(*symbols, which are considered the smallest entities of any Isabelle
  string, may be of the following form:
    (a) ASCII symbols: a
    (b) printable symbols: \<ident>
    (c) control symbols: \<^ident>

  output is subject to the print_mode variable (default: verbatim),
  actual interpretation in display is up to front-end tools;
*)

type symbol = string;

val space = " ";
fun spaces k = Library.replicate_string k space;
val sync = "\\<^sync>";
val malformed = "\\<^malformed>";
val eof = "";


(* kinds *)

fun is_sync s = s = sync;
fun not_sync s = s <> sync;

fun is_eof s = s = eof;
fun not_eof s = s <> eof;
val stopper = (eof, is_eof);

fun is_ascii s = size s = 1 andalso ord s < 128;

local
    fun wrap s = "\\<" ^ s ^ ">"

    val cal_letters =
	["A","B","C","D","E","F","G","H","I","J","K","L","M",
	 "N","O","P","Q","R","S","T","U","V","W","X","Y","Z"]

    val small_letters =
	["a","b","c","d","e","f","g","h","i","j","k","l","m",
	 "n","o","p","q","r","s","t","u","v","w","x","y","z"]

    val goth_letters =
	["AA","BB","CC","DD","EE","FF","GG","HH","II","JJ","KK","LL","MM",
	 "NN","OO","PP","QQ","RR","SS","TT","UU","VV","WW","XX","YY","ZZ",
	 "aa","bb","cc","dd","ee","ff","gg","hh","ii","jj","kk","ll","mm",
	 "nn","oo","pp","qq","rr","ss","tt","uu","vv","ww","xx","yy","zz"]

    val greek_letters =
	["alpha","beta","gamma","delta","epsilon","zeta","eta","theta",
	 "iota","kappa",(*"lambda",*)"mu","nu","xi","pi","rho","sigma","tau",
	 "upsilon","phi","psi","omega","Gamma","Delta","Theta","Lambda",
	 "Xi","Pi","Sigma","Upsilon","Phi","Psi","Omega"]

    val bbb_letters = ["bool","complex","nat","rat","real","int"]

    val pre_letters =
	cal_letters   @
	small_letters @
	goth_letters  @
	greek_letters
in
val ext_letters = map wrap pre_letters

fun is_ext_letter s = String.isPrefix "\\<" s andalso s mem ext_letters
end
     
fun is_letter s =
    (size s = 1 andalso
     (ord "A" <= ord s andalso ord s <= ord "Z" orelse
      ord "a" <= ord s andalso ord s <= ord "z"))
    orelse is_ext_letter s

fun is_digit s =
    size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9"

fun is_quasi "_" = true
  | is_quasi "'" = true
  | is_quasi _ = false;
<commit_msg>included \<^sub> in the range of identifier chars<commit_after>(*  Title:      Pure/General/symbol.ML
    ID:         $Id$
    Author:     <NAME>, <NAME>
    License:    GPL (GNU GENERAL PUBLIC LICENSE)

Generalized characters with infinitely many named symbols.
*)

signature SYMBOL =
sig
  type symbol
  val space: symbol
  val spaces: int -> symbol
  val sync: symbol
  val is_sync: symbol -> bool
  val not_sync: symbol -> bool
  val malformed: symbol
  val eof: symbol
  val is_eof: symbol -> bool
  val not_eof: symbol -> bool
  val stopper: symbol * (symbol -> bool)
  val is_ascii: symbol -> bool
  val is_letter: symbol -> bool
  val is_digit: symbol -> bool
  val is_quasi: symbol -> bool
  val is_quasi_letter: symbol -> bool
  val is_letdig: symbol -> bool
  val is_blank: symbol -> bool
  val is_identifier: symbol -> bool
  val is_symbolic: symbol -> bool
  val is_printable: symbol -> bool
  val length: symbol list -> int
  val strip_blanks: string -> string
  val beginning: symbol list -> string
  val scan_id: string list -> string * string list
  val scan: string list -> symbol * string list
  val scanner: string -> (symbol list -> 'a * symbol list) -> symbol list -> 'a
  val source: bool -> (string, 'a) Source.source ->
    (symbol, (string, 'a) Source.source) Source.source
  val explode: string -> symbol list
  val bump_string: string -> string
  val default_indent: string * int -> string
  val add_mode: string -> (string -> string * real) * (string * int -> string) -> unit
  val symbolsN: string
  val xsymbolsN: string
  val plain_output: string -> string
  val output: string -> string
  val output_width: string -> string * real
  val indent: string * int -> string
end;

structure Symbol: SYMBOL =
struct


(** generalized characters **)

(*symbols, which are considered the smallest entities of any Isabelle
  string, may be of the following form:
    (a) ASCII symbols: a
    (b) printable symbols: \<ident>
    (c) control symbols: \<^ident>

  output is subject to the print_mode variable (default: verbatim),
  actual interpretation in display is up to front-end tools;
*)

type symbol = string;

val space = " ";
fun spaces k = Library.replicate_string k space;
val sync = "\\<^sync>";
val malformed = "\\<^malformed>";
val eof = "";


(* kinds *)

fun is_sync s = s = sync;
fun not_sync s = s <> sync;

fun is_eof s = s = eof;
fun not_eof s = s <> eof;
val stopper = (eof, is_eof);

fun is_ascii s = size s = 1 andalso ord s < 128;

local
    fun wrap s = "\\<" ^ s ^ ">"

    val cal_letters =
	["A","B","C","D","E","F","G","H","I","J","K","L","M",
	 "N","O","P","Q","R","S","T","U","V","W","X","Y","Z"]

    val small_letters =
	["a","b","c","d","e","f","g","h","i","j","k","l","m",
	 "n","o","p","q","r","s","t","u","v","w","x","y","z"]

    val goth_letters =
	["AA","BB","CC","DD","EE","FF","GG","HH","II","JJ","KK","LL","MM",
	 "NN","OO","PP","QQ","RR","SS","TT","UU","VV","WW","XX","YY","ZZ",
	 "aa","bb","cc","dd","ee","ff","gg","hh","ii","jj","kk","ll","mm",
	 "nn","oo","pp","qq","rr","ss","tt","uu","vv","ww","xx","yy","zz"]

    val greek_letters =
	["alpha","beta","gamma","delta","epsilon","zeta","eta","theta",
	 "iota","kappa",(*"lambda",*)"mu","nu","xi","pi","rho","sigma","tau",
	 "upsilon","phi","psi","omega","Gamma","Delta","Theta","Lambda",
	 "Xi","Pi","Sigma","Upsilon","Phi","Psi","Omega"]

    val bbb_letters = ["bool","complex","nat","rat","real","int"]

    val control_letters = ["^sub"]
 
    val pre_letters =
	cal_letters   @
	small_letters @
	goth_letters  @
	greek_letters @
	control_letters

in
val ext_letters = map wrap pre_letters 

fun is_ext_letter s = String.isPrefix "\\<" s andalso s mem ext_letters
end
     
fun is_letter s =
    (size s = 1 andalso
     (ord "A" <= ord s andalso ord s <= ord "Z" orelse
      ord "a" <= ord s andalso ord s <= ord "z"))
    orelse is_ext_letter s

fun is_digit s =
    size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9"

fun is_quasi "_" = true
  | is_quasi "'" = true
  | is_quasi _ = false;

{'fraction_non_alphanumeric': 0.1966574516210103, 'fraction_numerical': 0.0020105554159336515, 'mean_word_length': 3.7601674641148324, 'pattern_counts': {'":': 0, '<': 38, '<?xml version=': 0, '>': 98, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '211095', 'n_tokens_mistral': 2849, 'n_tokens_neox': 2700, 'n_words': 833}