equal
deleted
inserted
replaced
33 val morph_values: morphism -> src -> src |
33 val morph_values: morphism -> src -> src |
34 val maxidx_values: src -> int -> int |
34 val maxidx_values: src -> int -> int |
35 val assignable: src -> src |
35 val assignable: src -> src |
36 val assign: value option -> T -> unit |
36 val assign: value option -> T -> unit |
37 val closure: src -> src |
37 val closure: src -> src |
|
38 val context: Context.generic * T list -> Context.proof * (Context.generic * T list) |
|
39 val theory: Context.generic * T list -> Context.theory * (Context.generic * T list) |
38 val position: (T list -> 'a * 'b) -> T list -> ('a * Position.T) * 'b |
40 val position: (T list -> 'a * 'b) -> T list -> ('a * Position.T) * 'b |
39 val !!! : (T list -> 'a) -> T list -> 'a |
41 val !!! : (T list -> 'a) -> T list -> 'a |
40 val $$$ : string -> T list -> string * T list |
42 val $$$ : string -> T list -> string * T list |
41 val add: T list -> string * T list |
43 val add: T list -> string * T list |
42 val del: T list -> string * T list |
44 val del: T list -> string * T list |
222 |
224 |
223 |
225 |
224 |
226 |
225 (** scanners **) |
227 (** scanners **) |
226 |
228 |
|
229 (* context *) |
|
230 |
|
231 fun context x = (Scan.state >> Context.proof_of) x; |
|
232 fun theory x = (Scan.state >> Context.theory_of) x; |
|
233 |
|
234 |
227 (* position *) |
235 (* position *) |
228 |
236 |
229 fun position scan = |
237 fun position scan = |
230 (Scan.ahead (Scan.one not_eof) >> pos_of) -- scan >> Library.swap; |
238 (Scan.ahead (Scan.one not_eof) >> pos_of) -- scan >> Library.swap; |
231 |
239 |