src/Pure/context_position.ML
author wenzelm
Wed Jun 13 00:01:57 2007 +0200 (2007-06-13)
changeset 23354 a189707c1d76
child 24773 ec3a04e6f1a9
permissions -rw-r--r--
Context positions.
wenzelm@23354
     1
(*  Title:      Pure/context_position.ML
wenzelm@23354
     2
    ID:         $Id$
wenzelm@23354
     3
    Author:     Makarius
wenzelm@23354
     4
wenzelm@23354
     5
Context positions.
wenzelm@23354
     6
*)
wenzelm@23354
     7
wenzelm@23354
     8
signature CONTEXT_POSITION =
wenzelm@23354
     9
sig
wenzelm@23354
    10
  val put: Position.T -> Proof.context -> Proof.context
wenzelm@23354
    11
  val get: Proof.context -> Position.T
wenzelm@23354
    12
  val str_of: Proof.context -> string
wenzelm@23354
    13
end;
wenzelm@23354
    14
wenzelm@23354
    15
structure ContextPosition: CONTEXT_POSITION =
wenzelm@23354
    16
struct
wenzelm@23354
    17
wenzelm@23354
    18
structure Data = ProofDataFun
wenzelm@23354
    19
(
wenzelm@23354
    20
  type T = Position.T;
wenzelm@23354
    21
  fun init _ = Position.none;
wenzelm@23354
    22
);
wenzelm@23354
    23
wenzelm@23354
    24
val put = Data.put;
wenzelm@23354
    25
val get = Data.get;
wenzelm@23354
    26
val str_of = Position.str_of o get;
wenzelm@23354
    27
wenzelm@23354
    28
end;