author | paulson |
Fri, 18 Feb 2000 15:35:29 +0100 | |
changeset 8255 | 38f96394c099 |
parent 7744 | f27d54c1ef39 |
permissions | -rw-r--r-- |
(* FIXME get rid of this!! *) (*Read a term from string "b", with expected type T*) fun readtm sign T b = read_cterm sign (b,T) |> term_of handle ERROR => error ("The error(s) above occurred for " ^ b); (* FIXME broken! *) (*Skipping initial blanks, find the first identifier*) fun scan_to_id s = s |> Symbol.explode |> Scan.error (Scan.finite Symbol.stopper (!! (fn _ => "Expected to find an identifier in " ^ s) (Scan.any Symbol.is_blank |-- Syntax.scan_id))) |> #1;