src/Pure/context_position.ML
author wenzelm
Mon Oct 01 15:14:53 2007 +0200 (2007-10-01)
changeset 24791 fb1830099265
parent 24773 ec3a04e6f1a9
permissions -rw-r--r--
turned into generic context data;
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@24791
    10
  val put: Position.T -> Context.generic -> Context.generic
wenzelm@24791
    11
  val put_ctxt: Position.T -> Proof.context -> Proof.context
wenzelm@23354
    12
  val get: Proof.context -> Position.T
wenzelm@23354
    13
  val str_of: Proof.context -> string
wenzelm@24773
    14
  val properties_of: Proof.context -> Markup.property list
wenzelm@23354
    15
end;
wenzelm@23354
    16
wenzelm@23354
    17
structure ContextPosition: CONTEXT_POSITION =
wenzelm@23354
    18
struct
wenzelm@23354
    19
wenzelm@24791
    20
structure Data = GenericDataFun
wenzelm@23354
    21
(
wenzelm@23354
    22
  type T = Position.T;
wenzelm@24791
    23
  val empty = Position.none;
wenzelm@24791
    24
  fun extend _ = empty;
wenzelm@24791
    25
  fun merge _ _ = empty;
wenzelm@23354
    26
);
wenzelm@23354
    27
wenzelm@23354
    28
val put = Data.put;
wenzelm@24791
    29
val put_ctxt = Context.proof_map o put;
wenzelm@24791
    30
wenzelm@24791
    31
val get = Data.get o Context.Proof;
wenzelm@23354
    32
val str_of = Position.str_of o get;
wenzelm@24773
    33
val properties_of = Position.properties_of o get;
wenzelm@23354
    34
wenzelm@23354
    35
end;