files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
authorwenzelm
Wed, 13 Jan 1999 12:44:33 +0100
changeset 6116 8ba2f25610f7
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
--- /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;