src/Pure/context_position.ML

pass explicit target record -- more informative peek operation;
removed obsolete hide_abbrev;
misc tuning;

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

Context positions.
*)

signature CONTEXT_POSITION =
sig
  val put: Position.T -> Context.generic -> Context.generic
  val put_ctxt: Position.T -> Proof.context -> Proof.context
  val get: Proof.context -> Position.T
  val str_of: Proof.context -> string
  val properties_of: Proof.context -> Markup.property list
end;

structure ContextPosition: CONTEXT_POSITION =
struct

structure Data = GenericDataFun
(
  type T = Position.T;
  val empty = Position.none;
  fun extend _ = empty;
  fun merge _ _ = empty;
);

val put = Data.put;
val put_ctxt = Context.proof_map o put;

val get = Data.get o Context.Proof;
val str_of = Position.str_of o get;
val properties_of = Position.properties_of o get;

end;