got rid of obsolete input filtering;

--- a/src/Pure/General/file.ML	Fri Nov 09 00:11:52 2001 +0100
+++ b/src/Pure/General/file.ML	Fri Nov 09 00:14:17 2001 +0100
@@ -27,8 +27,7 @@
   val exists: Path.T -> bool
   val mkdir: Path.T -> unit
   val copy_all: Path.T -> Path.T -> unit
-  val plain_use: Path.T -> unit
-  val symbol_use: Path.T -> unit
+  val use: Path.T -> unit
 end;
 
 structure File: FILE =
@@ -106,27 +105,8 @@
   system_command ("cp -r " ^ quote_sysify_path path1 ^ " " ^ quote_sysify_path path2);
 
 
-(* symbol_use *)
-
-val plain_use = use o sysify_path;
-
-(* version of 'use' with input filtering *)
+(* use ML files *)
 
-val symbol_use =
-  if not needs_filtered_use then plain_use	(*ML system (wrongly!) accepts non-ASCII*)
-  else
-    fn path =>
-      let
-        val txt = read path;
-        val txt_out = Symbol.input txt;
-      in
-        if txt = txt_out then plain_use path
-        else
-          let val tmp_path = tmp_path path in
-            write tmp_path txt_out;
-            plain_use tmp_path handle exn => (rm tmp_path; raise exn);
-            rm tmp_path
-          end
-      end;
+val use = use o sysify_path;
 
 end;

--- a/src/Pure/General/symbol.ML	Fri Nov 09 00:11:52 2001 +0100
+++ b/src/Pure/General/symbol.ML	Fri Nov 09 00:14:17 2001 +0100
@@ -3,7 +3,7 @@
     Author:     Markus Wenzel, TU Muenchen
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Generalized characters, independent of encoding.
+Generalized characters with infinitely many named symbols.
 *)
 
 signature SYMBOL =
@@ -35,10 +35,8 @@
   val source: bool -> (string, 'a) Source.source ->
     (symbol, (string, 'a) Source.source) Source.source
   val explode: string -> symbol list
-  val input: string -> string
   val default_indent: string * int -> string
   val add_mode: string -> (string -> string * real) * (string * int -> string) -> unit
-  val isabelle_fontN: string
   val symbolsN: string
   val xsymbolsN: string
   val plain_output: string -> string
@@ -59,8 +57,8 @@
     (b) printable symbols: \<ident>
     (c) control symbols: \<^ident>
 
-  input may include non-ASCII characters according to isabelle-0 encoding;
-  output is subject to the print_mode variable (default: verbatim);
+  output is subject to the print_mode variable (default: verbatim),
+  actual interpretation in display is up to front-end tools;
 *)
 
 type symbol = string;
@@ -133,135 +131,6 @@
 
 
 
-(** isabelle-0 encoding table **)
-
-val enc_start = 160;
-val enc_end = 255;
-
-val enc_vector =
-[
-(* GENERATED TEXT FOLLOWS - Do not edit! *)
-  "\\<spacespace>",
-  "\\<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>",
-  "\\<frown>",
-  "\\<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);
-
-
-
 (** scanning through symbols **)
 
 fun scanner msg scan chs =
@@ -301,21 +170,12 @@
 
 fun no_syms [] = true
   | no_syms ("\\" :: "<" :: _) = false
-  | no_syms (c :: cs) = ord c < enc_start andalso no_syms cs;
+  | no_syms (_ :: cs) = 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 (the (Scan.read stopper (Scan.repeat scan) chs))
-  end;
-
-
-(* input *)
-
-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)
+    else the (Scan.read stopper (Scan.repeat scan) chs)
   end;
 
 
@@ -333,22 +193,13 @@
 fun default_indent (_: string, k) = spaces k;
 
 
-(* isabelle_font *)
-
-fun isabelle_font_output s =
-  let val cs = sym_explode s
-  in (implode (map char cs), real (sym_length cs)) end;
-
-val isabelle_font_indent = default_indent;
-
-
 (* maintain modes *)
 
-val isabelle_fontN = "isabelle_font";
 val symbolsN = "symbols";
 val xsymbolsN = "xsymbols";
 
-val modes = ref (Symtab.make [(isabelle_fontN, (isabelle_font_output, isabelle_font_indent))]);
+val modes =
+  ref (Symtab.empty: ((string -> string * real) * (string * int -> string)) Symtab.table);
 
 fun lookup_mode name = Symtab.lookup (! modes, name);
 

--- a/src/Sequents/LK0.thy	Fri Nov 09 00:11:52 2001 +0100
+++ b/src/Sequents/LK0.thy	Fri Nov 09 00:14:17 2001 +0100
@@ -40,21 +40,17 @@
 translations
   "x ~= y"      == "~ (x = y)"
 
-syntax (symbols)
+syntax (xsymbols)
   Not           :: o => o               ("\\<not> _" [40] 40)
   "op &"        :: [o, o] => o          (infixr "\\<and>" 35)
   "op |"        :: [o, o] => o          (infixr "\\<or>" 30)
-  "op -->"      :: [o, o] => o          (infixr "\\<midarrow>\\<rightarrow>" 25)
-  "op <->"      :: [o, o] => o          (infixr "\\<leftarrow>\\<rightarrow>" 25)
+  "op -->"      :: [o, o] => o          (infixr "\\<longrightarrow>" 25)
+  "op <->"      :: [o, o] => o          (infixr "\\<longleftrightarrow>" 25)
   "ALL "        :: [idts, o] => o       ("(3\\<forall>_./ _)" [0, 10] 10)
   "EX "         :: [idts, o] => o       ("(3\\<exists>_./ _)" [0, 10] 10)
   "EX! "        :: [idts, o] => o       ("(3\\<exists>!_./ _)" [0, 10] 10)
   "op ~="       :: ['a, 'a] => o        (infixl "\\<noteq>" 50)
 
-syntax (xsymbols)
-  "op -->"      :: [o, o] => o          (infixr "\\<longrightarrow>" 25)
-  "op <->"      :: [o, o] => o          (infixr "\\<longleftrightarrow>" 25)
-
 syntax (HTML output)
   Not           :: o => o               ("\\<not> _" [40] 40)