isabelle: src/Pure/ML/exn_properties_dummy.ML@4194901fd513 (annotated)

50911 ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset; wenzelm parents: diff changeset	1	(* Title: Pure/ML/exn_properties_dummy.ML
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset; wenzelm parents: diff changeset	2	Author: Makarius
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset; wenzelm parents: diff changeset	3
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset; wenzelm parents: diff changeset	4	Exception properties -- dummy version.
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset; wenzelm parents: diff changeset	5	*)
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset; wenzelm parents: diff changeset	6
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset; wenzelm parents: diff changeset	7	signature EXN_PROPERTIES =
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset; wenzelm parents: diff changeset	8	sig
60865 4194901fd513 make SML/NJ work; wenzelm parents: 50911 diff changeset	9	val position_of: 'location -> Position.T
50911 ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset; wenzelm parents: diff changeset	10	val get: exn -> Properties.T
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset; wenzelm parents: diff changeset	11	val update: Properties.entry list -> exn -> exn
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset; wenzelm parents: diff changeset	12	end;
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset; wenzelm parents: diff changeset	13
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset; wenzelm parents: diff changeset	14	structure Exn_Properties: EXN_PROPERTIES =
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset; wenzelm parents: diff changeset	15	struct
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset; wenzelm parents: diff changeset	16
60865 4194901fd513 make SML/NJ work; wenzelm parents: 50911 diff changeset	17	fun position_of _ = Position.none;
4194901fd513 make SML/NJ work; wenzelm parents: 50911 diff changeset	18
50911 ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset; wenzelm parents: diff changeset	19	fun get _ = [];
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset; wenzelm parents: diff changeset	20	fun update _ exn = exn;
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset; wenzelm parents: diff changeset	21
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset; wenzelm parents: diff changeset	22	end;
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset; wenzelm parents: diff changeset	23

author	wenzelm
	Fri, 07 Aug 2015 17:58:12 +0200
changeset 60865	4194901fd513
parent 50911	ee7fe4230642
permissions	-rw-r--r--