src/Pure/ML/exn_properties_dummy.ML
author wenzelm
Thu, 04 Apr 2013 18:20:00 +0200
changeset 51618 a3577cd80c41
parent 50911 ee7fe4230642
child 60865 4194901fd513
permissions -rw-r--r--
tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;

(*  Title:      Pure/ML/exn_properties_dummy.ML
    Author:     Makarius

Exception properties -- dummy version.
*)

signature EXN_PROPERTIES =
sig
  val get: exn -> Properties.T
  val update: Properties.entry list -> exn -> exn
end;

structure Exn_Properties: EXN_PROPERTIES =
struct

fun get _ = [];
fun update _ exn = exn;

end;