equal
deleted
inserted
replaced
107 val root_path: theory -> theory |
107 val root_path: theory -> theory |
108 val parent_path: theory -> theory |
108 val parent_path: theory -> theory |
109 val mandatory_path: string -> theory -> theory |
109 val mandatory_path: string -> theory -> theory |
110 val qualified_path: bool -> binding -> theory -> theory |
110 val qualified_path: bool -> binding -> theory -> theory |
111 val local_path: theory -> theory |
111 val local_path: theory -> theory |
|
112 val concealed: theory -> theory |
112 val hide_class: bool -> string -> theory -> theory |
113 val hide_class: bool -> string -> theory -> theory |
113 val hide_type: bool -> string -> theory -> theory |
114 val hide_type: bool -> string -> theory -> theory |
114 val hide_const: bool -> string -> theory -> theory |
115 val hide_const: bool -> string -> theory -> theory |
115 end |
116 end |
116 |
117 |
508 val mandatory_path = map_naming o Name_Space.mandatory_path; |
509 val mandatory_path = map_naming o Name_Space.mandatory_path; |
509 val qualified_path = map_naming oo Name_Space.qualified_path; |
510 val qualified_path = map_naming oo Name_Space.qualified_path; |
510 |
511 |
511 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy); |
512 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy); |
512 |
513 |
|
514 val concealed = map_naming Name_Space.concealed; |
|
515 |
513 |
516 |
514 (* hide names *) |
517 (* hide names *) |
515 |
518 |
516 val hide_class = map_tsig oo Type.hide_class; |
519 val hide_class = map_tsig oo Type.hide_class; |
517 val hide_type = map_tsig oo Type.hide_type; |
520 val hide_type = map_tsig oo Type.hide_type; |