src/Pure/section_utils.ML
author paulson
Mon, 28 Dec 1998 16:48:22 +0100
changeset 6039 01f67f5f8dd0
parent 4938 c8bbbf3c59fa
child 6390 5d58c100ca3f
permissions -rw-r--r--
deleted "escape" and "trim"; Basis Library can do string escapes if necessary

(*  Title: 	Pure/section_utils.ML
    ID:         $Id$
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1994  University of Cambridge

Utilities for writing new theory sections.
*)

fun ap t u = t$u;
fun app t (u1,u2) = t $ u1 $ u2;

(*Make distinct individual variables a1, a2, a3, ..., an. *)
fun mk_frees a [] = []
  | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;


(*Read an assumption in the given theory*)
fun assume_read thy a = Thm.assume (read_cterm (sign_of thy) (a,propT));

(*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);

(*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
  | tryres (th, []) = raise THM("tryres", 0, [th]);

fun gen_make_elim elim_rls rl = 
      standard (tryres (rl, elim_rls @ [revcut_rl]));

(** String manipulation **)

(*Skipping initial blanks, find the first identifier*)	(* FIXME *)
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;

fun is_backslash c = c = "\\";