equal
deleted
inserted
replaced
108 val root_path: theory -> theory |
108 val root_path: theory -> theory |
109 val parent_path: theory -> theory |
109 val parent_path: theory -> theory |
110 val mandatory_path: string -> theory -> theory |
110 val mandatory_path: string -> theory -> theory |
111 val qualified_path: bool -> binding -> theory -> theory |
111 val qualified_path: bool -> binding -> theory -> theory |
112 val local_path: theory -> theory |
112 val local_path: theory -> theory |
113 val theory_naming: theory -> theory |
113 val init_naming: theory -> theory |
114 val private_scope: Binding.scope -> theory -> theory |
114 val private_scope: Binding.scope -> theory -> theory |
115 val private: Position.T -> theory -> theory |
115 val private: Position.T -> theory -> theory |
116 val qualified_scope: Binding.scope -> theory -> theory |
116 val qualified_scope: Binding.scope -> theory -> theory |
117 val qualified: Position.T -> theory -> theory |
117 val qualified: Position.T -> theory -> theory |
118 val concealed: theory -> theory |
118 val concealed: theory -> theory |
523 val mandatory_path = map_naming o Name_Space.mandatory_path; |
523 val mandatory_path = map_naming o Name_Space.mandatory_path; |
524 val qualified_path = map_naming oo Name_Space.qualified_path; |
524 val qualified_path = map_naming oo Name_Space.qualified_path; |
525 |
525 |
526 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy); |
526 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy); |
527 |
527 |
528 fun theory_naming thy = thy |
528 fun init_naming thy = |
529 |> map_naming (Name_Space.set_theory_long_name (Context.theory_long_name thy)); |
529 let |
|
530 val theory_naming = Name_Space.global_naming |
|
531 |> Name_Space.set_theory_long_name (Context.theory_long_name thy); |
|
532 in map_naming (K theory_naming) thy end; |
530 |
533 |
531 val private_scope = map_naming o Name_Space.private_scope; |
534 val private_scope = map_naming o Name_Space.private_scope; |
532 val private = map_naming o Name_Space.private; |
535 val private = map_naming o Name_Space.private; |
533 val qualified_scope = map_naming o Name_Space.qualified_scope; |
536 val qualified_scope = map_naming o Name_Space.qualified_scope; |
534 val qualified = map_naming o Name_Space.qualified; |
537 val qualified = map_naming o Name_Space.qualified; |