equal
deleted
inserted
replaced
1 (* Title: Pure/context_position.ML |
|
2 ID: $Id$ |
|
3 Author: Makarius |
|
4 |
|
5 Context positions. |
|
6 *) |
|
7 |
|
8 signature CONTEXT_POSITION = |
|
9 sig |
|
10 val put: Position.T -> Context.generic -> Context.generic |
|
11 val put_ctxt: Position.T -> Proof.context -> Proof.context |
|
12 val get: Proof.context -> Position.T |
|
13 val str_of: Proof.context -> string |
|
14 val properties_of: Proof.context -> Markup.property list |
|
15 end; |
|
16 |
|
17 structure ContextPosition: CONTEXT_POSITION = |
|
18 struct |
|
19 |
|
20 structure Data = GenericDataFun |
|
21 ( |
|
22 type T = Position.T; |
|
23 val empty = Position.none; |
|
24 fun extend _ = empty; |
|
25 fun merge _ _ = empty; |
|
26 ); |
|
27 |
|
28 val put = Data.put; |
|
29 val put_ctxt = Context.proof_map o put; |
|
30 |
|
31 val get = Data.get o Context.Proof; |
|
32 val str_of = Position.str_of o get; |
|
33 val properties_of = Position.properties_of o get; |
|
34 |
|
35 end; |
|