signature SYMBOL = sig type symbol = string val explode: string -> symbol list val spaces: int -> string val STX: symbol val DEL: symbol val open_: symbol val close: symbol val space: symbol val is_space: symbol -> bool val comment: symbol val cancel: symbol val latex: symbol val marker: symbol val is_char: symbol -> bool val is_utf8: symbol -> bool val is_symbolic: symbol -> bool val is_symbolic_char: symbol -> bool val is_printable: symbol -> bool val control_prefix: string val control_suffix: string val is_control: symbol -> bool val eof: symbol val is_eof: symbol -> bool val not_eof: symbol -> bool val stopper: symbol Scan.stopper val is_malformed: symbol -> bool val malformed_msg: symbol -> string val is_ascii: symbol -> bool val is_ascii_letter: symbol -> bool val is_ascii_digit: symbol -> bool val is_ascii_hex: symbol -> bool val is_ascii_quasi: symbol -> bool val is_ascii_blank: symbol -> bool val is_ascii_line_terminator: symbol -> bool val is_ascii_control: symbol -> bool val is_ascii_letdig: symbol -> bool val is_ascii_lower: symbol -> bool val is_ascii_upper: symbol -> bool val to_ascii_lower: symbol -> symbol val to_ascii_upper: symbol -> symbol val is_ascii_identifier: string -> bool val scan_ascii_id: stringlist -> string * stringlist datatype sym =
Char ofstring | UTF8 ofstring | Sym ofstring | Control ofstring | Malformed ofstring | EOF val decode: symbol -> sym val encode: sym -> symbol datatype kind = Letter | Digit | Quasi | Blank | Other val kind: symbol -> kind val is_letter: symbol -> bool val is_digit: symbol -> bool val is_quasi: symbol -> bool val is_blank: symbol -> bool val is_control_block: symbol -> bool val has_control_block: symbol list -> bool val is_quasi_letter: symbol -> bool val is_letdig: symbol -> bool val beginning: int -> symbol list -> string val esc: symbol -> string val escape: string -> string val scanner: string -> (stringlist -> 'a * string list) -> symbol list -> 'a val split_words: symbol list -> stringlist val explode_words: string -> stringlist val trim_blanks: string -> string val bump_init: string -> string val bump_string: string -> string valsub: symbol val sup: symbol val bold: symbol val make_sub: string -> string val make_sup: string -> string val make_bold: string -> string val length: symbol list -> int val output: string -> Output.output * int end;
structure Symbol: SYMBOL = struct
(** type symbol **)
(*Symbols, which are considered the smallest entities of any Isabelle string, may be of the following form:
(1) ASCII: a (2) UTF-8: ä (2) regular symbols: \<ident> (3) 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 STX = chr 2; val DEL = chr 127;
val open_ = "\"; val close = "\";
val space = chr 32; fun is_space s = s = space;
local val spaces0 = Vector.tabulate (65, fn i => replicate_string i space); in fun spaces n = if n < 64 then Vector.nth spaces0 n else implode (Vector.nth spaces0 (n mod 64) :: replicate (n div 64) (Vector.nth spaces0 64)); end;
val comment = "\"; val cancel = "\<^cancel>"; val latex = "\<^latex>"; val marker = "\<^marker>";
fun is_char s = size s = 1;
fun is_utf8 s = size s > 0 andalso String.forall (fn c => Char.ord c >= 128) s;
fun raw_symbolic s = String.isPrefix "\092<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\092<^" s);
fun is_symbolic s =
s <> open_ andalso s <> close andalso raw_symbolic s;
val is_symbolic_char = member (op =) (raw_explode "!#$%&*+-/<=>?@^_|~");
fun is_printable s = if is_char s then 32 <= ord s andalso ord s <= Char.ord #"~" else is_utf8 s orelse raw_symbolic s;
val control_prefix = "\092<^"; val control_suffix = ">";
fun is_control s = String.isPrefix control_prefix s andalso String.isSuffix control_suffix s;
(* input source control *)
val eof = ""; fun is_eof s = s = eof; fun not_eof s = s <> eof; val stopper = Scan.stopper (K eof) is_eof;
fun is_malformed s = String.isPrefix "\092<" s andalso not (String.isSuffix ">" s)
orelse s = "\092<>" orelse s = "\092<^>";
fun malformed_msg s = "Malformed symbolic character: " ^ quote s;
(* ASCII symbols *)
fun is_ascii s = is_char s andalso ord s < 128;
fun is_ascii_letter s =
is_char s andalso
(Char.ord #"A" <= ord s andalso ord s <= Char.ord #"Z" orelse
Char.ord #"a" <= ord s andalso ord s <= Char.ord #"z");
fun is_ascii_digit s =
is_char s andalso Char.ord #"0" <= ord s andalso ord s <= Char.ord #"9";
fun is_ascii_hex s =
is_char s andalso
(Char.ord #"0" <= ord s andalso ord s <= Char.ord #"9" orelse
Char.ord #"A" <= ord s andalso ord s <= Char.ord #"F" orelse
Char.ord #"a" <= ord s andalso ord s <= Char.ord #"f");
fun is_ascii_control s = is_char s andalso ord s < 32 andalso not (is_ascii_blank s);
fun is_ascii_letdig s = is_ascii_letter s orelse is_ascii_digit s orelse is_ascii_quasi s;
fun is_ascii_lower s = is_char s andalso (Char.ord #"a" <= ord s andalso ord s <= Char.ord #"z"); fun is_ascii_upper s = is_char s andalso (Char.ord #"A" <= ord s andalso ord s <= Char.ord #"Z");
fun to_ascii_lower s = if is_ascii_upper s thenchr (ord s + Char.ord #"a" - Char.ord #"A") else s; fun to_ascii_upper s = if is_ascii_lower s thenchr (ord s + Char.ord #"A" - Char.ord #"a") else s;
fun is_ascii_identifier s = size s > 0 andalso is_ascii_letter (String.substring (s, 0, 1)) andalso
forall_string is_ascii_letdig s;
val scan_ascii_id = Scan.one is_ascii_letter ^^ (Scan.many is_ascii_letdig >> implode);
(* diagnostics *)
fun beginning n cs = let val drop_blanks = drop_suffix is_ascii_blank; val all_cs = drop_blanks cs; val dots = if length all_cs > n then" ..."else""; in
(drop_blanks (take n all_cs)
|> map (fn c => if is_ascii_blank c then space else c)
|> implode) ^ dots end;
fun decode s = if s = ""then EOF elseif is_char s then Char s elseif is_utf8 s then UTF8 s elseif is_malformed s then Malformed s elseif is_control s then Control (String.substring (s, 3, size s - 4)) else Sym (String.substring (s, 2, size s - 3));
fun encode (Char s) = s
| encode (UTF8 s) = s
| encode (Sym s) = "\092<" ^ s ^ ">"
| encode (Control s) = "\092<^" ^ s ^ ">"
| encode (Malformed s) = s
| encode EOF = "";
val is_letter_symbol = Symset.member letter_symbols;
end;
datatype kind = Letter | Digit | Quasi | Blank | Other;
fun kind s = if is_ascii_letter s then Letter elseif is_ascii_digit s then Digit elseif is_ascii_quasi s then Quasi elseif is_ascii_blank s then Blank elseif is_char s then Other elseif is_letter_symbol s then Letter else Other;
fun is_letter s = kind s = Letter; fun is_digit s = kind s = Digit; fun is_quasi s = kind s = Quasi; fun is_blank s = kind s = Blank;
val is_control_block = member (op =) ["\<^bsub>", "\<^esub>", "\<^bsup>", "\<^esup>"]; val has_control_block = exists is_control_block;
fun is_quasi_letter s = letval k = kind s in k = Letter orelse k = Quasi end; fun is_letdig s = letval k = kind s in k = Letter orelse k = Digit orelse k = Quasi end;
(* escape *)
val esc = fn s => if is_char s then s elseif is_utf8 s then translate_string (fn c => "\\" ^ string_of_int (ord c)) s else"\\" ^ s;
val escape = implode o map esc o Symbol.explode;
(** scanning through symbols **)
(* scanner *)
fun scanner msg scan syms = let fun message (ss, NONE) = (fn () => msg ^ ": " ^ quote (beginning 10 ss))
| message (ss, SOME msg') = (fn () => msg ^ ", " ^ msg' () ^ ": " ^ quote (beginning 10 ss)); val finite_scan = Scan.error (Scan.finite stopper (!! message scan)); in
(case finite_scan syms of
(result, []) => result
| (_, rest) => error (message (rest, NONE) ())) end;
(* space-separated words *)
val scan_word =
Scan.many1 is_ascii_blank >> K NONE ||
Scan.many1 (fn s => not (is_ascii_blank s) andalso not_eof s) >> (SOME o implode);
val trim_blanks = Symbol.explode #> trim is_blank #> implode;
(* bump string -- treat as base 26 or base 1 numbers *)
fun symbolic_end (_ :: "\<^sub>" :: _) = true
| symbolic_end ("'" :: ss) = symbolic_end ss
| symbolic_end (s :: _) = raw_symbolic s
| symbolic_end [] = false;
fun bump_init str = if symbolic_end (rev (Symbol.explode str)) then str ^ "'" else str ^ "a";
fun bump_string str = let fun bump [] = ["a"]
| bump ("z" :: ss) = "a" :: bump ss
| bump (s :: ss) = if is_char s andalso Char.ord #"a" <= ord s andalso ord s < Char.ord #"z" thenchr (ord s + 1) :: ss else"a" :: s :: ss;
val (ss, qs) = apfst rev (chop_suffix is_quasi (Symbol.explode str)); val ss' = if symbolic_end ss then "'" :: ss else bump ss; in implode (rev ss' @ qs) end;
(* styles *)
valsub = "\092<^sub>"; val sup = "\092<^sup>"; val bold = "\092<^bold>";
fun make_style sym =
Symbol.explode #> maps (fn s => [sym, s]) #> implode;
val make_sub = make_style sub; val make_sup = make_style sup; val make_bold = make_style bold;
(** symbol output **)
(* metric *)
fun metric1 s = ifString.isPrefix "\092 s then 4 elseifString.isPrefix "\092 s then 3 elseifString.isPrefix "\092 s orelse String.isPrefix "\092 s then 2 elseif is_blank s orelse is_printable s then 1 else 0;
fun metric ss = fold (fn s => fn n => metric1 s + n) ss 0;
fun output s = (s, metric (Symbol.explode s));
(*final declarations of this structure!*) val explode = Symbol.explode; val length = metric;
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
