--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/README Wed Jan 13 12:44:33 1999 +0100
@@ -0,0 +1,20 @@
+
+ Pure/General/
+
+
+This directory contains general purpose modules, all of which are
+exported.
+
+ TableFun (generic tables)
+ Symtab (tables indexed by strings)
+ Object (generic objects of arbitrary type)
+ Seq (unbounded sequences)
+ NameSpace (hierarchically structured name spaces)
+ Position (input positions)
+ Path (abstract algebra of file paths)
+ File (file system operations)
+ History (histories of values, with undo and redo)
+ Scan (generic scanner toolbox)
+ Source (co-algebraic data sources)
+ Symbol (generalized characters)
+ Pretty (generic pretty printing module)
--- a/src/Pure/General/ROOT.ML Wed Jan 13 12:16:34 1999 +0100
+++ b/src/Pure/General/ROOT.ML Wed Jan 13 12:44:33 1999 +0100
@@ -12,6 +12,10 @@
use "path.ML";
use "file.ML";
use "history.ML";
+use "scan.ML";
+use "source.ML";
+use "symbol.ML";
+use "pretty.ML";
structure PureGeneral =
struct
@@ -23,4 +27,8 @@
structure Path = Path;
structure File = File;
structure History = History;
+ structure Scan = Scan;
+ structure Source = Source;
+ structure Symbol = Symbol;
+ structure Pretty = Pretty;
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/pretty.ML Wed Jan 13 12:44:33 1999 +0100
@@ -0,0 +1,249 @@
+(* Title: Pure/Syntax/pretty.ML
+ ID: $Id$
+ Author: Lawrence C Paulson
+ Copyright 1991 University of Cambridge
+
+Generic pretty printing module.
+
+Loosely based on
+ D. C. Oppen, "Pretty Printing",
+ ACM Transactions on Programming Languages and Systems (1980), 465-483.
+
+The object to be printed is given as a tree with indentation and line
+breaking information. A "break" inserts a newline if the text until
+the next break is too long to fit on the current line. After the newline,
+text is indented to the level of the enclosing block. Normally, if a block
+is broken then all enclosing blocks will also be broken. Only "inconsistent
+breaks" are provided.
+
+The stored length of a block is used in breakdist (to treat each inner block as
+a unit for breaking).
+*)
+
+type pprint_args = (string -> unit) * (int -> unit) * (int -> unit) *
+ (unit -> unit) * (unit -> unit);
+
+signature PRETTY =
+ sig
+ type T
+ val str: string -> T
+ val strlen: string -> int -> T
+ val sym: string -> T
+ val spc: int -> T
+ val brk: int -> T
+ val fbrk: T
+ val blk: int * T list -> T
+ val lst: string * string -> T list -> T
+ val quote: T -> T
+ val commas: T list -> T list
+ val breaks: T list -> T list
+ val fbreaks: T list -> T list
+ val block: T list -> T
+ val strs: string list -> T
+ val enclose: string -> string -> T list -> T
+ val list: string -> string -> T list -> T
+ val str_list: string -> string -> string list -> T
+ val big_list: string -> T list -> T
+ val string_of: T -> string
+ val writeln: T -> unit
+ val str_of: T -> string
+ val pprint: T -> pprint_args -> unit
+ val setdepth: int -> unit
+ val setmargin: int -> unit
+ end;
+
+structure Pretty : PRETTY =
+struct
+
+(*printing items: compound phrases, strings, and breaks*)
+datatype T =
+ Block of T list * int * int | (*body, indentation, length*)
+ String of string * int | (*text, length*)
+ Break of bool * int; (*mandatory flag, width if not taken*);
+
+(*Add the lengths of the expressions until the next Break; if no Break then
+ include "after", to account for text following this block. *)
+fun breakdist (Block(_,_,len)::es, after) = len + breakdist(es, after)
+ | breakdist (String (s, len) :: es, after) = len + breakdist (es, after)
+ | breakdist (Break _ :: es, after) = 0
+ | breakdist ([], after) = after;
+
+fun repstring a 0 = ""
+ | repstring a 1 = a
+ | repstring a k =
+ if k mod 2 = 0 then repstring(a^a) (k div 2)
+ else repstring(a^a) (k div 2) ^ a;
+
+(*** Type for lines of text: string, # of lines, position on line ***)
+
+type text = {tx: string, nl: int, pos: int};
+
+val emptytext = {tx="", nl=0, pos=0};
+
+fun blanks wd {tx,nl,pos} =
+ {tx = tx ^ repstring " " wd,
+ nl = nl,
+ pos = pos+wd};
+
+fun newline {tx,nl,pos} =
+ {tx = tx ^ "\n",
+ nl = nl+1,
+ pos = 0};
+
+fun string s len {tx,nl,pos:int} =
+ {tx = tx ^ s,
+ nl = nl,
+ pos = pos + len};
+
+
+(*** Formatting ***)
+
+(* margin *)
+
+(*example values*)
+val margin = ref 80 (*right margin, or page width*)
+and breakgain = ref 4 (*minimum added space required of a break*)
+and emergencypos = ref 40; (*position too far to right*)
+
+fun setmargin m =
+ (margin := m;
+ breakgain := !margin div 20;
+ emergencypos := !margin div 2);
+
+val () = setmargin 76;
+
+
+(*Search for the next break (at this or higher levels) and force it to occur*)
+fun forcenext [] = []
+ | forcenext (Break(_,wd) :: es) = Break(true,0) :: es
+ | forcenext (e :: es) = e :: forcenext es;
+
+(*es is list of expressions to print;
+ blockin is the indentation of the current block;
+ after is the width of the following context until next break. *)
+fun format ([], _, _) text = text
+ | format (e::es, blockin, after) (text as {pos,nl,...}) =
+ (case e of
+ Block(bes,indent,wd) =>
+ let val blockin' = (pos + indent) mod !emergencypos
+ val btext = format(bes, blockin', breakdist(es,after)) text
+ (*If this block was broken then force the next break.*)
+ val es2 = if nl < #nl(btext) then forcenext es else es
+ in format (es2,blockin,after) btext end
+ | String (s, len) => format (es,blockin,after) (string s len text)
+ | Break(force,wd) => (*no break if text to next break fits on this line
+ or if breaking would add only breakgain to space *)
+ format (es,blockin,after)
+ (if not force andalso
+ pos+wd <= Int.max(!margin - breakdist(es,after),
+ blockin + !breakgain)
+ then blanks wd text (*just insert wd blanks*)
+ else blanks blockin (newline text)));
+
+
+(*** Exported functions to create formatting expressions ***)
+
+fun length (Block (_, _, len)) = len
+ | length (String (_, len)) = len
+ | length (Break(_, wd)) = wd;
+
+fun str s = String (s, size s);
+fun strlen s len = String (s, len);
+fun sym s = String (s, Symbol.size s);
+
+fun spc n = str (repstring " " n);
+
+fun brk wd = Break (false, wd);
+val fbrk = Break (true, 0);
+
+fun blk (indent, es) =
+ let
+ fun sum([], k) = k
+ | sum(e :: es, k) = sum (es, length e + k);
+ in Block (es, indent, sum (es, 0)) end;
+
+(*Join the elements of es as a comma-separated list, bracketted by lp and rp*)
+fun lst(lp,rp) es =
+ let fun add(e,es) = str"," :: brk 1 :: e :: es;
+ fun list(e :: (es as _::_)) = str lp :: e :: foldr add (es,[str rp])
+ | list(e::[]) = [str lp, e, str rp]
+ | list([]) = []
+ in blk(size lp, list es) end;
+
+
+(* utils *)
+
+fun quote prt =
+ blk (1, [str "\"", prt, str "\""]);
+
+fun commas prts =
+ flat (separate [str ",", brk 1] (map (fn x => [x]) prts));
+
+fun breaks prts = separate (brk 1) prts;
+
+fun fbreaks prts = separate fbrk prts;
+
+fun block prts = blk (2, prts);
+
+val strs = block o breaks o (map str);
+
+fun enclose lpar rpar prts =
+ block (str lpar :: (prts @ [str rpar]));
+
+fun list lpar rpar prts =
+ enclose lpar rpar (commas prts);
+
+fun str_list lpar rpar strs =
+ list lpar rpar (map str strs);
+
+fun big_list name prts =
+ block (fbreaks (str name :: prts));
+
+
+
+(*** Pretty printing with depth limitation ***)
+
+val depth = ref 0; (*maximum depth; 0 means no limit*)
+
+fun setdepth dp = (depth := dp);
+
+(*Recursively prune blocks, discarding all text exceeding depth dp*)
+fun pruning dp (Block(bes,indent,wd)) =
+ if dp>0 then blk(indent, map (pruning(dp-1)) bes)
+ else str "..."
+ | pruning dp e = e;
+
+fun prune dp e = if dp>0 then pruning dp e else e;
+
+
+fun string_of e = #tx (format ([prune (!depth) e], 0, 0) emptytext);
+
+val writeln = writeln o string_of;
+
+
+(*Create a single flat string: no line breaking*)
+fun str_of prt =
+ let
+ fun s_of (Block (prts, _, _)) = implode (map s_of prts)
+ | s_of (String (s, _)) = s
+ | s_of (Break (false, wd)) = repstring " " wd
+ | s_of (Break (true, _)) = " ";
+ in
+ s_of (prune (! depth) prt)
+ end;
+
+(*Part of the interface to the Poly/ML and New Jersey ML pretty printers*)
+fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
+ let
+ fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
+ | pp (String (s, _)) = put_str s
+ | pp (Break (false, wd)) = put_brk wd
+ | pp (Break (true, _)) = put_fbrk ()
+ and pp_lst [] = ()
+ | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
+ in
+ pp (prune (! depth) prt)
+ end;
+
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/scan.ML Wed Jan 13 12:44:33 1999 +0100
@@ -0,0 +1,305 @@
+(* Title: Pure/Syntax/scan.ML
+ ID: $Id$
+ Author: Markus Wenzel and Tobias Nipkow, TU Muenchen
+
+Generic scanners (for potentially infinite input).
+*)
+
+infix 5 -- :-- |-- --| ^^;
+infix 3 >>;
+infix 0 ||;
+
+signature BASIC_SCAN =
+sig
+ val !! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b
+ val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
+ val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
+ val -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
+ val :-- : ('a -> 'b * 'c) * ('b -> 'c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
+ val |-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e
+ val --| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e
+ val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c
+ val $$ : ''a -> ''a list -> ''a * ''a list
+end;
+
+signature SCAN =
+sig
+ include BASIC_SCAN
+ val fail: 'a -> 'b
+ val fail_with: ('a -> string) -> 'a -> 'b
+ val succeed: 'a -> 'b -> 'a * 'b
+ val one: ('a -> bool) -> 'a list -> 'a * 'a list
+ val any: ('a -> bool) -> 'a list -> 'a list * 'a list
+ val any1: ('a -> bool) -> 'a list -> 'a list * 'a list
+ val optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a
+ val option: ('a -> 'b * 'a) -> 'a -> 'b option * 'a
+ val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
+ val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
+ val max: ('a * 'a -> bool) -> ('b -> 'a * 'b) -> ('b -> 'a * 'b) -> 'b -> 'a * 'b
+ val ahead: ('a -> 'b * 'c) -> 'a -> 'b * 'a
+ val unless: ('a -> 'b * 'a) -> ('a -> 'c * 'd) -> 'a -> 'c * 'd
+ val first: ('a -> 'b) list -> 'a -> 'b
+ val depend: ('a -> 'b -> ('c * 'd) * 'e) -> 'a * 'b -> 'd * ('c * 'e)
+ val lift: ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c)
+ val pass: 'a -> ('a * 'b -> 'c * ('d * 'e)) -> 'b -> 'c * 'e
+ val try: ('a -> 'b) -> 'a -> 'b
+ val force: ('a -> 'b) -> 'a -> 'b
+ val prompt: string -> ('a -> 'b) -> 'a -> 'b
+ val finite': 'a * ('a -> bool) -> ('b * 'a list -> 'c * ('d * 'a list))
+ -> 'b * 'a list -> 'c * ('d * 'a list)
+ val finite: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b * 'a list
+ val read: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b option
+ val catch: ('a -> 'b) -> 'a -> 'b
+ val error: ('a -> 'b) -> 'a -> 'b
+ val source': string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
+ 'b * ('b -> bool) -> ('d * 'b list -> 'e list * ('d * 'b list)) ->
+ ('d * 'b list -> 'f * ('d * 'b list)) option -> 'd * 'a -> 'e list * ('d * 'c)
+ val source: string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
+ 'b * ('b -> bool) -> ('b list -> 'd list * 'b list) ->
+ ('b list -> 'e * 'b list) option -> 'a -> 'd list * 'c
+ val single: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
+ val bulk: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
+ type lexicon
+ val dest_lexicon: lexicon -> string list list
+ val make_lexicon: string list list -> lexicon
+ val empty_lexicon: lexicon
+ val extend_lexicon: lexicon -> string list list -> lexicon
+ val merge_lexicons: lexicon -> lexicon -> lexicon
+ val literal: lexicon -> string list -> string list * string list
+end;
+
+structure Scan: SCAN =
+struct
+
+
+(** scanners **)
+
+exception MORE of string option; (*need more input (prompt)*)
+exception FAIL of string option; (*try alternatives (reason of failure)*)
+exception ABORT of string; (*dead end*)
+
+
+(* scanner combinators *)
+
+fun (scan >> f) xs = apfst f (scan xs);
+
+fun (scan1 || scan2) xs = scan1 xs handle FAIL _ => scan2 xs;
+
+(*dependent pairing*)
+fun (scan1 :-- scan2) xs =
+ let
+ val (x, ys) = scan1 xs;
+ val (y, zs) = scan2 x ys;
+ in ((x, y), zs) end;
+
+fun (scan1 -- scan2) = scan1 :-- (fn _ => scan2);
+fun (scan1 |-- scan2) = scan1 -- scan2 >> #2;
+fun (scan1 --| scan2) = scan1 -- scan2 >> #1;
+fun (scan1 ^^ scan2) = scan1 -- scan2 >> op ^;
+
+
+(* generic scanners *)
+
+fun fail _ = raise FAIL None;
+fun fail_with msg_of xs = raise FAIL (Some (msg_of xs));
+fun succeed y xs = (y, xs);
+
+fun one _ [] = raise MORE None
+ | one pred (x :: xs) =
+ if pred x then (x, xs) else raise FAIL None;
+
+fun $$ _ [] = raise MORE None
+ | $$ a (x :: xs) =
+ if a = x then (x, xs) else raise FAIL None;
+
+fun any _ [] = raise MORE None
+ | any pred (lst as x :: xs) =
+ if pred x then apfst (cons x) (any pred xs)
+ else ([], lst);
+
+fun any1 pred = one pred -- any pred >> op ::;
+
+fun optional scan def = scan || succeed def;
+fun option scan = optional (scan >> Some) None;
+
+fun repeat scan xs = (scan -- repeat scan >> op :: || succeed []) xs;
+fun repeat1 scan = scan -- repeat scan >> op ::;
+
+fun max leq scan1 scan2 xs =
+ (case (option scan1 xs, option scan2 xs) of
+ ((None, _), (None, _)) => raise FAIL None (*looses FAIL msg!*)
+ | ((Some tok1, xs'), (None, _)) => (tok1, xs')
+ | ((None, _), (Some tok2, xs')) => (tok2, xs')
+ | ((Some tok1, xs1'), (Some tok2, xs2')) =>
+ if leq (tok2, tok1) then (tok1, xs1') else (tok2, xs2'));
+
+fun ahead scan xs = (fst (scan xs), xs);
+
+fun unless test scan =
+ ahead (option test) :-- (fn None => scan | _ => fail) >> #2;
+
+fun first [] = fail
+ | first (scan :: scans) = scan || first scans;
+
+
+(* state based scanners *)
+
+fun depend scan (st, xs) =
+ let val ((st', y), xs') = scan st xs
+ in (y, (st', xs')) end;
+
+fun lift scan (st, xs) =
+ let val (y, xs') = scan xs
+ in (y, (st, xs')) end;
+
+fun pass st scan xs =
+ let val (y, (_, xs')) = scan (st, xs)
+ in (y, xs') end;
+
+
+(* exception handling *)
+
+fun !! err scan xs = scan xs handle FAIL msg => raise ABORT (err (xs, msg));
+fun try scan xs = scan xs handle MORE _ => raise FAIL None | ABORT _ => raise FAIL None;
+fun force scan xs = scan xs handle MORE _ => raise FAIL None;
+fun prompt str scan xs = scan xs handle MORE None => raise MORE (Some str);
+fun catch scan xs = scan xs handle ABORT msg => raise FAIL (Some msg);
+fun error scan xs = scan xs handle ABORT msg => Library.error msg;
+
+
+(* finite scans *)
+
+fun finite' (stopper, is_stopper) scan (state, input) =
+ let
+ fun lost () = raise ABORT "Scanner bug: lost stopper of finite scan!";
+
+ fun stop [] = lost ()
+ | stop lst =
+ let val (xs, x) = split_last lst
+ in if is_stopper x then ((), xs) else lost () end;
+ in
+ if exists is_stopper input then
+ raise ABORT "Stopper may not occur in input of finite scan!"
+ else (force scan --| lift stop) (state, input @ [stopper])
+ end;
+
+fun finite stopper scan xs =
+ let val (y, ((), xs')) = finite' stopper (lift scan) ((), xs)
+ in (y, xs') end;
+
+fun read stopper scan xs =
+ (case error (finite stopper (option scan)) xs of
+ (y as Some _, []) => y
+ | _ => None);
+
+
+
+(* infinite scans -- draining state-based source *)
+
+fun drain def_prmpt get stopper scan ((state, xs), src) =
+ (scan (state, xs), src) handle MORE prmpt =>
+ (case get (if_none prmpt def_prmpt) src of
+ ([], _) => (finite' stopper scan (state, xs), src)
+ | (xs', src') => drain def_prmpt get stopper scan ((state, xs @ xs'), src'));
+
+fun source' def_prmpt get unget stopper scanner opt_recover (state, src) =
+ let
+ fun drain_with scan = drain def_prmpt get stopper scan;
+
+ fun drain_loop recover inp =
+ drain_with (catch scanner) inp handle FAIL msg =>
+ (error_msg (if_none msg "Syntax error.");
+ drain_loop recover (apfst snd (drain_with recover inp)));
+
+ val ((ys, (state', xs')), src') =
+ (case (get def_prmpt src, opt_recover) of
+ (([], s), _) => (([], (state, [])), s)
+ | ((xs, s), None) => drain_with (error scanner) ((state, xs), s)
+ | ((xs, s), Some scan) => drain_loop scan ((state, xs), s));
+ in
+ (ys, (state', unget (xs', src')))
+ end;
+
+fun source def_prmpt get unget stopper scan opt_recover src =
+ let val (ys, ((), src')) =
+ source' def_prmpt get unget stopper (lift scan) (apsome lift opt_recover) ((), src)
+ in (ys, src') end;
+
+fun single scan = scan >> (fn x => [x]);
+fun bulk scan = scan -- repeat (try scan) >> (op ::);
+
+
+
+(** datatype lexicon **)
+
+datatype lexicon =
+ Empty |
+ Branch of string * string list * lexicon * lexicon * lexicon;
+
+val no_literal = [];
+
+
+(* dest_lexicon *)
+
+fun dest_lexicon Empty = []
+ | dest_lexicon (Branch (_, [], lt, eq, gt)) =
+ dest_lexicon lt @ dest_lexicon eq @ dest_lexicon gt
+ | dest_lexicon (Branch (_, cs, lt, eq, gt)) =
+ dest_lexicon lt @ [cs] @ dest_lexicon eq @ dest_lexicon gt;
+
+
+(* empty, extend, make, merge lexicons *)
+
+val empty_lexicon = Empty;
+
+fun extend_lexicon lexicon chrss =
+ let
+ fun ext (lex, chrs) =
+ let
+ fun add (Branch (d, a, lt, eq, gt)) (chs as c :: cs) =
+ if c < d then Branch (d, a, add lt chs, eq, gt)
+ else if c > d then Branch (d, a, lt, eq, add gt chs)
+ else Branch (d, if null cs then chrs else a, lt, add eq cs, gt)
+ | add Empty [c] =
+ Branch (c, chrs, Empty, Empty, Empty)
+ | add Empty (c :: cs) =
+ Branch (c, no_literal, Empty, add Empty cs, Empty)
+ | add lex [] = lex;
+ in add lex chrs end;
+ in foldl ext (lexicon, chrss \\ dest_lexicon lexicon) end;
+
+val make_lexicon = extend_lexicon empty_lexicon;
+
+fun merge_lexicons lex1 lex2 =
+ let
+ val chss1 = dest_lexicon lex1;
+ val chss2 = dest_lexicon lex2;
+ in
+ if chss2 subset chss1 then lex1
+ else if chss1 subset chss2 then lex2
+ else extend_lexicon lex1 chss2
+ end;
+
+
+(* scan literal *)
+
+fun literal lex chrs =
+ let
+ fun lit Empty res _ = res
+ | lit (Branch _) _ [] = raise MORE None
+ | lit (Branch (d, a, lt, eq, gt)) res (chs as c :: cs) =
+ if c < d then lit lt res chs
+ else if c > d then lit gt res chs
+ else lit eq (if a = no_literal then res else Some (a, cs)) cs;
+ in
+ (case lit lex None chrs of
+ None => raise FAIL None
+ | Some res => res)
+ end;
+
+
+end;
+
+
+structure BasicScan: BASIC_SCAN = Scan;
+open BasicScan;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/source.ML Wed Jan 13 12:44:33 1999 +0100
@@ -0,0 +1,150 @@
+(* Title: Pure/Syntax/source.ML
+ ID: $Id$
+ Author: Markus Wenzel, TU Muenchen
+
+Co-algebraic data sources.
+*)
+
+signature SOURCE =
+sig
+ type ('a, 'b) source
+ val set_prompt: string -> ('a, 'b) source -> ('a, 'b) source
+ val get: ('a, 'b) source -> 'a list * ('a, 'b) source
+ val unget: 'a list * ('a, 'b) source -> ('a, 'b) source
+ val get_single: ('a, 'b) source -> ('a * ('a, 'b) source) option
+ val exhaust: ('a, 'b) source -> 'a list
+ val mapfilter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) source) source
+ val filter: ('a -> bool) -> ('a, 'b) source -> ('a, ('a, 'b) source) source
+ val of_list: 'a list -> ('a, 'a list) source
+ val of_string: string -> (string, string list) source
+ val of_file: string -> (string, string list) source
+ val decorate_prompt_fn: (string -> string) ref
+ val of_stream: TextIO.instream -> TextIO.outstream -> (string, unit) source
+ val tty: (string, unit) source
+ val source': 'a -> 'b * ('b -> bool) -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
+ ('a * 'b list -> 'd * ('a * 'b list)) option ->
+ ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source
+ val source: 'a * ('a -> bool) -> ('a list -> 'b list * 'a list) ->
+ ('a list -> 'c * 'a list) option ->
+ ('a, 'd) source -> ('b, ('a, 'd) source) source
+end;
+
+structure Source: SOURCE =
+struct
+
+
+(** datatype source **)
+
+datatype ('a, 'b) source =
+ Source of
+ {buffer: 'a list,
+ info: 'b,
+ prompt: string,
+ drain: string -> 'b -> 'a list * 'b};
+
+fun make_source buffer info prompt drain =
+ Source {buffer = buffer, info = info, prompt = prompt, drain = drain};
+
+
+(* prompt *)
+
+val default_prompt = "> ";
+
+fun set_prompt prompt (Source {buffer, info, prompt = _, drain}) =
+ make_source buffer info prompt drain;
+
+
+(* get / unget *)
+
+fun get (Source {buffer = [], info, prompt, drain}) =
+ let val (xs, info') = drain prompt info
+ in (xs, make_source [] info' prompt drain) end
+ | get (Source {buffer, info, prompt, drain}) =
+ (buffer, make_source [] info prompt drain);
+
+fun unget (xs, Source {buffer, info, prompt, drain}) =
+ make_source (xs @ buffer) info prompt drain;
+
+
+(* variations on get *)
+
+fun get_prompt prompt src = get (set_prompt prompt src);
+
+fun get_single src =
+ (case get src of
+ ([], _) => None
+ | (x :: xs, src') => Some (x, unget (xs, src')));
+
+fun exhaust src =
+ (case get src of
+ ([], _) => []
+ | (xs, src') => xs @ exhaust src');
+
+
+(* (map)filter *)
+
+fun drain_mapfilter f prompt src =
+ let
+ val (xs, src') = get_prompt prompt src;
+ val xs' = Library.mapfilter f xs;
+ in
+ if null xs orelse not (null xs') then (xs', src')
+ else drain_mapfilter f prompt src'
+ end;
+
+fun mapfilter f src = make_source [] src default_prompt (drain_mapfilter f);
+fun filter pred = mapfilter (fn x => if pred x then Some x else None);
+
+
+
+(** build sources **)
+
+(* list source *)
+
+(*limiting the input buffer considerably improves performance*)
+val limit = 4000;
+
+fun drain_list _ xs = (take (limit, xs), drop (limit, xs));
+
+fun of_list xs = make_source [] xs default_prompt drain_list;
+val of_string = of_list o explode;
+val of_file = of_string o File.read;
+
+
+(* stream source *)
+
+val decorate_prompt_fn = ref (fn s:string => s);
+
+fun drain_stream instream outstream prompt () =
+ (TextIO.output (outstream, ! decorate_prompt_fn prompt);
+ TextIO.flushOut outstream;
+ (explode (TextIO.inputLine instream), ()));
+
+fun of_stream instream outstream =
+ make_source [] () default_prompt (drain_stream instream outstream);
+
+val tty = of_stream TextIO.stdIn TextIO.stdOut;
+
+
+
+(** compose sources **)
+
+fun drain_source source stopper scan recover prompt src =
+ source prompt get_prompt unget stopper scan recover src;
+
+
+(* state-based *)
+
+fun source' init_state stopper scan recover src =
+ make_source [] (init_state, src) default_prompt
+ (drain_source Scan.source' stopper scan recover);
+
+
+(* non state-based *)
+
+fun source stopper scan recover src =
+ make_source [] src default_prompt
+ (drain_source Scan.source stopper scan recover);
+
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/symbol.ML Wed Jan 13 12:44:33 1999 +0100
@@ -0,0 +1,274 @@
+(* Title: Pure/Syntax/symbol.ML
+ ID: $Id$
+ Author: Markus Wenzel, TU Muenchen
+
+Generalized characters.
+*)
+
+signature SYMBOL =
+sig
+ type symbol
+ val space: symbol
+ val eof: symbol
+ val is_eof: symbol -> bool
+ val not_eof: symbol -> bool
+ val stopper: symbol * (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 beginning: symbol list -> string
+ val scan: string list -> symbol * string list
+ val explode: string -> symbol list
+ val length: symbol list -> int
+ val size: string -> int
+ val input: string -> string
+ val output: string -> string
+ val source: bool -> (string, 'a) Source.source ->
+ (symbol, (string, 'a) Source.source) Source.source
+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;
+
+val space = " ";
+val eof = "";
+
+
+(* kinds *)
+
+fun is_eof s = s = eof;
+fun not_eof s = s <> eof;
+val stopper = (eof, is_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
+ | "\160" => true | "\\<space2>" => true
+ | _ => false;
+
+val is_letdig = is_quasi_letter orf is_digit;
+
+fun is_printable s =
+ size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" orelse
+ size s > 2 andalso nth_elem (2, explode s) <> "^";
+
+
+(* beginning *)
+
+val smash_blanks = map (fn s => if is_blank s then space else s);
+
+fun beginning raw_ss =
+ let
+ val (all_ss, _) = take_suffix is_blank raw_ss;
+ val dots = if length all_ss > 10 then " ..." else "";
+ val (ss, _) = take_suffix is_blank (take (10, all_ss));
+ in implode (smash_blanks ss) ^ dots end;
+
+
+(* 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;
+
+
+(* source *)
+
+val recover = Scan.any1 ((not o is_blank) andf not_eof);
+
+fun source do_recover src =
+ Source.source stopper (Scan.bulk scan) (if do_recover then Some recover else None) src;
+
+
+(* 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 (the (Scan.read stopper (Scan.repeat scan) chs))
+ end;
+
+
+(* printable length *)
+
+fun sym_length ss = foldl (fn (n, c) => if is_printable c then n + 1 else n) (0, ss);
+val sym_size = sym_length o sym_explode;
+
+
+(* 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 declarations of this structure!*)
+val explode = sym_explode;
+val length = sym_length;
+val size = sym_size;
+
+
+end;
--- a/src/Pure/IsaMakefile Wed Jan 13 12:16:34 1999 +0100
+++ b/src/Pure/IsaMakefile Wed Jan 13 12:44:33 1999 +0100
@@ -25,7 +25,8 @@
$(OUT)/Pure: General/ROOT.ML General/file.ML General/history.ML \
General/name_space.ML General/object.ML General/path.ML \
- General/position.ML General/seq.ML General/table.ML Isar/ROOT.ML \
+ General/position.ML General/pretty.ML General/scan.ML General/seq.ML \
+ General/source.ML General/symbol.ML General/table.ML Isar/ROOT.ML \
Isar/args.ML Isar/attrib.ML Isar/isar.ML Isar/isar_cmd.ML \
Isar/isar_syn.ML Isar/isar_thy.ML Isar/method.ML Isar/outer_lex.ML \
Isar/outer_parse.ML Isar/outer_syntax.ML Isar/proof.ML \
@@ -33,12 +34,11 @@
Isar/toplevel.ML ML-Systems/mlworks.ML ML-Systems/polyml.ML \
ML-Systems/smlnj-0.93.ML ML-Systems/smlnj.ML ROOT.ML Syntax/ROOT.ML \
Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \
- Syntax/pretty.ML Syntax/printer.ML Syntax/scan.ML Syntax/source.ML \
- Syntax/symbol.ML Syntax/syn_ext.ML Syntax/syn_trans.ML \
- Syntax/syntax.ML Syntax/token_trans.ML Syntax/type_ext.ML \
- Thy/ROOT.ML Thy/browser_info.ML Thy/context.ML Thy/thm_database.ML \
- Thy/thy_info.ML Thy/thy_parse.ML Thy/thy_read.ML Thy/thy_scan.ML \
- Thy/thy_syn.ML Thy/use.ML axclass.ML basis.ML deriv.ML display.ML \
+ Syntax/printer.ML Syntax/syn_ext.ML Syntax/syn_trans.ML \
+ Syntax/syntax.ML Syntax/token_trans.ML Syntax/type_ext.ML Thy/ROOT.ML \
+ Thy/browser_info.ML Thy/context.ML Thy/thm_database.ML Thy/thy_info.ML \
+ Thy/thy_parse.ML Thy/thy_read.ML Thy/thy_scan.ML Thy/thy_syn.ML \
+ Thy/use.ML axclass.ML basis.ML deriv.ML display.ML \
drule.ML envir.ML goals.ML install_pp.ML library.ML locale.ML \
logic.ML net.ML object_logic.ML pattern.ML pure.ML pure_thy.ML \
search.ML sign.ML sorts.ML tactic.ML tctical.ML term.ML theory.ML \
--- a/src/Pure/Syntax/README Wed Jan 13 12:16:34 1999 +0100
+++ b/src/Pure/Syntax/README Wed Jan 13 12:44:33 1999 +0100
@@ -4,12 +4,7 @@
This directory contains the source files for Isabelle's syntax module,
which includes a lexer, parser, pretty printer and macro system. Note
-that only the following structures are supposed to be exported:
-
- Pretty (generic pretty printing module)
- Scan (generic scanner toolbox)
- Source (co-algebraic data sources)
- Symbol (generalized characters)
+that only the following structures are exported:
Syntax (internal interface to the syntax module)
BasicSyntax (part of Syntax made pervasive)
--- a/src/Pure/Syntax/ROOT.ML Wed Jan 13 12:16:34 1999 +0100
+++ b/src/Pure/Syntax/ROOT.ML Wed Jan 13 12:44:33 1999 +0100
@@ -5,13 +5,6 @@
This file builds the syntax module.
*)
-(*generic modules*)
-use "scan.ML";
-use "source.ML";
-use "symbol.ML";
-use "pretty.ML";
-
-(*actual syntax module*)
use "lexicon.ML";
use "token_trans.ML";
use "ast.ML";
--- a/src/Pure/Syntax/pretty.ML Wed Jan 13 12:16:34 1999 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,249 +0,0 @@
-(* Title: Pure/Syntax/pretty.ML
- ID: $Id$
- Author: Lawrence C Paulson
- Copyright 1991 University of Cambridge
-
-Generic pretty printing module.
-
-Loosely based on
- D. C. Oppen, "Pretty Printing",
- ACM Transactions on Programming Languages and Systems (1980), 465-483.
-
-The object to be printed is given as a tree with indentation and line
-breaking information. A "break" inserts a newline if the text until
-the next break is too long to fit on the current line. After the newline,
-text is indented to the level of the enclosing block. Normally, if a block
-is broken then all enclosing blocks will also be broken. Only "inconsistent
-breaks" are provided.
-
-The stored length of a block is used in breakdist (to treat each inner block as
-a unit for breaking).
-*)
-
-type pprint_args = (string -> unit) * (int -> unit) * (int -> unit) *
- (unit -> unit) * (unit -> unit);
-
-signature PRETTY =
- sig
- type T
- val str: string -> T
- val strlen: string -> int -> T
- val sym: string -> T
- val spc: int -> T
- val brk: int -> T
- val fbrk: T
- val blk: int * T list -> T
- val lst: string * string -> T list -> T
- val quote: T -> T
- val commas: T list -> T list
- val breaks: T list -> T list
- val fbreaks: T list -> T list
- val block: T list -> T
- val strs: string list -> T
- val enclose: string -> string -> T list -> T
- val list: string -> string -> T list -> T
- val str_list: string -> string -> string list -> T
- val big_list: string -> T list -> T
- val string_of: T -> string
- val writeln: T -> unit
- val str_of: T -> string
- val pprint: T -> pprint_args -> unit
- val setdepth: int -> unit
- val setmargin: int -> unit
- end;
-
-structure Pretty : PRETTY =
-struct
-
-(*printing items: compound phrases, strings, and breaks*)
-datatype T =
- Block of T list * int * int | (*body, indentation, length*)
- String of string * int | (*text, length*)
- Break of bool * int; (*mandatory flag, width if not taken*);
-
-(*Add the lengths of the expressions until the next Break; if no Break then
- include "after", to account for text following this block. *)
-fun breakdist (Block(_,_,len)::es, after) = len + breakdist(es, after)
- | breakdist (String (s, len) :: es, after) = len + breakdist (es, after)
- | breakdist (Break _ :: es, after) = 0
- | breakdist ([], after) = after;
-
-fun repstring a 0 = ""
- | repstring a 1 = a
- | repstring a k =
- if k mod 2 = 0 then repstring(a^a) (k div 2)
- else repstring(a^a) (k div 2) ^ a;
-
-(*** Type for lines of text: string, # of lines, position on line ***)
-
-type text = {tx: string, nl: int, pos: int};
-
-val emptytext = {tx="", nl=0, pos=0};
-
-fun blanks wd {tx,nl,pos} =
- {tx = tx ^ repstring " " wd,
- nl = nl,
- pos = pos+wd};
-
-fun newline {tx,nl,pos} =
- {tx = tx ^ "\n",
- nl = nl+1,
- pos = 0};
-
-fun string s len {tx,nl,pos:int} =
- {tx = tx ^ s,
- nl = nl,
- pos = pos + len};
-
-
-(*** Formatting ***)
-
-(* margin *)
-
-(*example values*)
-val margin = ref 80 (*right margin, or page width*)
-and breakgain = ref 4 (*minimum added space required of a break*)
-and emergencypos = ref 40; (*position too far to right*)
-
-fun setmargin m =
- (margin := m;
- breakgain := !margin div 20;
- emergencypos := !margin div 2);
-
-val () = setmargin 76;
-
-
-(*Search for the next break (at this or higher levels) and force it to occur*)
-fun forcenext [] = []
- | forcenext (Break(_,wd) :: es) = Break(true,0) :: es
- | forcenext (e :: es) = e :: forcenext es;
-
-(*es is list of expressions to print;
- blockin is the indentation of the current block;
- after is the width of the following context until next break. *)
-fun format ([], _, _) text = text
- | format (e::es, blockin, after) (text as {pos,nl,...}) =
- (case e of
- Block(bes,indent,wd) =>
- let val blockin' = (pos + indent) mod !emergencypos
- val btext = format(bes, blockin', breakdist(es,after)) text
- (*If this block was broken then force the next break.*)
- val es2 = if nl < #nl(btext) then forcenext es else es
- in format (es2,blockin,after) btext end
- | String (s, len) => format (es,blockin,after) (string s len text)
- | Break(force,wd) => (*no break if text to next break fits on this line
- or if breaking would add only breakgain to space *)
- format (es,blockin,after)
- (if not force andalso
- pos+wd <= Int.max(!margin - breakdist(es,after),
- blockin + !breakgain)
- then blanks wd text (*just insert wd blanks*)
- else blanks blockin (newline text)));
-
-
-(*** Exported functions to create formatting expressions ***)
-
-fun length (Block (_, _, len)) = len
- | length (String (_, len)) = len
- | length (Break(_, wd)) = wd;
-
-fun str s = String (s, size s);
-fun strlen s len = String (s, len);
-fun sym s = String (s, Symbol.size s);
-
-fun spc n = str (repstring " " n);
-
-fun brk wd = Break (false, wd);
-val fbrk = Break (true, 0);
-
-fun blk (indent, es) =
- let
- fun sum([], k) = k
- | sum(e :: es, k) = sum (es, length e + k);
- in Block (es, indent, sum (es, 0)) end;
-
-(*Join the elements of es as a comma-separated list, bracketted by lp and rp*)
-fun lst(lp,rp) es =
- let fun add(e,es) = str"," :: brk 1 :: e :: es;
- fun list(e :: (es as _::_)) = str lp :: e :: foldr add (es,[str rp])
- | list(e::[]) = [str lp, e, str rp]
- | list([]) = []
- in blk(size lp, list es) end;
-
-
-(* utils *)
-
-fun quote prt =
- blk (1, [str "\"", prt, str "\""]);
-
-fun commas prts =
- flat (separate [str ",", brk 1] (map (fn x => [x]) prts));
-
-fun breaks prts = separate (brk 1) prts;
-
-fun fbreaks prts = separate fbrk prts;
-
-fun block prts = blk (2, prts);
-
-val strs = block o breaks o (map str);
-
-fun enclose lpar rpar prts =
- block (str lpar :: (prts @ [str rpar]));
-
-fun list lpar rpar prts =
- enclose lpar rpar (commas prts);
-
-fun str_list lpar rpar strs =
- list lpar rpar (map str strs);
-
-fun big_list name prts =
- block (fbreaks (str name :: prts));
-
-
-
-(*** Pretty printing with depth limitation ***)
-
-val depth = ref 0; (*maximum depth; 0 means no limit*)
-
-fun setdepth dp = (depth := dp);
-
-(*Recursively prune blocks, discarding all text exceeding depth dp*)
-fun pruning dp (Block(bes,indent,wd)) =
- if dp>0 then blk(indent, map (pruning(dp-1)) bes)
- else str "..."
- | pruning dp e = e;
-
-fun prune dp e = if dp>0 then pruning dp e else e;
-
-
-fun string_of e = #tx (format ([prune (!depth) e], 0, 0) emptytext);
-
-val writeln = writeln o string_of;
-
-
-(*Create a single flat string: no line breaking*)
-fun str_of prt =
- let
- fun s_of (Block (prts, _, _)) = implode (map s_of prts)
- | s_of (String (s, _)) = s
- | s_of (Break (false, wd)) = repstring " " wd
- | s_of (Break (true, _)) = " ";
- in
- s_of (prune (! depth) prt)
- end;
-
-(*Part of the interface to the Poly/ML and New Jersey ML pretty printers*)
-fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
- let
- fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
- | pp (String (s, _)) = put_str s
- | pp (Break (false, wd)) = put_brk wd
- | pp (Break (true, _)) = put_fbrk ()
- and pp_lst [] = ()
- | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
- in
- pp (prune (! depth) prt)
- end;
-
-
-end;
--- a/src/Pure/Syntax/scan.ML Wed Jan 13 12:16:34 1999 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,305 +0,0 @@
-(* Title: Pure/Syntax/scan.ML
- ID: $Id$
- Author: Markus Wenzel and Tobias Nipkow, TU Muenchen
-
-Generic scanners (for potentially infinite input).
-*)
-
-infix 5 -- :-- |-- --| ^^;
-infix 3 >>;
-infix 0 ||;
-
-signature BASIC_SCAN =
-sig
- val !! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b
- val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
- val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
- val -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
- val :-- : ('a -> 'b * 'c) * ('b -> 'c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
- val |-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e
- val --| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e
- val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c
- val $$ : ''a -> ''a list -> ''a * ''a list
-end;
-
-signature SCAN =
-sig
- include BASIC_SCAN
- val fail: 'a -> 'b
- val fail_with: ('a -> string) -> 'a -> 'b
- val succeed: 'a -> 'b -> 'a * 'b
- val one: ('a -> bool) -> 'a list -> 'a * 'a list
- val any: ('a -> bool) -> 'a list -> 'a list * 'a list
- val any1: ('a -> bool) -> 'a list -> 'a list * 'a list
- val optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a
- val option: ('a -> 'b * 'a) -> 'a -> 'b option * 'a
- val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
- val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
- val max: ('a * 'a -> bool) -> ('b -> 'a * 'b) -> ('b -> 'a * 'b) -> 'b -> 'a * 'b
- val ahead: ('a -> 'b * 'c) -> 'a -> 'b * 'a
- val unless: ('a -> 'b * 'a) -> ('a -> 'c * 'd) -> 'a -> 'c * 'd
- val first: ('a -> 'b) list -> 'a -> 'b
- val depend: ('a -> 'b -> ('c * 'd) * 'e) -> 'a * 'b -> 'd * ('c * 'e)
- val lift: ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c)
- val pass: 'a -> ('a * 'b -> 'c * ('d * 'e)) -> 'b -> 'c * 'e
- val try: ('a -> 'b) -> 'a -> 'b
- val force: ('a -> 'b) -> 'a -> 'b
- val prompt: string -> ('a -> 'b) -> 'a -> 'b
- val finite': 'a * ('a -> bool) -> ('b * 'a list -> 'c * ('d * 'a list))
- -> 'b * 'a list -> 'c * ('d * 'a list)
- val finite: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b * 'a list
- val read: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b option
- val catch: ('a -> 'b) -> 'a -> 'b
- val error: ('a -> 'b) -> 'a -> 'b
- val source': string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
- 'b * ('b -> bool) -> ('d * 'b list -> 'e list * ('d * 'b list)) ->
- ('d * 'b list -> 'f * ('d * 'b list)) option -> 'd * 'a -> 'e list * ('d * 'c)
- val source: string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
- 'b * ('b -> bool) -> ('b list -> 'd list * 'b list) ->
- ('b list -> 'e * 'b list) option -> 'a -> 'd list * 'c
- val single: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
- val bulk: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
- type lexicon
- val dest_lexicon: lexicon -> string list list
- val make_lexicon: string list list -> lexicon
- val empty_lexicon: lexicon
- val extend_lexicon: lexicon -> string list list -> lexicon
- val merge_lexicons: lexicon -> lexicon -> lexicon
- val literal: lexicon -> string list -> string list * string list
-end;
-
-structure Scan: SCAN =
-struct
-
-
-(** scanners **)
-
-exception MORE of string option; (*need more input (prompt)*)
-exception FAIL of string option; (*try alternatives (reason of failure)*)
-exception ABORT of string; (*dead end*)
-
-
-(* scanner combinators *)
-
-fun (scan >> f) xs = apfst f (scan xs);
-
-fun (scan1 || scan2) xs = scan1 xs handle FAIL _ => scan2 xs;
-
-(*dependent pairing*)
-fun (scan1 :-- scan2) xs =
- let
- val (x, ys) = scan1 xs;
- val (y, zs) = scan2 x ys;
- in ((x, y), zs) end;
-
-fun (scan1 -- scan2) = scan1 :-- (fn _ => scan2);
-fun (scan1 |-- scan2) = scan1 -- scan2 >> #2;
-fun (scan1 --| scan2) = scan1 -- scan2 >> #1;
-fun (scan1 ^^ scan2) = scan1 -- scan2 >> op ^;
-
-
-(* generic scanners *)
-
-fun fail _ = raise FAIL None;
-fun fail_with msg_of xs = raise FAIL (Some (msg_of xs));
-fun succeed y xs = (y, xs);
-
-fun one _ [] = raise MORE None
- | one pred (x :: xs) =
- if pred x then (x, xs) else raise FAIL None;
-
-fun $$ _ [] = raise MORE None
- | $$ a (x :: xs) =
- if a = x then (x, xs) else raise FAIL None;
-
-fun any _ [] = raise MORE None
- | any pred (lst as x :: xs) =
- if pred x then apfst (cons x) (any pred xs)
- else ([], lst);
-
-fun any1 pred = one pred -- any pred >> op ::;
-
-fun optional scan def = scan || succeed def;
-fun option scan = optional (scan >> Some) None;
-
-fun repeat scan xs = (scan -- repeat scan >> op :: || succeed []) xs;
-fun repeat1 scan = scan -- repeat scan >> op ::;
-
-fun max leq scan1 scan2 xs =
- (case (option scan1 xs, option scan2 xs) of
- ((None, _), (None, _)) => raise FAIL None (*looses FAIL msg!*)
- | ((Some tok1, xs'), (None, _)) => (tok1, xs')
- | ((None, _), (Some tok2, xs')) => (tok2, xs')
- | ((Some tok1, xs1'), (Some tok2, xs2')) =>
- if leq (tok2, tok1) then (tok1, xs1') else (tok2, xs2'));
-
-fun ahead scan xs = (fst (scan xs), xs);
-
-fun unless test scan =
- ahead (option test) :-- (fn None => scan | _ => fail) >> #2;
-
-fun first [] = fail
- | first (scan :: scans) = scan || first scans;
-
-
-(* state based scanners *)
-
-fun depend scan (st, xs) =
- let val ((st', y), xs') = scan st xs
- in (y, (st', xs')) end;
-
-fun lift scan (st, xs) =
- let val (y, xs') = scan xs
- in (y, (st, xs')) end;
-
-fun pass st scan xs =
- let val (y, (_, xs')) = scan (st, xs)
- in (y, xs') end;
-
-
-(* exception handling *)
-
-fun !! err scan xs = scan xs handle FAIL msg => raise ABORT (err (xs, msg));
-fun try scan xs = scan xs handle MORE _ => raise FAIL None | ABORT _ => raise FAIL None;
-fun force scan xs = scan xs handle MORE _ => raise FAIL None;
-fun prompt str scan xs = scan xs handle MORE None => raise MORE (Some str);
-fun catch scan xs = scan xs handle ABORT msg => raise FAIL (Some msg);
-fun error scan xs = scan xs handle ABORT msg => Library.error msg;
-
-
-(* finite scans *)
-
-fun finite' (stopper, is_stopper) scan (state, input) =
- let
- fun lost () = raise ABORT "Scanner bug: lost stopper of finite scan!";
-
- fun stop [] = lost ()
- | stop lst =
- let val (xs, x) = split_last lst
- in if is_stopper x then ((), xs) else lost () end;
- in
- if exists is_stopper input then
- raise ABORT "Stopper may not occur in input of finite scan!"
- else (force scan --| lift stop) (state, input @ [stopper])
- end;
-
-fun finite stopper scan xs =
- let val (y, ((), xs')) = finite' stopper (lift scan) ((), xs)
- in (y, xs') end;
-
-fun read stopper scan xs =
- (case error (finite stopper (option scan)) xs of
- (y as Some _, []) => y
- | _ => None);
-
-
-
-(* infinite scans -- draining state-based source *)
-
-fun drain def_prmpt get stopper scan ((state, xs), src) =
- (scan (state, xs), src) handle MORE prmpt =>
- (case get (if_none prmpt def_prmpt) src of
- ([], _) => (finite' stopper scan (state, xs), src)
- | (xs', src') => drain def_prmpt get stopper scan ((state, xs @ xs'), src'));
-
-fun source' def_prmpt get unget stopper scanner opt_recover (state, src) =
- let
- fun drain_with scan = drain def_prmpt get stopper scan;
-
- fun drain_loop recover inp =
- drain_with (catch scanner) inp handle FAIL msg =>
- (error_msg (if_none msg "Syntax error.");
- drain_loop recover (apfst snd (drain_with recover inp)));
-
- val ((ys, (state', xs')), src') =
- (case (get def_prmpt src, opt_recover) of
- (([], s), _) => (([], (state, [])), s)
- | ((xs, s), None) => drain_with (error scanner) ((state, xs), s)
- | ((xs, s), Some scan) => drain_loop scan ((state, xs), s));
- in
- (ys, (state', unget (xs', src')))
- end;
-
-fun source def_prmpt get unget stopper scan opt_recover src =
- let val (ys, ((), src')) =
- source' def_prmpt get unget stopper (lift scan) (apsome lift opt_recover) ((), src)
- in (ys, src') end;
-
-fun single scan = scan >> (fn x => [x]);
-fun bulk scan = scan -- repeat (try scan) >> (op ::);
-
-
-
-(** datatype lexicon **)
-
-datatype lexicon =
- Empty |
- Branch of string * string list * lexicon * lexicon * lexicon;
-
-val no_literal = [];
-
-
-(* dest_lexicon *)
-
-fun dest_lexicon Empty = []
- | dest_lexicon (Branch (_, [], lt, eq, gt)) =
- dest_lexicon lt @ dest_lexicon eq @ dest_lexicon gt
- | dest_lexicon (Branch (_, cs, lt, eq, gt)) =
- dest_lexicon lt @ [cs] @ dest_lexicon eq @ dest_lexicon gt;
-
-
-(* empty, extend, make, merge lexicons *)
-
-val empty_lexicon = Empty;
-
-fun extend_lexicon lexicon chrss =
- let
- fun ext (lex, chrs) =
- let
- fun add (Branch (d, a, lt, eq, gt)) (chs as c :: cs) =
- if c < d then Branch (d, a, add lt chs, eq, gt)
- else if c > d then Branch (d, a, lt, eq, add gt chs)
- else Branch (d, if null cs then chrs else a, lt, add eq cs, gt)
- | add Empty [c] =
- Branch (c, chrs, Empty, Empty, Empty)
- | add Empty (c :: cs) =
- Branch (c, no_literal, Empty, add Empty cs, Empty)
- | add lex [] = lex;
- in add lex chrs end;
- in foldl ext (lexicon, chrss \\ dest_lexicon lexicon) end;
-
-val make_lexicon = extend_lexicon empty_lexicon;
-
-fun merge_lexicons lex1 lex2 =
- let
- val chss1 = dest_lexicon lex1;
- val chss2 = dest_lexicon lex2;
- in
- if chss2 subset chss1 then lex1
- else if chss1 subset chss2 then lex2
- else extend_lexicon lex1 chss2
- end;
-
-
-(* scan literal *)
-
-fun literal lex chrs =
- let
- fun lit Empty res _ = res
- | lit (Branch _) _ [] = raise MORE None
- | lit (Branch (d, a, lt, eq, gt)) res (chs as c :: cs) =
- if c < d then lit lt res chs
- else if c > d then lit gt res chs
- else lit eq (if a = no_literal then res else Some (a, cs)) cs;
- in
- (case lit lex None chrs of
- None => raise FAIL None
- | Some res => res)
- end;
-
-
-end;
-
-
-structure BasicScan: BASIC_SCAN = Scan;
-open BasicScan;
--- a/src/Pure/Syntax/source.ML Wed Jan 13 12:16:34 1999 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,150 +0,0 @@
-(* Title: Pure/Syntax/source.ML
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
-
-Co-algebraic data sources.
-*)
-
-signature SOURCE =
-sig
- type ('a, 'b) source
- val set_prompt: string -> ('a, 'b) source -> ('a, 'b) source
- val get: ('a, 'b) source -> 'a list * ('a, 'b) source
- val unget: 'a list * ('a, 'b) source -> ('a, 'b) source
- val get_single: ('a, 'b) source -> ('a * ('a, 'b) source) option
- val exhaust: ('a, 'b) source -> 'a list
- val mapfilter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) source) source
- val filter: ('a -> bool) -> ('a, 'b) source -> ('a, ('a, 'b) source) source
- val of_list: 'a list -> ('a, 'a list) source
- val of_string: string -> (string, string list) source
- val of_file: string -> (string, string list) source
- val decorate_prompt_fn: (string -> string) ref
- val of_stream: TextIO.instream -> TextIO.outstream -> (string, unit) source
- val tty: (string, unit) source
- val source': 'a -> 'b * ('b -> bool) -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
- ('a * 'b list -> 'd * ('a * 'b list)) option ->
- ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source
- val source: 'a * ('a -> bool) -> ('a list -> 'b list * 'a list) ->
- ('a list -> 'c * 'a list) option ->
- ('a, 'd) source -> ('b, ('a, 'd) source) source
-end;
-
-structure Source: SOURCE =
-struct
-
-
-(** datatype source **)
-
-datatype ('a, 'b) source =
- Source of
- {buffer: 'a list,
- info: 'b,
- prompt: string,
- drain: string -> 'b -> 'a list * 'b};
-
-fun make_source buffer info prompt drain =
- Source {buffer = buffer, info = info, prompt = prompt, drain = drain};
-
-
-(* prompt *)
-
-val default_prompt = "> ";
-
-fun set_prompt prompt (Source {buffer, info, prompt = _, drain}) =
- make_source buffer info prompt drain;
-
-
-(* get / unget *)
-
-fun get (Source {buffer = [], info, prompt, drain}) =
- let val (xs, info') = drain prompt info
- in (xs, make_source [] info' prompt drain) end
- | get (Source {buffer, info, prompt, drain}) =
- (buffer, make_source [] info prompt drain);
-
-fun unget (xs, Source {buffer, info, prompt, drain}) =
- make_source (xs @ buffer) info prompt drain;
-
-
-(* variations on get *)
-
-fun get_prompt prompt src = get (set_prompt prompt src);
-
-fun get_single src =
- (case get src of
- ([], _) => None
- | (x :: xs, src') => Some (x, unget (xs, src')));
-
-fun exhaust src =
- (case get src of
- ([], _) => []
- | (xs, src') => xs @ exhaust src');
-
-
-(* (map)filter *)
-
-fun drain_mapfilter f prompt src =
- let
- val (xs, src') = get_prompt prompt src;
- val xs' = Library.mapfilter f xs;
- in
- if null xs orelse not (null xs') then (xs', src')
- else drain_mapfilter f prompt src'
- end;
-
-fun mapfilter f src = make_source [] src default_prompt (drain_mapfilter f);
-fun filter pred = mapfilter (fn x => if pred x then Some x else None);
-
-
-
-(** build sources **)
-
-(* list source *)
-
-(*limiting the input buffer considerably improves performance*)
-val limit = 4000;
-
-fun drain_list _ xs = (take (limit, xs), drop (limit, xs));
-
-fun of_list xs = make_source [] xs default_prompt drain_list;
-val of_string = of_list o explode;
-val of_file = of_string o File.read;
-
-
-(* stream source *)
-
-val decorate_prompt_fn = ref (fn s:string => s);
-
-fun drain_stream instream outstream prompt () =
- (TextIO.output (outstream, ! decorate_prompt_fn prompt);
- TextIO.flushOut outstream;
- (explode (TextIO.inputLine instream), ()));
-
-fun of_stream instream outstream =
- make_source [] () default_prompt (drain_stream instream outstream);
-
-val tty = of_stream TextIO.stdIn TextIO.stdOut;
-
-
-
-(** compose sources **)
-
-fun drain_source source stopper scan recover prompt src =
- source prompt get_prompt unget stopper scan recover src;
-
-
-(* state-based *)
-
-fun source' init_state stopper scan recover src =
- make_source [] (init_state, src) default_prompt
- (drain_source Scan.source' stopper scan recover);
-
-
-(* non state-based *)
-
-fun source stopper scan recover src =
- make_source [] src default_prompt
- (drain_source Scan.source stopper scan recover);
-
-
-end;
--- a/src/Pure/Syntax/symbol.ML Wed Jan 13 12:16:34 1999 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,274 +0,0 @@
-(* Title: Pure/Syntax/symbol.ML
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
-
-Generalized characters.
-*)
-
-signature SYMBOL =
-sig
- type symbol
- val space: symbol
- val eof: symbol
- val is_eof: symbol -> bool
- val not_eof: symbol -> bool
- val stopper: symbol * (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 beginning: symbol list -> string
- val scan: string list -> symbol * string list
- val explode: string -> symbol list
- val length: symbol list -> int
- val size: string -> int
- val input: string -> string
- val output: string -> string
- val source: bool -> (string, 'a) Source.source ->
- (symbol, (string, 'a) Source.source) Source.source
-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;
-
-val space = " ";
-val eof = "";
-
-
-(* kinds *)
-
-fun is_eof s = s = eof;
-fun not_eof s = s <> eof;
-val stopper = (eof, is_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
- | "\160" => true | "\\<space2>" => true
- | _ => false;
-
-val is_letdig = is_quasi_letter orf is_digit;
-
-fun is_printable s =
- size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" orelse
- size s > 2 andalso nth_elem (2, explode s) <> "^";
-
-
-(* beginning *)
-
-val smash_blanks = map (fn s => if is_blank s then space else s);
-
-fun beginning raw_ss =
- let
- val (all_ss, _) = take_suffix is_blank raw_ss;
- val dots = if length all_ss > 10 then " ..." else "";
- val (ss, _) = take_suffix is_blank (take (10, all_ss));
- in implode (smash_blanks ss) ^ dots end;
-
-
-(* 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;
-
-
-(* source *)
-
-val recover = Scan.any1 ((not o is_blank) andf not_eof);
-
-fun source do_recover src =
- Source.source stopper (Scan.bulk scan) (if do_recover then Some recover else None) src;
-
-
-(* 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 (the (Scan.read stopper (Scan.repeat scan) chs))
- end;
-
-
-(* printable length *)
-
-fun sym_length ss = foldl (fn (n, c) => if is_printable c then n + 1 else n) (0, ss);
-val sym_size = sym_length o sym_explode;
-
-
-(* 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 declarations of this structure!*)
-val explode = sym_explode;
-val length = sym_length;
-val size = sym_size;
-
-
-end;