isabelle: src/Pure/section_utils.ML@840c75ab2a7f (annotated)

579 08f465e23dc5 new file of useful things for writing theory sections lcp parents: diff changeset	1
7744 f27d54c1ef39 got rid of most; wenzelm parents: 6390 diff changeset	2	(* FIXME get rid of this!! *)
579 08f465e23dc5 new file of useful things for writing theory sections lcp parents: diff changeset	3
08f465e23dc5 new file of useful things for writing theory sections lcp parents: diff changeset	4
1390 bf523422a3df Commented and renamed vars in readtm paulson parents: 654 diff changeset	5	(Read a term from string "b", with expected type T)
bf523422a3df Commented and renamed vars in readtm paulson parents: 654 diff changeset	6	fun readtm sign T b =
bf523422a3df Commented and renamed vars in readtm paulson parents: 654 diff changeset	7	read_cterm sign (b,T) \|> term_of
3536 8fb4150e2ad3 tuned error propagation msg; wenzelm parents: 2863 diff changeset	8	handle ERROR => error ("The error(s) above occurred for " ^ b);
579 08f465e23dc5 new file of useful things for writing theory sections lcp parents: diff changeset	9
7744 f27d54c1ef39 got rid of most; wenzelm parents: 6390 diff changeset	10
f27d54c1ef39 got rid of most; wenzelm parents: 6390 diff changeset	11	(* FIXME broken! *)
579 08f465e23dc5 new file of useful things for writing theory sections lcp parents: diff changeset	12
7744 f27d54c1ef39 got rid of most; wenzelm parents: 6390 diff changeset	13	(Skipping initial blanks, find the first identifier)
f27d54c1ef39 got rid of most; wenzelm parents: 6390 diff changeset	14	fun scan_to_id s =
4695 6aa25ee18fc4 adapted to new scanners and baroque chars; wenzelm parents: 3974 diff changeset	15	s \|> Symbol.explode
4938 c8bbbf3c59fa Symbol.stopper; wenzelm parents: 4848 diff changeset	16	\|> Scan.error (Scan.finite Symbol.stopper
4695 6aa25ee18fc4 adapted to new scanners and baroque chars; wenzelm parents: 3974 diff changeset	17	(!! (fn _ => "Expected to find an identifier in " ^ s)
6aa25ee18fc4 adapted to new scanners and baroque chars; wenzelm parents: 3974 diff changeset	18	(Scan.any Symbol.is_blank \|-- Syntax.scan_id)))
6aa25ee18fc4 adapted to new scanners and baroque chars; wenzelm parents: 3974 diff changeset	19	\|> #1;

author	wenzelm
	Mon, 17 Apr 2000 13:57:55 +0200
changeset 8720	840c75ab2a7f
parent 7744	f27d54c1ef39
permissions	-rw-r--r--