files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
authorwenzelm
Wed Jan 13 12:44:33 1999 +0100 (1999-01-13)
changeset 61168ba2f25610f7
parent 6115 c70bce7deb0f
child 6117 f9aad8ccd590
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
src/Pure/General/README
src/Pure/General/ROOT.ML
src/Pure/General/pretty.ML
src/Pure/General/scan.ML
src/Pure/General/source.ML
src/Pure/General/symbol.ML
src/Pure/IsaMakefile
src/Pure/Syntax/README
src/Pure/Syntax/ROOT.ML
src/Pure/Syntax/pretty.ML
src/Pure/Syntax/scan.ML
src/Pure/Syntax/source.ML
src/Pure/Syntax/symbol.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/General/README	Wed Jan 13 12:44:33 1999 +0100
     1.3 @@ -0,0 +1,20 @@
     1.4 +
     1.5 +                                Pure/General/
     1.6 +
     1.7 +
     1.8 +This directory contains general purpose modules, all of which are
     1.9 +exported.
    1.10 +
    1.11 +  TableFun      (generic tables)
    1.12 +  Symtab        (tables indexed by strings)
    1.13 +  Object        (generic objects of arbitrary type)
    1.14 +  Seq           (unbounded sequences)
    1.15 +  NameSpace     (hierarchically structured name spaces)
    1.16 +  Position      (input positions)
    1.17 +  Path          (abstract algebra of file paths)
    1.18 +  File          (file system operations)
    1.19 +  History       (histories of values, with undo and redo)
    1.20 +  Scan          (generic scanner toolbox)
    1.21 +  Source        (co-algebraic data sources)
    1.22 +  Symbol        (generalized characters)
    1.23 +  Pretty        (generic pretty printing module)
     2.1 --- a/src/Pure/General/ROOT.ML	Wed Jan 13 12:16:34 1999 +0100
     2.2 +++ b/src/Pure/General/ROOT.ML	Wed Jan 13 12:44:33 1999 +0100
     2.3 @@ -12,6 +12,10 @@
     2.4  use "path.ML";
     2.5  use "file.ML";
     2.6  use "history.ML";
     2.7 +use "scan.ML";
     2.8 +use "source.ML";
     2.9 +use "symbol.ML";
    2.10 +use "pretty.ML";
    2.11  
    2.12  structure PureGeneral =
    2.13  struct
    2.14 @@ -23,4 +27,8 @@
    2.15    structure Path = Path;
    2.16    structure File = File;
    2.17    structure History = History;
    2.18 +  structure Scan = Scan;
    2.19 +  structure Source = Source;
    2.20 +  structure Symbol = Symbol;
    2.21 +  structure Pretty = Pretty;
    2.22  end;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/General/pretty.ML	Wed Jan 13 12:44:33 1999 +0100
     3.3 @@ -0,0 +1,249 @@
     3.4 +(*  Title:      Pure/Syntax/pretty.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson
     3.7 +    Copyright   1991  University of Cambridge
     3.8 +
     3.9 +Generic pretty printing module.
    3.10 +
    3.11 +Loosely based on
    3.12 +  D. C. Oppen, "Pretty Printing",
    3.13 +  ACM Transactions on Programming Languages and Systems (1980), 465-483.
    3.14 +
    3.15 +The object to be printed is given as a tree with indentation and line
    3.16 +breaking information.  A "break" inserts a newline if the text until
    3.17 +the next break is too long to fit on the current line.  After the newline,
    3.18 +text is indented to the level of the enclosing block.  Normally, if a block
    3.19 +is broken then all enclosing blocks will also be broken.  Only "inconsistent
    3.20 +breaks" are provided.
    3.21 +
    3.22 +The stored length of a block is used in breakdist (to treat each inner block as
    3.23 +a unit for breaking).
    3.24 +*)
    3.25 +
    3.26 +type pprint_args = (string -> unit) * (int -> unit) * (int -> unit) *
    3.27 +  (unit -> unit) * (unit -> unit);
    3.28 +
    3.29 +signature PRETTY =
    3.30 +  sig
    3.31 +  type T
    3.32 +  val str: string -> T
    3.33 +  val strlen: string -> int -> T
    3.34 +  val sym: string -> T
    3.35 +  val spc: int -> T
    3.36 +  val brk: int -> T
    3.37 +  val fbrk: T
    3.38 +  val blk: int * T list -> T
    3.39 +  val lst: string * string -> T list -> T
    3.40 +  val quote: T -> T
    3.41 +  val commas: T list -> T list
    3.42 +  val breaks: T list -> T list
    3.43 +  val fbreaks: T list -> T list
    3.44 +  val block: T list -> T
    3.45 +  val strs: string list -> T
    3.46 +  val enclose: string -> string -> T list -> T
    3.47 +  val list: string -> string -> T list -> T
    3.48 +  val str_list: string -> string -> string list -> T
    3.49 +  val big_list: string -> T list -> T
    3.50 +  val string_of: T -> string
    3.51 +  val writeln: T -> unit
    3.52 +  val str_of: T -> string
    3.53 +  val pprint: T -> pprint_args -> unit
    3.54 +  val setdepth: int -> unit
    3.55 +  val setmargin: int -> unit
    3.56 +  end;
    3.57 +
    3.58 +structure Pretty : PRETTY =
    3.59 +struct
    3.60 +
    3.61 +(*printing items: compound phrases, strings, and breaks*)
    3.62 +datatype T =
    3.63 +  Block of T list * int * int |         (*body, indentation, length*)
    3.64 +  String of string * int |              (*text, length*)
    3.65 +  Break of bool * int;                  (*mandatory flag, width if not taken*);
    3.66 +
    3.67 +(*Add the lengths of the expressions until the next Break; if no Break then
    3.68 +  include "after", to account for text following this block. *)
    3.69 +fun breakdist (Block(_,_,len)::es, after) = len + breakdist(es, after)
    3.70 +  | breakdist (String (s, len) :: es, after) = len + breakdist (es, after)
    3.71 +  | breakdist (Break _ :: es, after) = 0
    3.72 +  | breakdist ([], after) = after;
    3.73 +
    3.74 +fun repstring a 0 = ""
    3.75 +  | repstring a 1 = a
    3.76 +  | repstring a k =
    3.77 +      if k mod 2 = 0 then repstring(a^a) (k div 2)
    3.78 +                     else repstring(a^a) (k div 2) ^ a;
    3.79 +
    3.80 +(*** Type for lines of text: string, # of lines, position on line ***)
    3.81 +
    3.82 +type text = {tx: string, nl: int, pos: int};
    3.83 +
    3.84 +val emptytext = {tx="", nl=0, pos=0};
    3.85 +
    3.86 +fun blanks wd {tx,nl,pos} =
    3.87 +    {tx  = tx ^ repstring " " wd,
    3.88 +     nl  = nl,
    3.89 +     pos = pos+wd};
    3.90 +
    3.91 +fun newline {tx,nl,pos} =
    3.92 +    {tx  = tx ^ "\n",
    3.93 +     nl  = nl+1,
    3.94 +     pos = 0};
    3.95 +
    3.96 +fun string s len {tx,nl,pos:int} =
    3.97 +    {tx  = tx ^ s,
    3.98 +     nl  = nl,
    3.99 +     pos = pos + len};
   3.100 +
   3.101 +
   3.102 +(*** Formatting ***)
   3.103 +
   3.104 +(* margin *)
   3.105 +
   3.106 +(*example values*)
   3.107 +val margin      = ref 80        (*right margin, or page width*)
   3.108 +and breakgain   = ref 4         (*minimum added space required of a break*)
   3.109 +and emergencypos = ref 40;      (*position too far to right*)
   3.110 +
   3.111 +fun setmargin m =
   3.112 +    (margin     := m;
   3.113 +     breakgain  := !margin div 20;
   3.114 +     emergencypos := !margin div 2);
   3.115 +
   3.116 +val () = setmargin 76;
   3.117 +
   3.118 +
   3.119 +(*Search for the next break (at this or higher levels) and force it to occur*)
   3.120 +fun forcenext [] = []
   3.121 +  | forcenext (Break(_,wd) :: es) = Break(true,0) :: es
   3.122 +  | forcenext (e :: es) = e :: forcenext es;
   3.123 +
   3.124 +(*es is list of expressions to print;
   3.125 +  blockin is the indentation of the current block;
   3.126 +  after is the width of the following context until next break. *)
   3.127 +fun format ([], _, _) text = text
   3.128 +  | format (e::es, blockin, after) (text as {pos,nl,...}) =
   3.129 +    (case e of
   3.130 +       Block(bes,indent,wd) =>
   3.131 +         let val blockin' = (pos + indent) mod !emergencypos
   3.132 +             val btext = format(bes, blockin', breakdist(es,after)) text
   3.133 +             (*If this block was broken then force the next break.*)
   3.134 +             val es2 = if nl < #nl(btext) then forcenext es else es
   3.135 +         in  format (es2,blockin,after) btext  end
   3.136 +     | String (s, len) => format (es,blockin,after) (string s len text)
   3.137 +     | Break(force,wd) => (*no break if text to next break fits on this line
   3.138 +                            or if breaking would add only breakgain to space *)
   3.139 +           format (es,blockin,after)
   3.140 +               (if not force andalso
   3.141 +                   pos+wd <= Int.max(!margin - breakdist(es,after),
   3.142 +                                     blockin + !breakgain)
   3.143 +                then blanks wd text  (*just insert wd blanks*)
   3.144 +                else blanks blockin (newline text)));
   3.145 +
   3.146 +
   3.147 +(*** Exported functions to create formatting expressions ***)
   3.148 +
   3.149 +fun length (Block (_, _, len)) = len
   3.150 +  | length (String (_, len)) = len
   3.151 +  | length (Break(_, wd)) = wd;
   3.152 +
   3.153 +fun str s = String (s, size s);
   3.154 +fun strlen s len = String (s, len);
   3.155 +fun sym s = String (s, Symbol.size s);
   3.156 +
   3.157 +fun spc n = str (repstring " " n);
   3.158 +
   3.159 +fun brk wd = Break (false, wd);
   3.160 +val fbrk = Break (true, 0);
   3.161 +
   3.162 +fun blk (indent, es) =
   3.163 +  let
   3.164 +    fun sum([], k) = k
   3.165 +      | sum(e :: es, k) = sum (es, length e + k);
   3.166 +  in Block (es, indent, sum (es, 0)) end;
   3.167 +
   3.168 +(*Join the elements of es as a comma-separated list, bracketted by lp and rp*)
   3.169 +fun lst(lp,rp) es =
   3.170 +  let fun add(e,es) = str"," :: brk 1 :: e :: es;
   3.171 +      fun list(e :: (es as _::_)) = str lp :: e :: foldr add (es,[str rp])
   3.172 +        | list(e::[]) = [str lp, e, str rp]
   3.173 +        | list([]) = []
   3.174 +  in blk(size lp, list es) end;
   3.175 +
   3.176 +
   3.177 +(* utils *)
   3.178 +
   3.179 +fun quote prt =
   3.180 +  blk (1, [str "\"", prt, str "\""]);
   3.181 +
   3.182 +fun commas prts =
   3.183 +  flat (separate [str ",", brk 1] (map (fn x => [x]) prts));
   3.184 +
   3.185 +fun breaks prts = separate (brk 1) prts;
   3.186 +
   3.187 +fun fbreaks prts = separate fbrk prts;
   3.188 +
   3.189 +fun block prts = blk (2, prts);
   3.190 +
   3.191 +val strs = block o breaks o (map str);
   3.192 +
   3.193 +fun enclose lpar rpar prts =
   3.194 +  block (str lpar :: (prts @ [str rpar]));
   3.195 +
   3.196 +fun list lpar rpar prts =
   3.197 +  enclose lpar rpar (commas prts);
   3.198 +
   3.199 +fun str_list lpar rpar strs =
   3.200 +  list lpar rpar (map str strs);
   3.201 +
   3.202 +fun big_list name prts =
   3.203 +  block (fbreaks (str name :: prts));
   3.204 +
   3.205 +
   3.206 +
   3.207 +(*** Pretty printing with depth limitation ***)
   3.208 +
   3.209 +val depth       = ref 0;        (*maximum depth; 0 means no limit*)
   3.210 +
   3.211 +fun setdepth dp = (depth := dp);
   3.212 +
   3.213 +(*Recursively prune blocks, discarding all text exceeding depth dp*)
   3.214 +fun pruning dp (Block(bes,indent,wd)) =
   3.215 +      if dp>0 then blk(indent, map (pruning(dp-1)) bes)
   3.216 +              else str "..."
   3.217 +  | pruning dp e = e;
   3.218 +
   3.219 +fun prune dp e = if dp>0 then pruning dp e else e;
   3.220 +
   3.221 +
   3.222 +fun string_of e = #tx (format ([prune (!depth) e], 0, 0) emptytext);
   3.223 +
   3.224 +val writeln = writeln o string_of;
   3.225 +
   3.226 +
   3.227 +(*Create a single flat string: no line breaking*)
   3.228 +fun str_of prt =
   3.229 +  let
   3.230 +    fun s_of (Block (prts, _, _)) = implode (map s_of prts)
   3.231 +      | s_of (String (s, _)) = s
   3.232 +      | s_of (Break (false, wd)) = repstring " " wd
   3.233 +      | s_of (Break (true, _)) = " ";
   3.234 +  in
   3.235 +    s_of (prune (! depth) prt)
   3.236 +  end;
   3.237 +
   3.238 +(*Part of the interface to the Poly/ML and New Jersey ML pretty printers*)
   3.239 +fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
   3.240 +  let
   3.241 +    fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
   3.242 +      | pp (String (s, _)) = put_str s
   3.243 +      | pp (Break (false, wd)) = put_brk wd
   3.244 +      | pp (Break (true, _)) = put_fbrk ()
   3.245 +    and pp_lst [] = ()
   3.246 +      | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
   3.247 +  in
   3.248 +    pp (prune (! depth) prt)
   3.249 +  end;
   3.250 +
   3.251 +
   3.252 +end;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/General/scan.ML	Wed Jan 13 12:44:33 1999 +0100
     4.3 @@ -0,0 +1,305 @@
     4.4 +(*  Title:	Pure/Syntax/scan.ML
     4.5 +    ID:		$Id$
     4.6 +    Author:	Markus Wenzel and Tobias Nipkow, TU Muenchen
     4.7 +
     4.8 +Generic scanners (for potentially infinite input).
     4.9 +*)
    4.10 +
    4.11 +infix 5 -- :-- |-- --| ^^;
    4.12 +infix 3 >>;
    4.13 +infix 0 ||;
    4.14 +
    4.15 +signature BASIC_SCAN =
    4.16 +sig
    4.17 +  val !! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b
    4.18 +  val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
    4.19 +  val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
    4.20 +  val -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
    4.21 +  val :-- : ('a -> 'b * 'c) * ('b -> 'c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
    4.22 +  val |-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e
    4.23 +  val --| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e
    4.24 +  val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c
    4.25 +  val $$ : ''a -> ''a list -> ''a * ''a list
    4.26 +end;
    4.27 +
    4.28 +signature SCAN =
    4.29 +sig
    4.30 +  include BASIC_SCAN
    4.31 +  val fail: 'a -> 'b
    4.32 +  val fail_with: ('a -> string) -> 'a -> 'b
    4.33 +  val succeed: 'a -> 'b -> 'a * 'b
    4.34 +  val one: ('a -> bool) -> 'a list -> 'a * 'a list
    4.35 +  val any: ('a -> bool) -> 'a list -> 'a list * 'a list
    4.36 +  val any1: ('a -> bool) -> 'a list -> 'a list * 'a list
    4.37 +  val optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a
    4.38 +  val option: ('a -> 'b * 'a) -> 'a -> 'b option * 'a
    4.39 +  val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    4.40 +  val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    4.41 +  val max: ('a * 'a -> bool) -> ('b -> 'a * 'b) -> ('b -> 'a * 'b) -> 'b -> 'a * 'b
    4.42 +  val ahead: ('a -> 'b * 'c) -> 'a -> 'b * 'a
    4.43 +  val unless: ('a -> 'b * 'a) -> ('a -> 'c * 'd) -> 'a -> 'c * 'd
    4.44 +  val first: ('a -> 'b) list -> 'a -> 'b
    4.45 +  val depend: ('a -> 'b -> ('c * 'd) * 'e) -> 'a * 'b -> 'd * ('c * 'e)
    4.46 +  val lift: ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c)
    4.47 +  val pass: 'a -> ('a * 'b -> 'c * ('d * 'e)) -> 'b -> 'c * 'e
    4.48 +  val try: ('a -> 'b) -> 'a -> 'b
    4.49 +  val force: ('a -> 'b) -> 'a -> 'b
    4.50 +  val prompt: string -> ('a -> 'b) -> 'a -> 'b
    4.51 +  val finite': 'a * ('a -> bool) -> ('b * 'a list -> 'c * ('d * 'a list))
    4.52 +    -> 'b * 'a list -> 'c * ('d * 'a list)
    4.53 +  val finite: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b * 'a list
    4.54 +  val read: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b option
    4.55 +  val catch: ('a -> 'b) -> 'a -> 'b
    4.56 +  val error: ('a -> 'b) -> 'a -> 'b
    4.57 +  val source': string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
    4.58 +    'b * ('b -> bool) -> ('d * 'b list -> 'e list * ('d * 'b list)) ->
    4.59 +    ('d * 'b list -> 'f * ('d * 'b list)) option -> 'd * 'a -> 'e list * ('d * 'c)
    4.60 +  val source: string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
    4.61 +    'b * ('b -> bool) -> ('b list -> 'd list * 'b list) ->
    4.62 +    ('b list -> 'e * 'b list) option -> 'a -> 'd list * 'c
    4.63 +  val single: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    4.64 +  val bulk: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    4.65 +  type lexicon
    4.66 +  val dest_lexicon: lexicon -> string list list
    4.67 +  val make_lexicon: string list list -> lexicon
    4.68 +  val empty_lexicon: lexicon
    4.69 +  val extend_lexicon: lexicon -> string list list -> lexicon
    4.70 +  val merge_lexicons: lexicon -> lexicon -> lexicon
    4.71 +  val literal: lexicon -> string list -> string list * string list
    4.72 +end;
    4.73 +
    4.74 +structure Scan: SCAN =
    4.75 +struct
    4.76 +
    4.77 +
    4.78 +(** scanners **)
    4.79 +
    4.80 +exception MORE of string option;	(*need more input (prompt)*)
    4.81 +exception FAIL of string option;	(*try alternatives (reason of failure)*)
    4.82 +exception ABORT of string;		(*dead end*)
    4.83 +
    4.84 +
    4.85 +(* scanner combinators *)
    4.86 +
    4.87 +fun (scan >> f) xs = apfst f (scan xs);
    4.88 +
    4.89 +fun (scan1 || scan2) xs = scan1 xs handle FAIL _ => scan2 xs;
    4.90 +
    4.91 +(*dependent pairing*)
    4.92 +fun (scan1 :-- scan2) xs =
    4.93 +  let
    4.94 +    val (x, ys) = scan1 xs;
    4.95 +    val (y, zs) = scan2 x ys;
    4.96 +  in ((x, y), zs) end;
    4.97 +
    4.98 +fun (scan1 -- scan2) = scan1 :-- (fn _ => scan2);
    4.99 +fun (scan1 |-- scan2) = scan1 -- scan2 >> #2;
   4.100 +fun (scan1 --| scan2) = scan1 -- scan2 >> #1;
   4.101 +fun (scan1 ^^ scan2) = scan1 -- scan2 >> op ^;
   4.102 +
   4.103 +
   4.104 +(* generic scanners *)
   4.105 +
   4.106 +fun fail _ = raise FAIL None;
   4.107 +fun fail_with msg_of xs = raise FAIL (Some (msg_of xs));
   4.108 +fun succeed y xs = (y, xs);
   4.109 +
   4.110 +fun one _ [] = raise MORE None
   4.111 +  | one pred (x :: xs) =
   4.112 +      if pred x then (x, xs) else raise FAIL None;
   4.113 +
   4.114 +fun $$ _ [] = raise MORE None
   4.115 +  | $$ a (x :: xs) =
   4.116 +      if a = x then (x, xs) else raise FAIL None;
   4.117 +
   4.118 +fun any _ [] = raise MORE None
   4.119 +  | any pred (lst as x :: xs) =
   4.120 +      if pred x then apfst (cons x) (any pred xs)
   4.121 +      else ([], lst);
   4.122 +
   4.123 +fun any1 pred = one pred -- any pred >> op ::;
   4.124 +
   4.125 +fun optional scan def = scan || succeed def;
   4.126 +fun option scan = optional (scan >> Some) None;
   4.127 +
   4.128 +fun repeat scan xs = (scan -- repeat scan >> op :: || succeed []) xs;
   4.129 +fun repeat1 scan = scan -- repeat scan >> op ::;
   4.130 +
   4.131 +fun max leq scan1 scan2 xs =
   4.132 +  (case (option scan1 xs, option scan2 xs) of
   4.133 +    ((None, _), (None, _)) => raise FAIL None		(*looses FAIL msg!*)
   4.134 +  | ((Some tok1, xs'), (None, _)) => (tok1, xs')
   4.135 +  | ((None, _), (Some tok2, xs')) => (tok2, xs')
   4.136 +  | ((Some tok1, xs1'), (Some tok2, xs2')) =>
   4.137 +      if leq (tok2, tok1) then (tok1, xs1') else (tok2, xs2'));
   4.138 +
   4.139 +fun ahead scan xs = (fst (scan xs), xs);
   4.140 +
   4.141 +fun unless test scan =
   4.142 +  ahead (option test) :-- (fn None => scan | _ => fail) >> #2;
   4.143 +
   4.144 +fun first [] = fail
   4.145 +  | first (scan :: scans) = scan || first scans;
   4.146 +
   4.147 +
   4.148 +(* state based scanners *)
   4.149 +
   4.150 +fun depend scan (st, xs) =
   4.151 +  let val ((st', y), xs') = scan st xs
   4.152 +  in (y, (st', xs')) end;
   4.153 +
   4.154 +fun lift scan (st, xs) =
   4.155 +  let val (y, xs') = scan xs
   4.156 +  in (y, (st, xs')) end;
   4.157 +
   4.158 +fun pass st scan xs =
   4.159 +  let val (y, (_, xs')) = scan (st, xs)
   4.160 +  in (y, xs') end;
   4.161 +
   4.162 +
   4.163 +(* exception handling *)
   4.164 +
   4.165 +fun !! err scan xs = scan xs handle FAIL msg => raise ABORT (err (xs, msg));
   4.166 +fun try scan xs = scan xs handle MORE _ => raise FAIL None | ABORT _ => raise FAIL None;
   4.167 +fun force scan xs = scan xs handle MORE _ => raise FAIL None;
   4.168 +fun prompt str scan xs = scan xs handle MORE None => raise MORE (Some str);
   4.169 +fun catch scan xs = scan xs handle ABORT msg => raise FAIL (Some msg);
   4.170 +fun error scan xs = scan xs handle ABORT msg => Library.error msg;
   4.171 +
   4.172 +
   4.173 +(* finite scans *)
   4.174 +
   4.175 +fun finite' (stopper, is_stopper) scan (state, input) =
   4.176 +  let
   4.177 +    fun lost () = raise ABORT "Scanner bug: lost stopper of finite scan!";
   4.178 +
   4.179 +    fun stop [] = lost ()
   4.180 +      | stop lst =
   4.181 +          let val (xs, x) = split_last lst
   4.182 +          in if is_stopper x then ((), xs) else lost () end;
   4.183 +  in
   4.184 +    if exists is_stopper input then
   4.185 +      raise ABORT "Stopper may not occur in input of finite scan!"
   4.186 +    else (force scan --| lift stop) (state, input @ [stopper])
   4.187 +  end;
   4.188 +
   4.189 +fun finite stopper scan xs =
   4.190 +  let val (y, ((), xs')) = finite' stopper (lift scan) ((), xs)
   4.191 +  in (y, xs') end;
   4.192 +
   4.193 +fun read stopper scan xs =
   4.194 +  (case error (finite stopper (option scan)) xs of
   4.195 +    (y as Some _, []) => y
   4.196 +  | _ => None);
   4.197 +
   4.198 +
   4.199 +
   4.200 +(* infinite scans -- draining state-based source *)
   4.201 +
   4.202 +fun drain def_prmpt get stopper scan ((state, xs), src) =
   4.203 +  (scan (state, xs), src) handle MORE prmpt =>
   4.204 +    (case get (if_none prmpt def_prmpt) src of
   4.205 +      ([], _) => (finite' stopper scan (state, xs), src)
   4.206 +    | (xs', src') => drain def_prmpt get stopper scan ((state, xs @ xs'), src'));
   4.207 +
   4.208 +fun source' def_prmpt get unget stopper scanner opt_recover (state, src) =
   4.209 +  let
   4.210 +    fun drain_with scan = drain def_prmpt get stopper scan;
   4.211 +
   4.212 +    fun drain_loop recover inp =
   4.213 +      drain_with (catch scanner) inp handle FAIL msg =>
   4.214 +        (error_msg (if_none msg "Syntax error.");
   4.215 +          drain_loop recover (apfst snd (drain_with recover inp)));
   4.216 +
   4.217 +    val ((ys, (state', xs')), src') =
   4.218 +      (case (get def_prmpt src, opt_recover) of
   4.219 +        (([], s), _) => (([], (state, [])), s)
   4.220 +      | ((xs, s), None) => drain_with (error scanner) ((state, xs), s)
   4.221 +      | ((xs, s), Some scan) => drain_loop scan ((state, xs), s));
   4.222 +  in
   4.223 +    (ys, (state', unget (xs', src')))
   4.224 +  end;
   4.225 +
   4.226 +fun source def_prmpt get unget stopper scan opt_recover src =
   4.227 +  let val (ys, ((), src')) =
   4.228 +    source' def_prmpt get unget stopper (lift scan) (apsome lift opt_recover) ((), src)
   4.229 +  in (ys, src') end;
   4.230 +
   4.231 +fun single scan = scan >> (fn x => [x]);
   4.232 +fun bulk scan = scan -- repeat (try scan) >> (op ::);
   4.233 +
   4.234 +
   4.235 +
   4.236 +(** datatype lexicon **)
   4.237 +
   4.238 +datatype lexicon =
   4.239 +  Empty |
   4.240 +  Branch of string * string list * lexicon * lexicon * lexicon;
   4.241 +
   4.242 +val no_literal = [];
   4.243 +
   4.244 +
   4.245 +(* dest_lexicon *)
   4.246 +
   4.247 +fun dest_lexicon Empty = []
   4.248 +  | dest_lexicon (Branch (_, [], lt, eq, gt)) =
   4.249 +      dest_lexicon lt @ dest_lexicon eq @ dest_lexicon gt
   4.250 +  | dest_lexicon (Branch (_, cs, lt, eq, gt)) =
   4.251 +      dest_lexicon lt @ [cs] @ dest_lexicon eq @ dest_lexicon gt;
   4.252 +
   4.253 +
   4.254 +(* empty, extend, make, merge lexicons *)
   4.255 +
   4.256 +val empty_lexicon = Empty;
   4.257 +
   4.258 +fun extend_lexicon lexicon chrss =
   4.259 +  let
   4.260 +    fun ext (lex, chrs) =
   4.261 +      let
   4.262 +	fun add (Branch (d, a, lt, eq, gt)) (chs as c :: cs) =
   4.263 +	      if c < d then Branch (d, a, add lt chs, eq, gt)
   4.264 +	      else if c > d then Branch (d, a, lt, eq, add gt chs)
   4.265 +	      else Branch (d, if null cs then chrs else a, lt, add eq cs, gt)
   4.266 +	  | add Empty [c] =
   4.267 +	      Branch (c, chrs, Empty, Empty, Empty)
   4.268 +	  | add Empty (c :: cs) =
   4.269 +	      Branch (c, no_literal, Empty, add Empty cs, Empty)
   4.270 +	  | add lex [] = lex;
   4.271 +      in add lex chrs end;
   4.272 +  in foldl ext (lexicon, chrss \\ dest_lexicon lexicon) end;
   4.273 +
   4.274 +val make_lexicon = extend_lexicon empty_lexicon;
   4.275 +
   4.276 +fun merge_lexicons lex1 lex2 =
   4.277 +  let
   4.278 +    val chss1 = dest_lexicon lex1;
   4.279 +    val chss2 = dest_lexicon lex2;
   4.280 +  in
   4.281 +    if chss2 subset chss1 then lex1
   4.282 +    else if chss1 subset chss2 then lex2
   4.283 +    else extend_lexicon lex1 chss2
   4.284 +  end;
   4.285 +
   4.286 +
   4.287 +(* scan literal *)
   4.288 +
   4.289 +fun literal lex chrs =
   4.290 +  let
   4.291 +    fun lit Empty res _ = res
   4.292 +      | lit (Branch _) _ [] = raise MORE None
   4.293 +      | lit (Branch (d, a, lt, eq, gt)) res (chs as c :: cs) =
   4.294 +	  if c < d then lit lt res chs
   4.295 +	  else if c > d then lit gt res chs
   4.296 +	  else lit eq (if a = no_literal then res else Some (a, cs)) cs;
   4.297 +  in
   4.298 +    (case lit lex None chrs of
   4.299 +      None => raise FAIL None
   4.300 +    | Some res => res)
   4.301 +  end;
   4.302 +
   4.303 +
   4.304 +end;
   4.305 +
   4.306 +
   4.307 +structure BasicScan: BASIC_SCAN = Scan;
   4.308 +open BasicScan;
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Pure/General/source.ML	Wed Jan 13 12:44:33 1999 +0100
     5.3 @@ -0,0 +1,150 @@
     5.4 +(*  Title:      Pure/Syntax/source.ML
     5.5 +    ID:         $Id$
     5.6 +    Author:     Markus Wenzel, TU Muenchen
     5.7 +
     5.8 +Co-algebraic data sources.
     5.9 +*)
    5.10 +
    5.11 +signature SOURCE =
    5.12 +sig
    5.13 +  type ('a, 'b) source
    5.14 +  val set_prompt: string -> ('a, 'b) source -> ('a, 'b) source
    5.15 +  val get: ('a, 'b) source -> 'a list * ('a, 'b) source
    5.16 +  val unget: 'a list * ('a, 'b) source -> ('a, 'b) source
    5.17 +  val get_single: ('a, 'b) source -> ('a * ('a, 'b) source) option
    5.18 +  val exhaust: ('a, 'b) source -> 'a list
    5.19 +  val mapfilter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) source) source
    5.20 +  val filter: ('a -> bool) -> ('a, 'b) source -> ('a, ('a, 'b) source) source
    5.21 +  val of_list: 'a list -> ('a, 'a list) source
    5.22 +  val of_string: string -> (string, string list) source
    5.23 +  val of_file: string -> (string, string list) source
    5.24 +  val decorate_prompt_fn: (string -> string) ref
    5.25 +  val of_stream: TextIO.instream -> TextIO.outstream -> (string, unit) source
    5.26 +  val tty: (string, unit) source
    5.27 +  val source': 'a -> 'b * ('b -> bool) -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
    5.28 +    ('a * 'b list -> 'd * ('a * 'b list)) option ->
    5.29 +    ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source
    5.30 +  val source: 'a * ('a -> bool) -> ('a list -> 'b list * 'a list) ->
    5.31 +    ('a list -> 'c * 'a list) option ->
    5.32 +    ('a, 'd) source -> ('b, ('a, 'd) source) source
    5.33 +end;
    5.34 +
    5.35 +structure Source: SOURCE =
    5.36 +struct
    5.37 +
    5.38 +
    5.39 +(** datatype source **)
    5.40 +
    5.41 +datatype ('a, 'b) source =
    5.42 +  Source of
    5.43 +   {buffer: 'a list,
    5.44 +    info: 'b,
    5.45 +    prompt: string,
    5.46 +    drain: string -> 'b -> 'a list * 'b};
    5.47 +
    5.48 +fun make_source buffer info prompt drain =
    5.49 +  Source {buffer = buffer, info = info, prompt = prompt, drain = drain};
    5.50 +
    5.51 +
    5.52 +(* prompt *)
    5.53 +
    5.54 +val default_prompt = "> ";
    5.55 +
    5.56 +fun set_prompt prompt (Source {buffer, info, prompt = _, drain}) =
    5.57 +  make_source buffer info prompt drain;
    5.58 +
    5.59 +
    5.60 +(* get / unget *)
    5.61 +
    5.62 +fun get (Source {buffer = [], info, prompt, drain}) =
    5.63 +      let val (xs, info') = drain prompt info
    5.64 +      in (xs, make_source [] info' prompt drain) end
    5.65 +  | get (Source {buffer, info, prompt, drain}) =
    5.66 +      (buffer, make_source [] info prompt drain);
    5.67 +
    5.68 +fun unget (xs, Source {buffer, info, prompt, drain}) =
    5.69 +  make_source (xs @ buffer) info prompt drain;
    5.70 +
    5.71 +
    5.72 +(* variations on get *)
    5.73 +
    5.74 +fun get_prompt prompt src = get (set_prompt prompt src);
    5.75 +
    5.76 +fun get_single src =
    5.77 +  (case get src of
    5.78 +    ([], _) => None
    5.79 +  | (x :: xs, src') => Some (x, unget (xs, src')));
    5.80 +
    5.81 +fun exhaust src =
    5.82 +  (case get src of
    5.83 +    ([], _) => []
    5.84 +  | (xs, src') => xs @ exhaust src');
    5.85 +
    5.86 +
    5.87 +(* (map)filter *)
    5.88 +
    5.89 +fun drain_mapfilter f prompt src =
    5.90 +  let
    5.91 +    val (xs, src') = get_prompt prompt src;
    5.92 +    val xs' = Library.mapfilter f xs;
    5.93 +  in
    5.94 +    if null xs orelse not (null xs') then (xs', src')
    5.95 +    else drain_mapfilter f prompt src'
    5.96 +  end;
    5.97 +
    5.98 +fun mapfilter f src = make_source [] src default_prompt (drain_mapfilter f);
    5.99 +fun filter pred = mapfilter (fn x => if pred x then Some x else None);
   5.100 +
   5.101 +
   5.102 +
   5.103 +(** build sources **)
   5.104 +
   5.105 +(* list source *)
   5.106 +
   5.107 +(*limiting the input buffer considerably improves performance*)
   5.108 +val limit = 4000;
   5.109 +
   5.110 +fun drain_list _ xs = (take (limit, xs), drop (limit, xs));
   5.111 +
   5.112 +fun of_list xs = make_source [] xs default_prompt drain_list;
   5.113 +val of_string = of_list o explode;
   5.114 +val of_file = of_string o File.read;
   5.115 +
   5.116 +
   5.117 +(* stream source *)
   5.118 +
   5.119 +val decorate_prompt_fn = ref (fn s:string => s);
   5.120 +
   5.121 +fun drain_stream instream outstream prompt () =
   5.122 +  (TextIO.output (outstream, ! decorate_prompt_fn prompt);
   5.123 +    TextIO.flushOut outstream;
   5.124 +    (explode (TextIO.inputLine instream), ()));
   5.125 +
   5.126 +fun of_stream instream outstream =
   5.127 +  make_source [] () default_prompt (drain_stream instream outstream);
   5.128 +
   5.129 +val tty = of_stream TextIO.stdIn TextIO.stdOut;
   5.130 +
   5.131 +
   5.132 +
   5.133 +(** compose sources **)
   5.134 +
   5.135 +fun drain_source source stopper scan recover prompt src =
   5.136 +  source prompt get_prompt unget stopper scan recover src;
   5.137 +
   5.138 +
   5.139 +(* state-based *)
   5.140 +
   5.141 +fun source' init_state stopper scan recover src =
   5.142 +  make_source [] (init_state, src) default_prompt
   5.143 +    (drain_source Scan.source' stopper scan recover);
   5.144 +
   5.145 +
   5.146 +(* non state-based *)
   5.147 +
   5.148 +fun source stopper scan recover src =
   5.149 +  make_source [] src default_prompt
   5.150 +    (drain_source Scan.source stopper scan recover);
   5.151 +
   5.152 +
   5.153 +end;
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Pure/General/symbol.ML	Wed Jan 13 12:44:33 1999 +0100
     6.3 @@ -0,0 +1,274 @@
     6.4 +(*  Title:      Pure/Syntax/symbol.ML
     6.5 +    ID:         $Id$
     6.6 +    Author:     Markus Wenzel, TU Muenchen
     6.7 +
     6.8 +Generalized characters.
     6.9 +*)
    6.10 +
    6.11 +signature SYMBOL =
    6.12 +sig
    6.13 +  type symbol
    6.14 +  val space: symbol
    6.15 +  val eof: symbol
    6.16 +  val is_eof: symbol -> bool
    6.17 +  val not_eof: symbol -> bool
    6.18 +  val stopper: symbol * (symbol -> bool)
    6.19 +  val is_ascii: symbol -> bool
    6.20 +  val is_letter: symbol -> bool
    6.21 +  val is_digit: symbol -> bool
    6.22 +  val is_quasi_letter: symbol -> bool
    6.23 +  val is_letdig: symbol -> bool
    6.24 +  val is_blank: symbol -> bool
    6.25 +  val is_printable: symbol -> bool
    6.26 +  val beginning: symbol list -> string
    6.27 +  val scan: string list -> symbol * string list
    6.28 +  val explode: string -> symbol list
    6.29 +  val length: symbol list -> int
    6.30 +  val size: string -> int
    6.31 +  val input: string -> string
    6.32 +  val output: string -> string
    6.33 +  val source: bool -> (string, 'a) Source.source ->
    6.34 +    (symbol, (string, 'a) Source.source) Source.source
    6.35 +end;
    6.36 +
    6.37 +structure Symbol: SYMBOL =
    6.38 +struct
    6.39 +
    6.40 +
    6.41 +(** encoding table (isabelle-0) **)
    6.42 +
    6.43 +val enc_start = 160;
    6.44 +val enc_end = 255;
    6.45 +
    6.46 +val enc_vector =
    6.47 +[
    6.48 +(* GENERATED TEXT FOLLOWS - Do not edit! *)
    6.49 +  "\\<space2>",
    6.50 +  "\\<Gamma>",
    6.51 +  "\\<Delta>",
    6.52 +  "\\<Theta>",
    6.53 +  "\\<Lambda>",
    6.54 +  "\\<Pi>",
    6.55 +  "\\<Sigma>",
    6.56 +  "\\<Phi>",
    6.57 +  "\\<Psi>",
    6.58 +  "\\<Omega>",
    6.59 +  "\\<alpha>",
    6.60 +  "\\<beta>",
    6.61 +  "\\<gamma>",
    6.62 +  "\\<delta>",
    6.63 +  "\\<epsilon>",
    6.64 +  "\\<zeta>",
    6.65 +  "\\<eta>",
    6.66 +  "\\<theta>",
    6.67 +  "\\<kappa>",
    6.68 +  "\\<lambda>",
    6.69 +  "\\<mu>",
    6.70 +  "\\<nu>",
    6.71 +  "\\<xi>",
    6.72 +  "\\<pi>",
    6.73 +  "\\<rho>",
    6.74 +  "\\<sigma>",
    6.75 +  "\\<tau>",
    6.76 +  "\\<phi>",
    6.77 +  "\\<chi>",
    6.78 +  "\\<psi>",
    6.79 +  "\\<omega>",
    6.80 +  "\\<not>",
    6.81 +  "\\<and>",
    6.82 +  "\\<or>",
    6.83 +  "\\<forall>",
    6.84 +  "\\<exists>",
    6.85 +  "\\<And>",
    6.86 +  "\\<lceil>",
    6.87 +  "\\<rceil>",
    6.88 +  "\\<lfloor>",
    6.89 +  "\\<rfloor>",
    6.90 +  "\\<turnstile>",
    6.91 +  "\\<Turnstile>",
    6.92 +  "\\<lbrakk>",
    6.93 +  "\\<rbrakk>",
    6.94 +  "\\<cdot>",
    6.95 +  "\\<in>",
    6.96 +  "\\<subseteq>",
    6.97 +  "\\<inter>",
    6.98 +  "\\<union>",
    6.99 +  "\\<Inter>",
   6.100 +  "\\<Union>",
   6.101 +  "\\<sqinter>",
   6.102 +  "\\<squnion>",
   6.103 +  "\\<Sqinter>",
   6.104 +  "\\<Squnion>",
   6.105 +  "\\<bottom>",
   6.106 +  "\\<doteq>",
   6.107 +  "\\<equiv>",
   6.108 +  "\\<noteq>",
   6.109 +  "\\<sqsubset>",
   6.110 +  "\\<sqsubseteq>",
   6.111 +  "\\<prec>",
   6.112 +  "\\<preceq>",
   6.113 +  "\\<succ>",
   6.114 +  "\\<approx>",
   6.115 +  "\\<sim>",
   6.116 +  "\\<simeq>",
   6.117 +  "\\<le>",
   6.118 +  "\\<Colon>",
   6.119 +  "\\<leftarrow>",
   6.120 +  "\\<midarrow>",
   6.121 +  "\\<rightarrow>",
   6.122 +  "\\<Leftarrow>",
   6.123 +  "\\<Midarrow>",
   6.124 +  "\\<Rightarrow>",
   6.125 +  "\\<bow>",
   6.126 +  "\\<mapsto>",
   6.127 +  "\\<leadsto>",
   6.128 +  "\\<up>",
   6.129 +  "\\<down>",
   6.130 +  "\\<notin>",
   6.131 +  "\\<times>",
   6.132 +  "\\<oplus>",
   6.133 +  "\\<ominus>",
   6.134 +  "\\<otimes>",
   6.135 +  "\\<oslash>",
   6.136 +  "\\<subset>",
   6.137 +  "\\<infinity>",
   6.138 +  "\\<box>",
   6.139 +  "\\<diamond>",
   6.140 +  "\\<circ>",
   6.141 +  "\\<bullet>",
   6.142 +  "\\<parallel>",
   6.143 +  "\\<surd>",
   6.144 +  "\\<copyright>"
   6.145 +(* END OF GENERATED TEXT *)
   6.146 +];
   6.147 +
   6.148 +val enc_rel = enc_vector ~~ map chr (enc_start upto enc_end);
   6.149 +
   6.150 +val char_tab = Symtab.make enc_rel;
   6.151 +val symbol_tab = Symtab.make (map swap enc_rel);
   6.152 +
   6.153 +fun lookup_symbol c =
   6.154 +  if ord c < enc_start then None
   6.155 +  else Symtab.lookup (symbol_tab, c);
   6.156 +
   6.157 +
   6.158 +(* encode / decode *)
   6.159 +
   6.160 +fun char s = if_none (Symtab.lookup (char_tab, s)) s;
   6.161 +fun symbol c = if_none (lookup_symbol c) c;
   6.162 +
   6.163 +fun symbol' c =
   6.164 +  (case lookup_symbol c of
   6.165 +    None => c
   6.166 +  | Some s => "\\" ^ s);
   6.167 +
   6.168 +
   6.169 +
   6.170 +(** type symbol **)
   6.171 +
   6.172 +type symbol = string;
   6.173 +
   6.174 +val space = " ";
   6.175 +val eof = "";
   6.176 +
   6.177 +
   6.178 +(* kinds *)
   6.179 +
   6.180 +fun is_eof s = s = eof;
   6.181 +fun not_eof s = s <> eof;
   6.182 +val stopper = (eof, is_eof);
   6.183 +
   6.184 +fun is_ascii s = size s = 1 andalso ord s < 128;
   6.185 +
   6.186 +fun is_letter s =
   6.187 +  size s = 1 andalso
   6.188 +   (ord "A" <= ord s andalso ord s <= ord "Z" orelse
   6.189 +    ord "a" <= ord s andalso ord s <= ord "z");
   6.190 +
   6.191 +fun is_digit s =
   6.192 +  size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9";
   6.193 +
   6.194 +fun is_quasi_letter "_" = true
   6.195 +  | is_quasi_letter "'" = true
   6.196 +  | is_quasi_letter s = is_letter s;
   6.197 +
   6.198 +val is_blank =
   6.199 +  fn " " => true | "\t" => true | "\n" => true | "\^L" => true
   6.200 +    | "\160" => true | "\\<space2>" => true
   6.201 +    | _ => false;
   6.202 +
   6.203 +val is_letdig = is_quasi_letter orf is_digit;
   6.204 +
   6.205 +fun is_printable s =
   6.206 +  size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" orelse
   6.207 +  size s > 2 andalso nth_elem (2, explode s) <> "^";
   6.208 +
   6.209 +
   6.210 +(* beginning *)
   6.211 +
   6.212 +val smash_blanks = map (fn s => if is_blank s then space else s);
   6.213 +
   6.214 +fun beginning raw_ss =
   6.215 +  let
   6.216 +    val (all_ss, _) = take_suffix is_blank raw_ss;
   6.217 +    val dots = if length all_ss > 10 then " ..." else "";
   6.218 +    val (ss, _) = take_suffix is_blank (take (10, all_ss));
   6.219 +  in implode (smash_blanks ss) ^ dots end;
   6.220 +
   6.221 +
   6.222 +(* scan *)
   6.223 +
   6.224 +val scan_id = Scan.one is_letter ^^ (Scan.any is_letdig >> implode);
   6.225 +
   6.226 +val scan =
   6.227 +  ($$ "\\" --| Scan.optional ($$ "\\") "") ^^ $$ "<" ^^
   6.228 +    !! (fn (cs, _) => "Malformed symbolic character specification: \\" ^ "<" ^ beginning cs)
   6.229 +      (Scan.optional ($$ "^") "" ^^ scan_id ^^ $$ ">") ||
   6.230 +  Scan.one not_eof;
   6.231 +
   6.232 +
   6.233 +(* source *)
   6.234 +
   6.235 +val recover = Scan.any1 ((not o is_blank) andf not_eof);
   6.236 +
   6.237 +fun source do_recover src =
   6.238 +  Source.source stopper (Scan.bulk scan) (if do_recover then Some recover else None) src;
   6.239 +
   6.240 +
   6.241 +(* explode *)
   6.242 +
   6.243 +fun no_syms [] = true
   6.244 +  | no_syms ("\\" :: "<" :: _) = false
   6.245 +  | no_syms (c :: cs) = ord c < enc_start andalso no_syms cs;
   6.246 +
   6.247 +fun sym_explode str =
   6.248 +  let val chs = explode str in
   6.249 +    if no_syms chs then chs     (*tune trivial case*)
   6.250 +    else map symbol (the (Scan.read stopper (Scan.repeat scan) chs))
   6.251 +  end;
   6.252 +
   6.253 +
   6.254 +(* printable length *)
   6.255 +
   6.256 +fun sym_length ss = foldl (fn (n, c) => if is_printable c then n + 1 else n) (0, ss);
   6.257 +val sym_size = sym_length o sym_explode;
   6.258 +
   6.259 +
   6.260 +(* input / output *)
   6.261 +
   6.262 +fun input str =
   6.263 +  let val chs = explode str in
   6.264 +    if forall (fn c => ord c < enc_start) chs then str
   6.265 +    else implode (map symbol' chs)
   6.266 +  end;
   6.267 +
   6.268 +val output = implode o map char o sym_explode;
   6.269 +
   6.270 +
   6.271 +(*final declarations of this structure!*)
   6.272 +val explode = sym_explode;
   6.273 +val length = sym_length;
   6.274 +val size = sym_size;
   6.275 +
   6.276 +
   6.277 +end;
     7.1 --- a/src/Pure/IsaMakefile	Wed Jan 13 12:16:34 1999 +0100
     7.2 +++ b/src/Pure/IsaMakefile	Wed Jan 13 12:44:33 1999 +0100
     7.3 @@ -25,7 +25,8 @@
     7.4  
     7.5  $(OUT)/Pure: General/ROOT.ML General/file.ML General/history.ML \
     7.6    General/name_space.ML General/object.ML General/path.ML \
     7.7 -  General/position.ML General/seq.ML General/table.ML Isar/ROOT.ML \
     7.8 +  General/position.ML General/pretty.ML General/scan.ML General/seq.ML \
     7.9 +  General/source.ML General/symbol.ML General/table.ML Isar/ROOT.ML \
    7.10    Isar/args.ML Isar/attrib.ML Isar/isar.ML Isar/isar_cmd.ML \
    7.11    Isar/isar_syn.ML Isar/isar_thy.ML Isar/method.ML Isar/outer_lex.ML \
    7.12    Isar/outer_parse.ML Isar/outer_syntax.ML Isar/proof.ML \
    7.13 @@ -33,12 +34,11 @@
    7.14    Isar/toplevel.ML ML-Systems/mlworks.ML ML-Systems/polyml.ML \
    7.15    ML-Systems/smlnj-0.93.ML ML-Systems/smlnj.ML ROOT.ML Syntax/ROOT.ML \
    7.16    Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \
    7.17 -  Syntax/pretty.ML Syntax/printer.ML Syntax/scan.ML Syntax/source.ML \
    7.18 -  Syntax/symbol.ML Syntax/syn_ext.ML Syntax/syn_trans.ML \
    7.19 -  Syntax/syntax.ML Syntax/token_trans.ML Syntax/type_ext.ML \
    7.20 -  Thy/ROOT.ML Thy/browser_info.ML Thy/context.ML Thy/thm_database.ML \
    7.21 -  Thy/thy_info.ML Thy/thy_parse.ML Thy/thy_read.ML Thy/thy_scan.ML \
    7.22 -  Thy/thy_syn.ML Thy/use.ML axclass.ML basis.ML deriv.ML display.ML \
    7.23 +  Syntax/printer.ML Syntax/syn_ext.ML Syntax/syn_trans.ML \
    7.24 +  Syntax/syntax.ML Syntax/token_trans.ML Syntax/type_ext.ML Thy/ROOT.ML \
    7.25 +  Thy/browser_info.ML Thy/context.ML Thy/thm_database.ML Thy/thy_info.ML \
    7.26 +  Thy/thy_parse.ML Thy/thy_read.ML Thy/thy_scan.ML Thy/thy_syn.ML \
    7.27 +  Thy/use.ML axclass.ML basis.ML deriv.ML display.ML \
    7.28    drule.ML envir.ML goals.ML install_pp.ML library.ML locale.ML \
    7.29    logic.ML net.ML object_logic.ML pattern.ML pure.ML pure_thy.ML \
    7.30    search.ML sign.ML sorts.ML tactic.ML tctical.ML term.ML theory.ML \
     8.1 --- a/src/Pure/Syntax/README	Wed Jan 13 12:16:34 1999 +0100
     8.2 +++ b/src/Pure/Syntax/README	Wed Jan 13 12:44:33 1999 +0100
     8.3 @@ -4,12 +4,7 @@
     8.4  
     8.5  This directory contains the source files for Isabelle's syntax module,
     8.6  which includes a lexer, parser, pretty printer and macro system. Note
     8.7 -that only the following structures are supposed to be exported:
     8.8 -
     8.9 -  Pretty        (generic pretty printing module)
    8.10 -  Scan          (generic scanner toolbox)
    8.11 -  Source	(co-algebraic data sources)
    8.12 -  Symbol	(generalized characters)
    8.13 +that only the following structures are exported:
    8.14  
    8.15    Syntax        (internal interface to the syntax module)
    8.16    BasicSyntax   (part of Syntax made pervasive)
     9.1 --- a/src/Pure/Syntax/ROOT.ML	Wed Jan 13 12:16:34 1999 +0100
     9.2 +++ b/src/Pure/Syntax/ROOT.ML	Wed Jan 13 12:44:33 1999 +0100
     9.3 @@ -5,13 +5,6 @@
     9.4  This file builds the syntax module.
     9.5  *)
     9.6  
     9.7 -(*generic modules*)
     9.8 -use "scan.ML";
     9.9 -use "source.ML";
    9.10 -use "symbol.ML";
    9.11 -use "pretty.ML";
    9.12 -
    9.13 -(*actual syntax module*)
    9.14  use "lexicon.ML";
    9.15  use "token_trans.ML";
    9.16  use "ast.ML";
    10.1 --- a/src/Pure/Syntax/pretty.ML	Wed Jan 13 12:16:34 1999 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,249 +0,0 @@
    10.4 -(*  Title:      Pure/Syntax/pretty.ML
    10.5 -    ID:         $Id$
    10.6 -    Author:     Lawrence C Paulson
    10.7 -    Copyright   1991  University of Cambridge
    10.8 -
    10.9 -Generic pretty printing module.
   10.10 -
   10.11 -Loosely based on
   10.12 -  D. C. Oppen, "Pretty Printing",
   10.13 -  ACM Transactions on Programming Languages and Systems (1980), 465-483.
   10.14 -
   10.15 -The object to be printed is given as a tree with indentation and line
   10.16 -breaking information.  A "break" inserts a newline if the text until
   10.17 -the next break is too long to fit on the current line.  After the newline,
   10.18 -text is indented to the level of the enclosing block.  Normally, if a block
   10.19 -is broken then all enclosing blocks will also be broken.  Only "inconsistent
   10.20 -breaks" are provided.
   10.21 -
   10.22 -The stored length of a block is used in breakdist (to treat each inner block as
   10.23 -a unit for breaking).
   10.24 -*)
   10.25 -
   10.26 -type pprint_args = (string -> unit) * (int -> unit) * (int -> unit) *
   10.27 -  (unit -> unit) * (unit -> unit);
   10.28 -
   10.29 -signature PRETTY =
   10.30 -  sig
   10.31 -  type T
   10.32 -  val str: string -> T
   10.33 -  val strlen: string -> int -> T
   10.34 -  val sym: string -> T
   10.35 -  val spc: int -> T
   10.36 -  val brk: int -> T
   10.37 -  val fbrk: T
   10.38 -  val blk: int * T list -> T
   10.39 -  val lst: string * string -> T list -> T
   10.40 -  val quote: T -> T
   10.41 -  val commas: T list -> T list
   10.42 -  val breaks: T list -> T list
   10.43 -  val fbreaks: T list -> T list
   10.44 -  val block: T list -> T
   10.45 -  val strs: string list -> T
   10.46 -  val enclose: string -> string -> T list -> T
   10.47 -  val list: string -> string -> T list -> T
   10.48 -  val str_list: string -> string -> string list -> T
   10.49 -  val big_list: string -> T list -> T
   10.50 -  val string_of: T -> string
   10.51 -  val writeln: T -> unit
   10.52 -  val str_of: T -> string
   10.53 -  val pprint: T -> pprint_args -> unit
   10.54 -  val setdepth: int -> unit
   10.55 -  val setmargin: int -> unit
   10.56 -  end;
   10.57 -
   10.58 -structure Pretty : PRETTY =
   10.59 -struct
   10.60 -
   10.61 -(*printing items: compound phrases, strings, and breaks*)
   10.62 -datatype T =
   10.63 -  Block of T list * int * int |         (*body, indentation, length*)
   10.64 -  String of string * int |              (*text, length*)
   10.65 -  Break of bool * int;                  (*mandatory flag, width if not taken*);
   10.66 -
   10.67 -(*Add the lengths of the expressions until the next Break; if no Break then
   10.68 -  include "after", to account for text following this block. *)
   10.69 -fun breakdist (Block(_,_,len)::es, after) = len + breakdist(es, after)
   10.70 -  | breakdist (String (s, len) :: es, after) = len + breakdist (es, after)
   10.71 -  | breakdist (Break _ :: es, after) = 0
   10.72 -  | breakdist ([], after) = after;
   10.73 -
   10.74 -fun repstring a 0 = ""
   10.75 -  | repstring a 1 = a
   10.76 -  | repstring a k =
   10.77 -      if k mod 2 = 0 then repstring(a^a) (k div 2)
   10.78 -                     else repstring(a^a) (k div 2) ^ a;
   10.79 -
   10.80 -(*** Type for lines of text: string, # of lines, position on line ***)
   10.81 -
   10.82 -type text = {tx: string, nl: int, pos: int};
   10.83 -
   10.84 -val emptytext = {tx="", nl=0, pos=0};
   10.85 -
   10.86 -fun blanks wd {tx,nl,pos} =
   10.87 -    {tx  = tx ^ repstring " " wd,
   10.88 -     nl  = nl,
   10.89 -     pos = pos+wd};
   10.90 -
   10.91 -fun newline {tx,nl,pos} =
   10.92 -    {tx  = tx ^ "\n",
   10.93 -     nl  = nl+1,
   10.94 -     pos = 0};
   10.95 -
   10.96 -fun string s len {tx,nl,pos:int} =
   10.97 -    {tx  = tx ^ s,
   10.98 -     nl  = nl,
   10.99 -     pos = pos + len};
  10.100 -
  10.101 -
  10.102 -(*** Formatting ***)
  10.103 -
  10.104 -(* margin *)
  10.105 -
  10.106 -(*example values*)
  10.107 -val margin      = ref 80        (*right margin, or page width*)
  10.108 -and breakgain   = ref 4         (*minimum added space required of a break*)
  10.109 -and emergencypos = ref 40;      (*position too far to right*)
  10.110 -
  10.111 -fun setmargin m =
  10.112 -    (margin     := m;
  10.113 -     breakgain  := !margin div 20;
  10.114 -     emergencypos := !margin div 2);
  10.115 -
  10.116 -val () = setmargin 76;
  10.117 -
  10.118 -
  10.119 -(*Search for the next break (at this or higher levels) and force it to occur*)
  10.120 -fun forcenext [] = []
  10.121 -  | forcenext (Break(_,wd) :: es) = Break(true,0) :: es
  10.122 -  | forcenext (e :: es) = e :: forcenext es;
  10.123 -
  10.124 -(*es is list of expressions to print;
  10.125 -  blockin is the indentation of the current block;
  10.126 -  after is the width of the following context until next break. *)
  10.127 -fun format ([], _, _) text = text
  10.128 -  | format (e::es, blockin, after) (text as {pos,nl,...}) =
  10.129 -    (case e of
  10.130 -       Block(bes,indent,wd) =>
  10.131 -         let val blockin' = (pos + indent) mod !emergencypos
  10.132 -             val btext = format(bes, blockin', breakdist(es,after)) text
  10.133 -             (*If this block was broken then force the next break.*)
  10.134 -             val es2 = if nl < #nl(btext) then forcenext es else es
  10.135 -         in  format (es2,blockin,after) btext  end
  10.136 -     | String (s, len) => format (es,blockin,after) (string s len text)
  10.137 -     | Break(force,wd) => (*no break if text to next break fits on this line
  10.138 -                            or if breaking would add only breakgain to space *)
  10.139 -           format (es,blockin,after)
  10.140 -               (if not force andalso
  10.141 -                   pos+wd <= Int.max(!margin - breakdist(es,after),
  10.142 -                                     blockin + !breakgain)
  10.143 -                then blanks wd text  (*just insert wd blanks*)
  10.144 -                else blanks blockin (newline text)));
  10.145 -
  10.146 -
  10.147 -(*** Exported functions to create formatting expressions ***)
  10.148 -
  10.149 -fun length (Block (_, _, len)) = len
  10.150 -  | length (String (_, len)) = len
  10.151 -  | length (Break(_, wd)) = wd;
  10.152 -
  10.153 -fun str s = String (s, size s);
  10.154 -fun strlen s len = String (s, len);
  10.155 -fun sym s = String (s, Symbol.size s);
  10.156 -
  10.157 -fun spc n = str (repstring " " n);
  10.158 -
  10.159 -fun brk wd = Break (false, wd);
  10.160 -val fbrk = Break (true, 0);
  10.161 -
  10.162 -fun blk (indent, es) =
  10.163 -  let
  10.164 -    fun sum([], k) = k
  10.165 -      | sum(e :: es, k) = sum (es, length e + k);
  10.166 -  in Block (es, indent, sum (es, 0)) end;
  10.167 -
  10.168 -(*Join the elements of es as a comma-separated list, bracketted by lp and rp*)
  10.169 -fun lst(lp,rp) es =
  10.170 -  let fun add(e,es) = str"," :: brk 1 :: e :: es;
  10.171 -      fun list(e :: (es as _::_)) = str lp :: e :: foldr add (es,[str rp])
  10.172 -        | list(e::[]) = [str lp, e, str rp]
  10.173 -        | list([]) = []
  10.174 -  in blk(size lp, list es) end;
  10.175 -
  10.176 -
  10.177 -(* utils *)
  10.178 -
  10.179 -fun quote prt =
  10.180 -  blk (1, [str "\"", prt, str "\""]);
  10.181 -
  10.182 -fun commas prts =
  10.183 -  flat (separate [str ",", brk 1] (map (fn x => [x]) prts));
  10.184 -
  10.185 -fun breaks prts = separate (brk 1) prts;
  10.186 -
  10.187 -fun fbreaks prts = separate fbrk prts;
  10.188 -
  10.189 -fun block prts = blk (2, prts);
  10.190 -
  10.191 -val strs = block o breaks o (map str);
  10.192 -
  10.193 -fun enclose lpar rpar prts =
  10.194 -  block (str lpar :: (prts @ [str rpar]));
  10.195 -
  10.196 -fun list lpar rpar prts =
  10.197 -  enclose lpar rpar (commas prts);
  10.198 -
  10.199 -fun str_list lpar rpar strs =
  10.200 -  list lpar rpar (map str strs);
  10.201 -
  10.202 -fun big_list name prts =
  10.203 -  block (fbreaks (str name :: prts));
  10.204 -
  10.205 -
  10.206 -
  10.207 -(*** Pretty printing with depth limitation ***)
  10.208 -
  10.209 -val depth       = ref 0;        (*maximum depth; 0 means no limit*)
  10.210 -
  10.211 -fun setdepth dp = (depth := dp);
  10.212 -
  10.213 -(*Recursively prune blocks, discarding all text exceeding depth dp*)
  10.214 -fun pruning dp (Block(bes,indent,wd)) =
  10.215 -      if dp>0 then blk(indent, map (pruning(dp-1)) bes)
  10.216 -              else str "..."
  10.217 -  | pruning dp e = e;
  10.218 -
  10.219 -fun prune dp e = if dp>0 then pruning dp e else e;
  10.220 -
  10.221 -
  10.222 -fun string_of e = #tx (format ([prune (!depth) e], 0, 0) emptytext);
  10.223 -
  10.224 -val writeln = writeln o string_of;
  10.225 -
  10.226 -
  10.227 -(*Create a single flat string: no line breaking*)
  10.228 -fun str_of prt =
  10.229 -  let
  10.230 -    fun s_of (Block (prts, _, _)) = implode (map s_of prts)
  10.231 -      | s_of (String (s, _)) = s
  10.232 -      | s_of (Break (false, wd)) = repstring " " wd
  10.233 -      | s_of (Break (true, _)) = " ";
  10.234 -  in
  10.235 -    s_of (prune (! depth) prt)
  10.236 -  end;
  10.237 -
  10.238 -(*Part of the interface to the Poly/ML and New Jersey ML pretty printers*)
  10.239 -fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
  10.240 -  let
  10.241 -    fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
  10.242 -      | pp (String (s, _)) = put_str s
  10.243 -      | pp (Break (false, wd)) = put_brk wd
  10.244 -      | pp (Break (true, _)) = put_fbrk ()
  10.245 -    and pp_lst [] = ()
  10.246 -      | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
  10.247 -  in
  10.248 -    pp (prune (! depth) prt)
  10.249 -  end;
  10.250 -
  10.251 -
  10.252 -end;
    11.1 --- a/src/Pure/Syntax/scan.ML	Wed Jan 13 12:16:34 1999 +0100
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,305 +0,0 @@
    11.4 -(*  Title:	Pure/Syntax/scan.ML
    11.5 -    ID:		$Id$
    11.6 -    Author:	Markus Wenzel and Tobias Nipkow, TU Muenchen
    11.7 -
    11.8 -Generic scanners (for potentially infinite input).
    11.9 -*)
   11.10 -
   11.11 -infix 5 -- :-- |-- --| ^^;
   11.12 -infix 3 >>;
   11.13 -infix 0 ||;
   11.14 -
   11.15 -signature BASIC_SCAN =
   11.16 -sig
   11.17 -  val !! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b
   11.18 -  val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
   11.19 -  val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
   11.20 -  val -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
   11.21 -  val :-- : ('a -> 'b * 'c) * ('b -> 'c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
   11.22 -  val |-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e
   11.23 -  val --| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e
   11.24 -  val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c
   11.25 -  val $$ : ''a -> ''a list -> ''a * ''a list
   11.26 -end;
   11.27 -
   11.28 -signature SCAN =
   11.29 -sig
   11.30 -  include BASIC_SCAN
   11.31 -  val fail: 'a -> 'b
   11.32 -  val fail_with: ('a -> string) -> 'a -> 'b
   11.33 -  val succeed: 'a -> 'b -> 'a * 'b
   11.34 -  val one: ('a -> bool) -> 'a list -> 'a * 'a list
   11.35 -  val any: ('a -> bool) -> 'a list -> 'a list * 'a list
   11.36 -  val any1: ('a -> bool) -> 'a list -> 'a list * 'a list
   11.37 -  val optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a
   11.38 -  val option: ('a -> 'b * 'a) -> 'a -> 'b option * 'a
   11.39 -  val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
   11.40 -  val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
   11.41 -  val max: ('a * 'a -> bool) -> ('b -> 'a * 'b) -> ('b -> 'a * 'b) -> 'b -> 'a * 'b
   11.42 -  val ahead: ('a -> 'b * 'c) -> 'a -> 'b * 'a
   11.43 -  val unless: ('a -> 'b * 'a) -> ('a -> 'c * 'd) -> 'a -> 'c * 'd
   11.44 -  val first: ('a -> 'b) list -> 'a -> 'b
   11.45 -  val depend: ('a -> 'b -> ('c * 'd) * 'e) -> 'a * 'b -> 'd * ('c * 'e)
   11.46 -  val lift: ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c)
   11.47 -  val pass: 'a -> ('a * 'b -> 'c * ('d * 'e)) -> 'b -> 'c * 'e
   11.48 -  val try: ('a -> 'b) -> 'a -> 'b
   11.49 -  val force: ('a -> 'b) -> 'a -> 'b
   11.50 -  val prompt: string -> ('a -> 'b) -> 'a -> 'b
   11.51 -  val finite': 'a * ('a -> bool) -> ('b * 'a list -> 'c * ('d * 'a list))
   11.52 -    -> 'b * 'a list -> 'c * ('d * 'a list)
   11.53 -  val finite: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b * 'a list
   11.54 -  val read: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b option
   11.55 -  val catch: ('a -> 'b) -> 'a -> 'b
   11.56 -  val error: ('a -> 'b) -> 'a -> 'b
   11.57 -  val source': string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
   11.58 -    'b * ('b -> bool) -> ('d * 'b list -> 'e list * ('d * 'b list)) ->
   11.59 -    ('d * 'b list -> 'f * ('d * 'b list)) option -> 'd * 'a -> 'e list * ('d * 'c)
   11.60 -  val source: string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
   11.61 -    'b * ('b -> bool) -> ('b list -> 'd list * 'b list) ->
   11.62 -    ('b list -> 'e * 'b list) option -> 'a -> 'd list * 'c
   11.63 -  val single: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
   11.64 -  val bulk: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
   11.65 -  type lexicon
   11.66 -  val dest_lexicon: lexicon -> string list list
   11.67 -  val make_lexicon: string list list -> lexicon
   11.68 -  val empty_lexicon: lexicon
   11.69 -  val extend_lexicon: lexicon -> string list list -> lexicon
   11.70 -  val merge_lexicons: lexicon -> lexicon -> lexicon
   11.71 -  val literal: lexicon -> string list -> string list * string list
   11.72 -end;
   11.73 -
   11.74 -structure Scan: SCAN =
   11.75 -struct
   11.76 -
   11.77 -
   11.78 -(** scanners **)
   11.79 -
   11.80 -exception MORE of string option;	(*need more input (prompt)*)
   11.81 -exception FAIL of string option;	(*try alternatives (reason of failure)*)
   11.82 -exception ABORT of string;		(*dead end*)
   11.83 -
   11.84 -
   11.85 -(* scanner combinators *)
   11.86 -
   11.87 -fun (scan >> f) xs = apfst f (scan xs);
   11.88 -
   11.89 -fun (scan1 || scan2) xs = scan1 xs handle FAIL _ => scan2 xs;
   11.90 -
   11.91 -(*dependent pairing*)
   11.92 -fun (scan1 :-- scan2) xs =
   11.93 -  let
   11.94 -    val (x, ys) = scan1 xs;
   11.95 -    val (y, zs) = scan2 x ys;
   11.96 -  in ((x, y), zs) end;
   11.97 -
   11.98 -fun (scan1 -- scan2) = scan1 :-- (fn _ => scan2);
   11.99 -fun (scan1 |-- scan2) = scan1 -- scan2 >> #2;
  11.100 -fun (scan1 --| scan2) = scan1 -- scan2 >> #1;
  11.101 -fun (scan1 ^^ scan2) = scan1 -- scan2 >> op ^;
  11.102 -
  11.103 -
  11.104 -(* generic scanners *)
  11.105 -
  11.106 -fun fail _ = raise FAIL None;
  11.107 -fun fail_with msg_of xs = raise FAIL (Some (msg_of xs));
  11.108 -fun succeed y xs = (y, xs);
  11.109 -
  11.110 -fun one _ [] = raise MORE None
  11.111 -  | one pred (x :: xs) =
  11.112 -      if pred x then (x, xs) else raise FAIL None;
  11.113 -
  11.114 -fun $$ _ [] = raise MORE None
  11.115 -  | $$ a (x :: xs) =
  11.116 -      if a = x then (x, xs) else raise FAIL None;
  11.117 -
  11.118 -fun any _ [] = raise MORE None
  11.119 -  | any pred (lst as x :: xs) =
  11.120 -      if pred x then apfst (cons x) (any pred xs)
  11.121 -      else ([], lst);
  11.122 -
  11.123 -fun any1 pred = one pred -- any pred >> op ::;
  11.124 -
  11.125 -fun optional scan def = scan || succeed def;
  11.126 -fun option scan = optional (scan >> Some) None;
  11.127 -
  11.128 -fun repeat scan xs = (scan -- repeat scan >> op :: || succeed []) xs;
  11.129 -fun repeat1 scan = scan -- repeat scan >> op ::;
  11.130 -
  11.131 -fun max leq scan1 scan2 xs =
  11.132 -  (case (option scan1 xs, option scan2 xs) of
  11.133 -    ((None, _), (None, _)) => raise FAIL None		(*looses FAIL msg!*)
  11.134 -  | ((Some tok1, xs'), (None, _)) => (tok1, xs')
  11.135 -  | ((None, _), (Some tok2, xs')) => (tok2, xs')
  11.136 -  | ((Some tok1, xs1'), (Some tok2, xs2')) =>
  11.137 -      if leq (tok2, tok1) then (tok1, xs1') else (tok2, xs2'));
  11.138 -
  11.139 -fun ahead scan xs = (fst (scan xs), xs);
  11.140 -
  11.141 -fun unless test scan =
  11.142 -  ahead (option test) :-- (fn None => scan | _ => fail) >> #2;
  11.143 -
  11.144 -fun first [] = fail
  11.145 -  | first (scan :: scans) = scan || first scans;
  11.146 -
  11.147 -
  11.148 -(* state based scanners *)
  11.149 -
  11.150 -fun depend scan (st, xs) =
  11.151 -  let val ((st', y), xs') = scan st xs
  11.152 -  in (y, (st', xs')) end;
  11.153 -
  11.154 -fun lift scan (st, xs) =
  11.155 -  let val (y, xs') = scan xs
  11.156 -  in (y, (st, xs')) end;
  11.157 -
  11.158 -fun pass st scan xs =
  11.159 -  let val (y, (_, xs')) = scan (st, xs)
  11.160 -  in (y, xs') end;
  11.161 -
  11.162 -
  11.163 -(* exception handling *)
  11.164 -
  11.165 -fun !! err scan xs = scan xs handle FAIL msg => raise ABORT (err (xs, msg));
  11.166 -fun try scan xs = scan xs handle MORE _ => raise FAIL None | ABORT _ => raise FAIL None;
  11.167 -fun force scan xs = scan xs handle MORE _ => raise FAIL None;
  11.168 -fun prompt str scan xs = scan xs handle MORE None => raise MORE (Some str);
  11.169 -fun catch scan xs = scan xs handle ABORT msg => raise FAIL (Some msg);
  11.170 -fun error scan xs = scan xs handle ABORT msg => Library.error msg;
  11.171 -
  11.172 -
  11.173 -(* finite scans *)
  11.174 -
  11.175 -fun finite' (stopper, is_stopper) scan (state, input) =
  11.176 -  let
  11.177 -    fun lost () = raise ABORT "Scanner bug: lost stopper of finite scan!";
  11.178 -
  11.179 -    fun stop [] = lost ()
  11.180 -      | stop lst =
  11.181 -          let val (xs, x) = split_last lst
  11.182 -          in if is_stopper x then ((), xs) else lost () end;
  11.183 -  in
  11.184 -    if exists is_stopper input then
  11.185 -      raise ABORT "Stopper may not occur in input of finite scan!"
  11.186 -    else (force scan --| lift stop) (state, input @ [stopper])
  11.187 -  end;
  11.188 -
  11.189 -fun finite stopper scan xs =
  11.190 -  let val (y, ((), xs')) = finite' stopper (lift scan) ((), xs)
  11.191 -  in (y, xs') end;
  11.192 -
  11.193 -fun read stopper scan xs =
  11.194 -  (case error (finite stopper (option scan)) xs of
  11.195 -    (y as Some _, []) => y
  11.196 -  | _ => None);
  11.197 -
  11.198 -
  11.199 -
  11.200 -(* infinite scans -- draining state-based source *)
  11.201 -
  11.202 -fun drain def_prmpt get stopper scan ((state, xs), src) =
  11.203 -  (scan (state, xs), src) handle MORE prmpt =>
  11.204 -    (case get (if_none prmpt def_prmpt) src of
  11.205 -      ([], _) => (finite' stopper scan (state, xs), src)
  11.206 -    | (xs', src') => drain def_prmpt get stopper scan ((state, xs @ xs'), src'));
  11.207 -
  11.208 -fun source' def_prmpt get unget stopper scanner opt_recover (state, src) =
  11.209 -  let
  11.210 -    fun drain_with scan = drain def_prmpt get stopper scan;
  11.211 -
  11.212 -    fun drain_loop recover inp =
  11.213 -      drain_with (catch scanner) inp handle FAIL msg =>
  11.214 -        (error_msg (if_none msg "Syntax error.");
  11.215 -          drain_loop recover (apfst snd (drain_with recover inp)));
  11.216 -
  11.217 -    val ((ys, (state', xs')), src') =
  11.218 -      (case (get def_prmpt src, opt_recover) of
  11.219 -        (([], s), _) => (([], (state, [])), s)
  11.220 -      | ((xs, s), None) => drain_with (error scanner) ((state, xs), s)
  11.221 -      | ((xs, s), Some scan) => drain_loop scan ((state, xs), s));
  11.222 -  in
  11.223 -    (ys, (state', unget (xs', src')))
  11.224 -  end;
  11.225 -
  11.226 -fun source def_prmpt get unget stopper scan opt_recover src =
  11.227 -  let val (ys, ((), src')) =
  11.228 -    source' def_prmpt get unget stopper (lift scan) (apsome lift opt_recover) ((), src)
  11.229 -  in (ys, src') end;
  11.230 -
  11.231 -fun single scan = scan >> (fn x => [x]);
  11.232 -fun bulk scan = scan -- repeat (try scan) >> (op ::);
  11.233 -
  11.234 -
  11.235 -
  11.236 -(** datatype lexicon **)
  11.237 -
  11.238 -datatype lexicon =
  11.239 -  Empty |
  11.240 -  Branch of string * string list * lexicon * lexicon * lexicon;
  11.241 -
  11.242 -val no_literal = [];
  11.243 -
  11.244 -
  11.245 -(* dest_lexicon *)
  11.246 -
  11.247 -fun dest_lexicon Empty = []
  11.248 -  | dest_lexicon (Branch (_, [], lt, eq, gt)) =
  11.249 -      dest_lexicon lt @ dest_lexicon eq @ dest_lexicon gt
  11.250 -  | dest_lexicon (Branch (_, cs, lt, eq, gt)) =
  11.251 -      dest_lexicon lt @ [cs] @ dest_lexicon eq @ dest_lexicon gt;
  11.252 -
  11.253 -
  11.254 -(* empty, extend, make, merge lexicons *)
  11.255 -
  11.256 -val empty_lexicon = Empty;
  11.257 -
  11.258 -fun extend_lexicon lexicon chrss =
  11.259 -  let
  11.260 -    fun ext (lex, chrs) =
  11.261 -      let
  11.262 -	fun add (Branch (d, a, lt, eq, gt)) (chs as c :: cs) =
  11.263 -	      if c < d then Branch (d, a, add lt chs, eq, gt)
  11.264 -	      else if c > d then Branch (d, a, lt, eq, add gt chs)
  11.265 -	      else Branch (d, if null cs then chrs else a, lt, add eq cs, gt)
  11.266 -	  | add Empty [c] =
  11.267 -	      Branch (c, chrs, Empty, Empty, Empty)
  11.268 -	  | add Empty (c :: cs) =
  11.269 -	      Branch (c, no_literal, Empty, add Empty cs, Empty)
  11.270 -	  | add lex [] = lex;
  11.271 -      in add lex chrs end;
  11.272 -  in foldl ext (lexicon, chrss \\ dest_lexicon lexicon) end;
  11.273 -
  11.274 -val make_lexicon = extend_lexicon empty_lexicon;
  11.275 -
  11.276 -fun merge_lexicons lex1 lex2 =
  11.277 -  let
  11.278 -    val chss1 = dest_lexicon lex1;
  11.279 -    val chss2 = dest_lexicon lex2;
  11.280 -  in
  11.281 -    if chss2 subset chss1 then lex1
  11.282 -    else if chss1 subset chss2 then lex2
  11.283 -    else extend_lexicon lex1 chss2
  11.284 -  end;
  11.285 -
  11.286 -
  11.287 -(* scan literal *)
  11.288 -
  11.289 -fun literal lex chrs =
  11.290 -  let
  11.291 -    fun lit Empty res _ = res
  11.292 -      | lit (Branch _) _ [] = raise MORE None
  11.293 -      | lit (Branch (d, a, lt, eq, gt)) res (chs as c :: cs) =
  11.294 -	  if c < d then lit lt res chs
  11.295 -	  else if c > d then lit gt res chs
  11.296 -	  else lit eq (if a = no_literal then res else Some (a, cs)) cs;
  11.297 -  in
  11.298 -    (case lit lex None chrs of
  11.299 -      None => raise FAIL None
  11.300 -    | Some res => res)
  11.301 -  end;
  11.302 -
  11.303 -
  11.304 -end;
  11.305 -
  11.306 -
  11.307 -structure BasicScan: BASIC_SCAN = Scan;
  11.308 -open BasicScan;
    12.1 --- a/src/Pure/Syntax/source.ML	Wed Jan 13 12:16:34 1999 +0100
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,150 +0,0 @@
    12.4 -(*  Title:      Pure/Syntax/source.ML
    12.5 -    ID:         $Id$
    12.6 -    Author:     Markus Wenzel, TU Muenchen
    12.7 -
    12.8 -Co-algebraic data sources.
    12.9 -*)
   12.10 -
   12.11 -signature SOURCE =
   12.12 -sig
   12.13 -  type ('a, 'b) source
   12.14 -  val set_prompt: string -> ('a, 'b) source -> ('a, 'b) source
   12.15 -  val get: ('a, 'b) source -> 'a list * ('a, 'b) source
   12.16 -  val unget: 'a list * ('a, 'b) source -> ('a, 'b) source
   12.17 -  val get_single: ('a, 'b) source -> ('a * ('a, 'b) source) option
   12.18 -  val exhaust: ('a, 'b) source -> 'a list
   12.19 -  val mapfilter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) source) source
   12.20 -  val filter: ('a -> bool) -> ('a, 'b) source -> ('a, ('a, 'b) source) source
   12.21 -  val of_list: 'a list -> ('a, 'a list) source
   12.22 -  val of_string: string -> (string, string list) source
   12.23 -  val of_file: string -> (string, string list) source
   12.24 -  val decorate_prompt_fn: (string -> string) ref
   12.25 -  val of_stream: TextIO.instream -> TextIO.outstream -> (string, unit) source
   12.26 -  val tty: (string, unit) source
   12.27 -  val source': 'a -> 'b * ('b -> bool) -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
   12.28 -    ('a * 'b list -> 'd * ('a * 'b list)) option ->
   12.29 -    ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source
   12.30 -  val source: 'a * ('a -> bool) -> ('a list -> 'b list * 'a list) ->
   12.31 -    ('a list -> 'c * 'a list) option ->
   12.32 -    ('a, 'd) source -> ('b, ('a, 'd) source) source
   12.33 -end;
   12.34 -
   12.35 -structure Source: SOURCE =
   12.36 -struct
   12.37 -
   12.38 -
   12.39 -(** datatype source **)
   12.40 -
   12.41 -datatype ('a, 'b) source =
   12.42 -  Source of
   12.43 -   {buffer: 'a list,
   12.44 -    info: 'b,
   12.45 -    prompt: string,
   12.46 -    drain: string -> 'b -> 'a list * 'b};
   12.47 -
   12.48 -fun make_source buffer info prompt drain =
   12.49 -  Source {buffer = buffer, info = info, prompt = prompt, drain = drain};
   12.50 -
   12.51 -
   12.52 -(* prompt *)
   12.53 -
   12.54 -val default_prompt = "> ";
   12.55 -
   12.56 -fun set_prompt prompt (Source {buffer, info, prompt = _, drain}) =
   12.57 -  make_source buffer info prompt drain;
   12.58 -
   12.59 -
   12.60 -(* get / unget *)
   12.61 -
   12.62 -fun get (Source {buffer = [], info, prompt, drain}) =
   12.63 -      let val (xs, info') = drain prompt info
   12.64 -      in (xs, make_source [] info' prompt drain) end
   12.65 -  | get (Source {buffer, info, prompt, drain}) =
   12.66 -      (buffer, make_source [] info prompt drain);
   12.67 -
   12.68 -fun unget (xs, Source {buffer, info, prompt, drain}) =
   12.69 -  make_source (xs @ buffer) info prompt drain;
   12.70 -
   12.71 -
   12.72 -(* variations on get *)
   12.73 -
   12.74 -fun get_prompt prompt src = get (set_prompt prompt src);
   12.75 -
   12.76 -fun get_single src =
   12.77 -  (case get src of
   12.78 -    ([], _) => None
   12.79 -  | (x :: xs, src') => Some (x, unget (xs, src')));
   12.80 -
   12.81 -fun exhaust src =
   12.82 -  (case get src of
   12.83 -    ([], _) => []
   12.84 -  | (xs, src') => xs @ exhaust src');
   12.85 -
   12.86 -
   12.87 -(* (map)filter *)
   12.88 -
   12.89 -fun drain_mapfilter f prompt src =
   12.90 -  let
   12.91 -    val (xs, src') = get_prompt prompt src;
   12.92 -    val xs' = Library.mapfilter f xs;
   12.93 -  in
   12.94 -    if null xs orelse not (null xs') then (xs', src')
   12.95 -    else drain_mapfilter f prompt src'
   12.96 -  end;
   12.97 -
   12.98 -fun mapfilter f src = make_source [] src default_prompt (drain_mapfilter f);
   12.99 -fun filter pred = mapfilter (fn x => if pred x then Some x else None);
  12.100 -
  12.101 -
  12.102 -
  12.103 -(** build sources **)
  12.104 -
  12.105 -(* list source *)
  12.106 -
  12.107 -(*limiting the input buffer considerably improves performance*)
  12.108 -val limit = 4000;
  12.109 -
  12.110 -fun drain_list _ xs = (take (limit, xs), drop (limit, xs));
  12.111 -
  12.112 -fun of_list xs = make_source [] xs default_prompt drain_list;
  12.113 -val of_string = of_list o explode;
  12.114 -val of_file = of_string o File.read;
  12.115 -
  12.116 -
  12.117 -(* stream source *)
  12.118 -
  12.119 -val decorate_prompt_fn = ref (fn s:string => s);
  12.120 -
  12.121 -fun drain_stream instream outstream prompt () =
  12.122 -  (TextIO.output (outstream, ! decorate_prompt_fn prompt);
  12.123 -    TextIO.flushOut outstream;
  12.124 -    (explode (TextIO.inputLine instream), ()));
  12.125 -
  12.126 -fun of_stream instream outstream =
  12.127 -  make_source [] () default_prompt (drain_stream instream outstream);
  12.128 -
  12.129 -val tty = of_stream TextIO.stdIn TextIO.stdOut;
  12.130 -
  12.131 -
  12.132 -
  12.133 -(** compose sources **)
  12.134 -
  12.135 -fun drain_source source stopper scan recover prompt src =
  12.136 -  source prompt get_prompt unget stopper scan recover src;
  12.137 -
  12.138 -
  12.139 -(* state-based *)
  12.140 -
  12.141 -fun source' init_state stopper scan recover src =
  12.142 -  make_source [] (init_state, src) default_prompt
  12.143 -    (drain_source Scan.source' stopper scan recover);
  12.144 -
  12.145 -
  12.146 -(* non state-based *)
  12.147 -
  12.148 -fun source stopper scan recover src =
  12.149 -  make_source [] src default_prompt
  12.150 -    (drain_source Scan.source stopper scan recover);
  12.151 -
  12.152 -
  12.153 -end;
    13.1 --- a/src/Pure/Syntax/symbol.ML	Wed Jan 13 12:16:34 1999 +0100
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,274 +0,0 @@
    13.4 -(*  Title:      Pure/Syntax/symbol.ML
    13.5 -    ID:         $Id$
    13.6 -    Author:     Markus Wenzel, TU Muenchen
    13.7 -
    13.8 -Generalized characters.
    13.9 -*)
   13.10 -
   13.11 -signature SYMBOL =
   13.12 -sig
   13.13 -  type symbol
   13.14 -  val space: symbol
   13.15 -  val eof: symbol
   13.16 -  val is_eof: symbol -> bool
   13.17 -  val not_eof: symbol -> bool
   13.18 -  val stopper: symbol * (symbol -> bool)
   13.19 -  val is_ascii: symbol -> bool
   13.20 -  val is_letter: symbol -> bool
   13.21 -  val is_digit: symbol -> bool
   13.22 -  val is_quasi_letter: symbol -> bool
   13.23 -  val is_letdig: symbol -> bool
   13.24 -  val is_blank: symbol -> bool
   13.25 -  val is_printable: symbol -> bool
   13.26 -  val beginning: symbol list -> string
   13.27 -  val scan: string list -> symbol * string list
   13.28 -  val explode: string -> symbol list
   13.29 -  val length: symbol list -> int
   13.30 -  val size: string -> int
   13.31 -  val input: string -> string
   13.32 -  val output: string -> string
   13.33 -  val source: bool -> (string, 'a) Source.source ->
   13.34 -    (symbol, (string, 'a) Source.source) Source.source
   13.35 -end;
   13.36 -
   13.37 -structure Symbol: SYMBOL =
   13.38 -struct
   13.39 -
   13.40 -
   13.41 -(** encoding table (isabelle-0) **)
   13.42 -
   13.43 -val enc_start = 160;
   13.44 -val enc_end = 255;
   13.45 -
   13.46 -val enc_vector =
   13.47 -[
   13.48 -(* GENERATED TEXT FOLLOWS - Do not edit! *)
   13.49 -  "\\<space2>",
   13.50 -  "\\<Gamma>",
   13.51 -  "\\<Delta>",
   13.52 -  "\\<Theta>",
   13.53 -  "\\<Lambda>",
   13.54 -  "\\<Pi>",
   13.55 -  "\\<Sigma>",
   13.56 -  "\\<Phi>",
   13.57 -  "\\<Psi>",
   13.58 -  "\\<Omega>",
   13.59 -  "\\<alpha>",
   13.60 -  "\\<beta>",
   13.61 -  "\\<gamma>",
   13.62 -  "\\<delta>",
   13.63 -  "\\<epsilon>",
   13.64 -  "\\<zeta>",
   13.65 -  "\\<eta>",
   13.66 -  "\\<theta>",
   13.67 -  "\\<kappa>",
   13.68 -  "\\<lambda>",
   13.69 -  "\\<mu>",
   13.70 -  "\\<nu>",
   13.71 -  "\\<xi>",
   13.72 -  "\\<pi>",
   13.73 -  "\\<rho>",
   13.74 -  "\\<sigma>",
   13.75 -  "\\<tau>",
   13.76 -  "\\<phi>",
   13.77 -  "\\<chi>",
   13.78 -  "\\<psi>",
   13.79 -  "\\<omega>",
   13.80 -  "\\<not>",
   13.81 -  "\\<and>",
   13.82 -  "\\<or>",
   13.83 -  "\\<forall>",
   13.84 -  "\\<exists>",
   13.85 -  "\\<And>",
   13.86 -  "\\<lceil>",
   13.87 -  "\\<rceil>",
   13.88 -  "\\<lfloor>",
   13.89 -  "\\<rfloor>",
   13.90 -  "\\<turnstile>",
   13.91 -  "\\<Turnstile>",
   13.92 -  "\\<lbrakk>",
   13.93 -  "\\<rbrakk>",
   13.94 -  "\\<cdot>",
   13.95 -  "\\<in>",
   13.96 -  "\\<subseteq>",
   13.97 -  "\\<inter>",
   13.98 -  "\\<union>",
   13.99 -  "\\<Inter>",
  13.100 -  "\\<Union>",
  13.101 -  "\\<sqinter>",
  13.102 -  "\\<squnion>",
  13.103 -  "\\<Sqinter>",
  13.104 -  "\\<Squnion>",
  13.105 -  "\\<bottom>",
  13.106 -  "\\<doteq>",
  13.107 -  "\\<equiv>",
  13.108 -  "\\<noteq>",
  13.109 -  "\\<sqsubset>",
  13.110 -  "\\<sqsubseteq>",
  13.111 -  "\\<prec>",
  13.112 -  "\\<preceq>",
  13.113 -  "\\<succ>",
  13.114 -  "\\<approx>",
  13.115 -  "\\<sim>",
  13.116 -  "\\<simeq>",
  13.117 -  "\\<le>",
  13.118 -  "\\<Colon>",
  13.119 -  "\\<leftarrow>",
  13.120 -  "\\<midarrow>",
  13.121 -  "\\<rightarrow>",
  13.122 -  "\\<Leftarrow>",
  13.123 -  "\\<Midarrow>",
  13.124 -  "\\<Rightarrow>",
  13.125 -  "\\<bow>",
  13.126 -  "\\<mapsto>",
  13.127 -  "\\<leadsto>",
  13.128 -  "\\<up>",
  13.129 -  "\\<down>",
  13.130 -  "\\<notin>",
  13.131 -  "\\<times>",
  13.132 -  "\\<oplus>",
  13.133 -  "\\<ominus>",
  13.134 -  "\\<otimes>",
  13.135 -  "\\<oslash>",
  13.136 -  "\\<subset>",
  13.137 -  "\\<infinity>",
  13.138 -  "\\<box>",
  13.139 -  "\\<diamond>",
  13.140 -  "\\<circ>",
  13.141 -  "\\<bullet>",
  13.142 -  "\\<parallel>",
  13.143 -  "\\<surd>",
  13.144 -  "\\<copyright>"
  13.145 -(* END OF GENERATED TEXT *)
  13.146 -];
  13.147 -
  13.148 -val enc_rel = enc_vector ~~ map chr (enc_start upto enc_end);
  13.149 -
  13.150 -val char_tab = Symtab.make enc_rel;
  13.151 -val symbol_tab = Symtab.make (map swap enc_rel);
  13.152 -
  13.153 -fun lookup_symbol c =
  13.154 -  if ord c < enc_start then None
  13.155 -  else Symtab.lookup (symbol_tab, c);
  13.156 -
  13.157 -
  13.158 -(* encode / decode *)
  13.159 -
  13.160 -fun char s = if_none (Symtab.lookup (char_tab, s)) s;
  13.161 -fun symbol c = if_none (lookup_symbol c) c;
  13.162 -
  13.163 -fun symbol' c =
  13.164 -  (case lookup_symbol c of
  13.165 -    None => c
  13.166 -  | Some s => "\\" ^ s);
  13.167 -
  13.168 -
  13.169 -
  13.170 -(** type symbol **)
  13.171 -
  13.172 -type symbol = string;
  13.173 -
  13.174 -val space = " ";
  13.175 -val eof = "";
  13.176 -
  13.177 -
  13.178 -(* kinds *)
  13.179 -
  13.180 -fun is_eof s = s = eof;
  13.181 -fun not_eof s = s <> eof;
  13.182 -val stopper = (eof, is_eof);
  13.183 -
  13.184 -fun is_ascii s = size s = 1 andalso ord s < 128;
  13.185 -
  13.186 -fun is_letter s =
  13.187 -  size s = 1 andalso
  13.188 -   (ord "A" <= ord s andalso ord s <= ord "Z" orelse
  13.189 -    ord "a" <= ord s andalso ord s <= ord "z");
  13.190 -
  13.191 -fun is_digit s =
  13.192 -  size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9";
  13.193 -
  13.194 -fun is_quasi_letter "_" = true
  13.195 -  | is_quasi_letter "'" = true
  13.196 -  | is_quasi_letter s = is_letter s;
  13.197 -
  13.198 -val is_blank =
  13.199 -  fn " " => true | "\t" => true | "\n" => true | "\^L" => true
  13.200 -    | "\160" => true | "\\<space2>" => true
  13.201 -    | _ => false;
  13.202 -
  13.203 -val is_letdig = is_quasi_letter orf is_digit;
  13.204 -
  13.205 -fun is_printable s =
  13.206 -  size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" orelse
  13.207 -  size s > 2 andalso nth_elem (2, explode s) <> "^";
  13.208 -
  13.209 -
  13.210 -(* beginning *)
  13.211 -
  13.212 -val smash_blanks = map (fn s => if is_blank s then space else s);
  13.213 -
  13.214 -fun beginning raw_ss =
  13.215 -  let
  13.216 -    val (all_ss, _) = take_suffix is_blank raw_ss;
  13.217 -    val dots = if length all_ss > 10 then " ..." else "";
  13.218 -    val (ss, _) = take_suffix is_blank (take (10, all_ss));
  13.219 -  in implode (smash_blanks ss) ^ dots end;
  13.220 -
  13.221 -
  13.222 -(* scan *)
  13.223 -
  13.224 -val scan_id = Scan.one is_letter ^^ (Scan.any is_letdig >> implode);
  13.225 -
  13.226 -val scan =
  13.227 -  ($$ "\\" --| Scan.optional ($$ "\\") "") ^^ $$ "<" ^^
  13.228 -    !! (fn (cs, _) => "Malformed symbolic character specification: \\" ^ "<" ^ beginning cs)
  13.229 -      (Scan.optional ($$ "^") "" ^^ scan_id ^^ $$ ">") ||
  13.230 -  Scan.one not_eof;
  13.231 -
  13.232 -
  13.233 -(* source *)
  13.234 -
  13.235 -val recover = Scan.any1 ((not o is_blank) andf not_eof);
  13.236 -
  13.237 -fun source do_recover src =
  13.238 -  Source.source stopper (Scan.bulk scan) (if do_recover then Some recover else None) src;
  13.239 -
  13.240 -
  13.241 -(* explode *)
  13.242 -
  13.243 -fun no_syms [] = true
  13.244 -  | no_syms ("\\" :: "<" :: _) = false
  13.245 -  | no_syms (c :: cs) = ord c < enc_start andalso no_syms cs;
  13.246 -
  13.247 -fun sym_explode str =
  13.248 -  let val chs = explode str in
  13.249 -    if no_syms chs then chs     (*tune trivial case*)
  13.250 -    else map symbol (the (Scan.read stopper (Scan.repeat scan) chs))
  13.251 -  end;
  13.252 -
  13.253 -
  13.254 -(* printable length *)
  13.255 -
  13.256 -fun sym_length ss = foldl (fn (n, c) => if is_printable c then n + 1 else n) (0, ss);
  13.257 -val sym_size = sym_length o sym_explode;
  13.258 -
  13.259 -
  13.260 -(* input / output *)
  13.261 -
  13.262 -fun input str =
  13.263 -  let val chs = explode str in
  13.264 -    if forall (fn c => ord c < enc_start) chs then str
  13.265 -    else implode (map symbol' chs)
  13.266 -  end;
  13.267 -
  13.268 -val output = implode o map char o sym_explode;
  13.269 -
  13.270 -
  13.271 -(*final declarations of this structure!*)
  13.272 -val explode = sym_explode;
  13.273 -val length = sym_length;
  13.274 -val size = sym_size;
  13.275 -
  13.276 -
  13.277 -end;