src/Pure/context_position.ML
author wenzelm
Sun, 08 Jul 2007 19:51:58 +0200
changeset 23655 d2d1138e0ddc
parent 23354 a189707c1d76
child 24773 ec3a04e6f1a9
permissions -rw-r--r--
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;

(*  Title:      Pure/context_position.ML
    ID:         $Id$
    Author:     Makarius

Context positions.
*)

signature CONTEXT_POSITION =
sig
  val put: Position.T -> Proof.context -> Proof.context
  val get: Proof.context -> Position.T
  val str_of: Proof.context -> string
end;

structure ContextPosition: CONTEXT_POSITION =
struct

structure Data = ProofDataFun
(
  type T = Position.T;
  fun init _ = Position.none;
);

val put = Data.put;
val get = Data.get;
val str_of = Position.str_of o get;

end;