isabelle: src/Pure/ML/exn_properties_dummy.ML@87f0f707a5f8 (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
	Sun, 16 Aug 2015 23:14:27 +0200
changeset 60953	87f0f707a5f8
parent 60865	4194901fd513
permissions	-rw-r--r--