# HG changeset patch # User wenzelm # Date 889455934 -3600 # Node ID 8cec457a8961169f838c56cdc4cfe304cae5da16 # Parent 74a12e86b20bd9c3d70e60dd8f1179c737c4b991 replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML; diff -r 74a12e86b20b -r 8cec457a8961 Admin/fixencoding --- a/Admin/fixencoding Sat Mar 07 16:29:29 1998 +0100 +++ b/Admin/fixencoding Mon Mar 09 16:05:34 1998 +0100 @@ -123,7 +123,7 @@ # make tables for ($current = $enc_first; $current <= $enc_last; $current++) { - push(@ml_tab, '"' . $enc_tab[$current] . '"'); + push(@ml_tab, '"\\\\<' . $enc_tab[$current] . '>"'); push(@perl_tab, sprintf('"\\x%2x", "\\\\<%s>"', $current, $enc_tab[$current])); push(@perl_revtab, sprintf('"\\\\<%s>", "\\x%2x"', $enc_tab[$current], $current)); } @@ -135,7 +135,7 @@ # patch files -&patch_file("Pure/Syntax/symbol_font.ML", $ml_tab); +&patch_file("Pure/Syntax/symbol.ML", $ml_tab); &patch_file("Distribution/lib/scripts/symbolinput.pl", $perl_tab); &patch_file("Distribution/lib/scripts/feeder.pl", $perl_tab); #&patch_file("Distribution/lib/scripts/symboloutput.pl", $perl_revtab); diff -r 74a12e86b20b -r 8cec457a8961 src/Pure/Syntax/symbol.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Syntax/symbol.ML Mon Mar 09 16:05:34 1998 +0100 @@ -0,0 +1,235 @@ +(* Title: Pure/Syntax/symbol.ML + ID: $Id$ + Author: Markus Wenzel, TU Muenchen + +Baroque characters. +*) + +signature SYMBOL = +sig + type symbol + val eof: symbol + val is_eof: symbol -> bool + val not_eof: symbol -> bool + val is_ascii: symbol -> bool + val is_letter: symbol -> bool + val is_digit: symbol -> bool + val is_quasi_letter: symbol -> bool + val is_letdig: symbol -> bool + val is_blank: symbol -> bool + val is_printable: symbol -> bool + val scan: string list -> symbol * string list + val explode: string -> symbol list + val input: string -> string + val output: string -> string +end; + +structure Symbol: SYMBOL = +struct + + +(** encoding table (isabelle-0) **) + +val enc_start = 160; +val enc_end = 255; + +val enc_vector = +[ +(* GENERATED TEXT FOLLOWS - Do not edit! *) + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\" +(* END OF GENERATED TEXT *) +]; + +val enc_rel = enc_vector ~~ map chr (enc_start upto enc_end); + +val char_tab = Symtab.make enc_rel; +val symbol_tab = Symtab.make (map swap enc_rel); + +fun lookup_symbol c = + if ord c < enc_start then None + else Symtab.lookup (symbol_tab, c); + + +(* encode / decode *) + +fun char s = if_none (Symtab.lookup (char_tab, s)) s; +fun symbol c = if_none (lookup_symbol c) c; + +fun symbol' c = + (case lookup_symbol c of + None => c + | Some s => "\\" ^ s); + + + +(** type symbol **) + +type symbol = string; + + +(* kinds *) + +val eof = ""; +fun is_eof s = s = eof; +fun not_eof s = s <> eof; + +fun is_ascii s = size s = 1 andalso ord s < 128; + +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"); + +fun is_digit s = + size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9"; + +fun is_quasi_letter "_" = true + | is_quasi_letter "'" = true + | is_quasi_letter s = is_letter s; + +val is_blank = + fn " " => true | "\t" => true | "\n" => true | "\^L" => true | "\\" => true + | _ => false; + +val is_letdig = is_quasi_letter orf is_digit; + +fun is_printable s = + size s = 1 andalso ord " " <= ord s andalso ord s <= ord "~" orelse + size s > 2 andalso nth_elem (2, explode s) <> "^"; + + +(* scan *) + +val scan_id = Scan.one is_letter ^^ (Scan.any is_letdig >> implode); + +val scan = + ($$ "\\" --| Scan.optional ($$ "\\") "") ^^ $$ "<" ^^ + !! (fn cs => "Malformed symbolic character specification: \\" ^ "<" ^ beginning cs) + (Scan.optional ($$ "^") "" ^^ scan_id ^^ $$ ">") || + Scan.one not_eof; + + +(* explode *) + +fun no_syms [] = true + | no_syms ("\\" :: "<" :: _) = false + | no_syms (c :: cs) = ord c < enc_start andalso no_syms cs; + +fun sym_explode str = + let val chs = explode str in + if no_syms chs then chs (*tune trivial case*) + else map symbol (#1 (Scan.error (Scan.finite eof (Scan.repeat scan)) chs)) + end; + + +(* input / output *) + +fun input str = + let val chs = explode str in + if forall (fn c => ord c < enc_start) chs then str + else implode (map symbol' chs) + end; + +val output = implode o map char o sym_explode; + + +(*final declaration of this structure!*) +val explode = sym_explode; + + +end; diff -r 74a12e86b20b -r 8cec457a8961 src/Pure/Syntax/symbol_font.ML --- a/src/Pure/Syntax/symbol_font.ML Sat Mar 07 16:29:29 1998 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,191 +0,0 @@ -(* Title: Pure/Syntax/symbol_font.ML - ID: $Id$ - Author: Markus Wenzel, TU Muenchen - -The Isabelle symbol font. -*) - -signature SYMBOL_FONT = -sig - val char: string -> string option - val name: string -> string option - val read_charnames: string list -> string list - val read_chnames: string -> string - val write_charnames: string list -> string list (*normal backslashes*) - val write_chnames: string -> string - val write_charnames': string list -> string list (*escaped backslashes*) - val write_chnames': string -> string -end; - - -structure SymbolFont : SYMBOL_FONT = -struct - - -(** font encoding vector **) - -(* tables *) - -val enc_start = 160; -val enc_end = 255; - -val enc_vector = -[ -(* GENERATED TEXT FOLLOWS - Do not edit! *) - "space2", - "Gamma", - "Delta", - "Theta", - "Lambda", - "Pi", - "Sigma", - "Phi", - "Psi", - "Omega", - "alpha", - "beta", - "gamma", - "delta", - "epsilon", - "zeta", - "eta", - "theta", - "kappa", - "lambda", - "mu", - "nu", - "xi", - "pi", - "rho", - "sigma", - "tau", - "phi", - "chi", - "psi", - "omega", - "not", - "and", - "or", - "forall", - "exists", - "And", - "lceil", - "rceil", - "lfloor", - "rfloor", - "turnstile", - "Turnstile", - "lbrakk", - "rbrakk", - "cdot", - "in", - "subseteq", - "inter", - "union", - "Inter", - "Union", - "sqinter", - "squnion", - "Sqinter", - "Squnion", - "bottom", - "doteq", - "equiv", - "noteq", - "sqsubset", - "sqsubseteq", - "prec", - "preceq", - "succ", - "approx", - "sim", - "simeq", - "le", - "Colon", - "leftarrow", - "midarrow", - "rightarrow", - "Leftarrow", - "Midarrow", - "Rightarrow", - "bow", - "mapsto", - "leadsto", - "up", - "down", - "notin", - "times", - "oplus", - "ominus", - "otimes", - "oslash", - "subset", - "infinity", - "box", - "diamond", - "circ", - "bullet", - "parallel", - "surd", - "copyright" -(* END OF GENERATED TEXT *) -]; - -val enc_rel = enc_vector ~~ (map chr (enc_start upto enc_end)); - -val enc_tab = Symtab.make enc_rel; -val dec_tab = Symtab.make (map swap enc_rel); - - -(* chars and names *) - -fun char name = Symtab.lookup (enc_tab, name); - -fun name char = - if ord char < enc_start then None - else Symtab.lookup (dec_tab, char); - - - -(** input and output of symbols **) - -(* read_charnames *) - -local - open Scanner; - - fun scan_symbol ("\\" :: "<" :: cs) = - let - val (name, cs') = (scan_id -- $$ ">" >> #1) cs handle LEXICAL_ERROR - => error ("Malformed symbolic char specification: \"\\<" ^ implode cs ^ "\""); - val c = the (char name) handle OPTION - => error ("Unknown symbolic char name: " ^ quote name); - in (c, cs') end - | scan_symbol _ = raise LEXICAL_ERROR; -in - fun read_charnames chs = - if forall (not_equal "\\") chs then chs - else #1 (repeat (scan_symbol || scan_one (K true)) chs); - - val read_chnames = implode o read_charnames o explode; -end; - - -(* write_charnames *) - -fun write_char prfx ch = - (case name ch of - None => ch - | Some nm => prfx ^ "\\<" ^ nm ^ ">"); - -fun write_chars prfx chs = - if forall (fn ch => ord ch < enc_start) chs then chs - else map (write_char prfx) chs; - -val write_charnames = write_chars ""; -val write_charnames' = write_chars "\\"; - -val write_chnames = implode o write_charnames o explode; -val write_chnames' = implode o write_charnames' o explode; - -end;