# HG changeset patch # User wenzelm # Date 1005261257 -3600 # Node ID 4027b15377a5784d5ef4b6da78db6066ec7e0560 # Parent d0d41884f787caec4fc3c70c4ae0e1f812fbdc83 got rid of obsolete input filtering; diff -r d0d41884f787 -r 4027b15377a5 src/Pure/General/file.ML --- 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; diff -r d0d41884f787 -r 4027b15377a5 src/Pure/General/symbol.ML --- 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: \ (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! *) - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\" -(* 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); diff -r d0d41884f787 -r 4027b15377a5 src/Sequents/LK0.thy --- 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 ("\\ _" [40] 40) "op &" :: [o, o] => o (infixr "\\" 35) "op |" :: [o, o] => o (infixr "\\" 30) - "op -->" :: [o, o] => o (infixr "\\\\" 25) - "op <->" :: [o, o] => o (infixr "\\\\" 25) + "op -->" :: [o, o] => o (infixr "\\" 25) + "op <->" :: [o, o] => o (infixr "\\" 25) "ALL " :: [idts, o] => o ("(3\\_./ _)" [0, 10] 10) "EX " :: [idts, o] => o ("(3\\_./ _)" [0, 10] 10) "EX! " :: [idts, o] => o ("(3\\!_./ _)" [0, 10] 10) "op ~=" :: ['a, 'a] => o (infixl "\\" 50) -syntax (xsymbols) - "op -->" :: [o, o] => o (infixr "\\" 25) - "op <->" :: [o, o] => o (infixr "\\" 25) - syntax (HTML output) Not :: o => o ("\\ _" [40] 40)