src/Pure/context_position.ML
author wenzelm
Mon, 01 Oct 2007 15:14:53 +0200
changeset 24791 fb1830099265
parent 24773 ec3a04e6f1a9
permissions -rw-r--r--
turned into generic context data;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23354
a189707c1d76 Context positions.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/context_position.ML
a189707c1d76 Context positions.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
a189707c1d76 Context positions.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
a189707c1d76 Context positions.
wenzelm
parents:
diff changeset
     4
a189707c1d76 Context positions.
wenzelm
parents:
diff changeset
     5
Context positions.
a189707c1d76 Context positions.
wenzelm
parents:
diff changeset
     6
*)
a189707c1d76 Context positions.
wenzelm
parents:
diff changeset
     7
a189707c1d76 Context positions.
wenzelm
parents:
diff changeset
     8
signature CONTEXT_POSITION =
a189707c1d76 Context positions.
wenzelm
parents:
diff changeset
     9
sig
24791
fb1830099265 turned into generic context data;
wenzelm
parents: 24773
diff changeset
    10
  val put: Position.T -> Context.generic -> Context.generic
fb1830099265 turned into generic context data;
wenzelm
parents: 24773
diff changeset
    11
  val put_ctxt: Position.T -> Proof.context -> Proof.context
23354
a189707c1d76 Context positions.
wenzelm
parents:
diff changeset
    12
  val get: Proof.context -> Position.T
a189707c1d76 Context positions.
wenzelm
parents:
diff changeset
    13
  val str_of: Proof.context -> string
24773
ec3a04e6f1a9 added properties_of;
wenzelm
parents: 23354
diff changeset
    14
  val properties_of: Proof.context -> Markup.property list
23354
a189707c1d76 Context positions.
wenzelm
parents:
diff changeset
    15
end;
a189707c1d76 Context positions.
wenzelm
parents:
diff changeset
    16
a189707c1d76 Context positions.
wenzelm
parents:
diff changeset
    17
structure ContextPosition: CONTEXT_POSITION =
a189707c1d76 Context positions.
wenzelm
parents:
diff changeset
    18
struct
a189707c1d76 Context positions.
wenzelm
parents:
diff changeset
    19
24791
fb1830099265 turned into generic context data;
wenzelm
parents: 24773
diff changeset
    20
structure Data = GenericDataFun
23354
a189707c1d76 Context positions.
wenzelm
parents:
diff changeset
    21
(
a189707c1d76 Context positions.
wenzelm
parents:
diff changeset
    22
  type T = Position.T;
24791
fb1830099265 turned into generic context data;
wenzelm
parents: 24773
diff changeset
    23
  val empty = Position.none;
fb1830099265 turned into generic context data;
wenzelm
parents: 24773
diff changeset
    24
  fun extend _ = empty;
fb1830099265 turned into generic context data;
wenzelm
parents: 24773
diff changeset
    25
  fun merge _ _ = empty;
23354
a189707c1d76 Context positions.
wenzelm
parents:
diff changeset
    26
);
a189707c1d76 Context positions.
wenzelm
parents:
diff changeset
    27
a189707c1d76 Context positions.
wenzelm
parents:
diff changeset
    28
val put = Data.put;
24791
fb1830099265 turned into generic context data;
wenzelm
parents: 24773
diff changeset
    29
val put_ctxt = Context.proof_map o put;
fb1830099265 turned into generic context data;
wenzelm
parents: 24773
diff changeset
    30
fb1830099265 turned into generic context data;
wenzelm
parents: 24773
diff changeset
    31
val get = Data.get o Context.Proof;
23354
a189707c1d76 Context positions.
wenzelm
parents:
diff changeset
    32
val str_of = Position.str_of o get;
24773
ec3a04e6f1a9 added properties_of;
wenzelm
parents: 23354
diff changeset
    33
val properties_of = Position.properties_of o get;
23354
a189707c1d76 Context positions.
wenzelm
parents:
diff changeset
    34
a189707c1d76 Context positions.
wenzelm
parents:
diff changeset
    35
end;