author | wenzelm |
Fri, 01 Jan 2016 16:40:47 +0100 | |
changeset 62028 | 2ecee4679f99 |
parent 60865 | 4194901fd513 |
permissions | -rw-r--r-- |
(* Title: Pure/ML/exn_properties_dummy.ML Author: Makarius Exception properties -- dummy version. *) signature EXN_PROPERTIES = sig val position_of: 'location -> Position.T val get: exn -> Properties.T val update: Properties.entry list -> exn -> exn end; structure Exn_Properties: EXN_PROPERTIES = struct fun position_of _ = Position.none; fun get _ = []; fun update _ exn = exn; end;