# 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! *)
+  "\\<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 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 | "\\<space2>" => 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;