equal
deleted
inserted
replaced
32 val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context |
32 val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context |
33 val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context |
33 val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context |
34 val naming_of: Proof.context -> Name_Space.naming |
34 val naming_of: Proof.context -> Name_Space.naming |
35 val restore_naming: Proof.context -> Proof.context -> Proof.context |
35 val restore_naming: Proof.context -> Proof.context -> Proof.context |
36 val full_name: Proof.context -> binding -> string |
36 val full_name: Proof.context -> binding -> string |
|
37 val get_scope: Proof.context -> Binding.scope option |
|
38 val new_scope: Proof.context -> Binding.scope * Proof.context |
37 val concealed: Proof.context -> Proof.context |
39 val concealed: Proof.context -> Proof.context |
38 val class_space: Proof.context -> Name_Space.T |
40 val class_space: Proof.context -> Name_Space.T |
39 val type_space: Proof.context -> Name_Space.T |
41 val type_space: Proof.context -> Name_Space.T |
40 val const_space: Proof.context -> Name_Space.T |
42 val const_space: Proof.context -> Name_Space.T |
41 val intern_class: Proof.context -> xstring -> string |
43 val intern_class: Proof.context -> xstring -> string |
303 val map_naming = Context.proof_map o Name_Space.map_naming; |
305 val map_naming = Context.proof_map o Name_Space.map_naming; |
304 val restore_naming = map_naming o K o naming_of; |
306 val restore_naming = map_naming o K o naming_of; |
305 |
307 |
306 val full_name = Name_Space.full_name o naming_of; |
308 val full_name = Name_Space.full_name o naming_of; |
307 |
309 |
|
310 val get_scope = Name_Space.get_scope o naming_of; |
|
311 |
|
312 fun new_scope ctxt = |
|
313 let |
|
314 val (scope, naming') = Name_Space.new_scope (naming_of ctxt); |
|
315 val ctxt' = map_naming (K naming') ctxt; |
|
316 in (scope, ctxt') end; |
|
317 |
308 val concealed = map_naming Name_Space.concealed; |
318 val concealed = map_naming Name_Space.concealed; |
309 |
319 |
310 |
320 |
311 (* name spaces *) |
321 (* name spaces *) |
312 |
322 |