explicit root_path, parent_path;
authorwenzelm
Tue Mar 10 21:20:01 2009 +0100 (2009-03-10)
changeset 304219498e99e58a6
parent 30420 ebbec8d8d7a9
child 30422 9e9b8adddb93
explicit root_path, parent_path;
derived absolute_path;
tuned;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Tue Mar 10 21:19:22 2009 +0100
     1.2 +++ b/src/Pure/sign.ML	Tue Mar 10 21:20:01 2009 +0100
     1.3 @@ -122,13 +122,13 @@
     1.4    val add_trrules_i: ast Syntax.trrule list -> theory -> theory
     1.5    val del_trrules_i: ast Syntax.trrule list -> theory -> theory
     1.6    val add_path: string -> theory -> theory
     1.7 +  val root_path: theory -> theory
     1.8    val parent_path: theory -> theory
     1.9 -  val root_path: theory -> theory
    1.10 +  val sticky_prefix: string -> theory -> theory
    1.11 +  val no_base_names: theory -> theory
    1.12 +  val qualified_names: theory -> theory
    1.13    val absolute_path: theory -> theory
    1.14    val local_path: theory -> theory
    1.15 -  val no_base_names: theory -> theory
    1.16 -  val qualified_names: theory -> theory
    1.17 -  val sticky_prefix: string -> theory -> theory
    1.18    val restore_naming: theory -> theory -> theory
    1.19    val hide_class: bool -> string -> theory -> theory
    1.20    val hide_type: bool -> string -> theory -> theory
    1.21 @@ -619,17 +619,18 @@
    1.22  (* naming *)
    1.23  
    1.24  val add_path        = map_naming o NameSpace.add_path;
    1.25 +val root_path       = map_naming NameSpace.root_path;
    1.26 +val parent_path     = map_naming NameSpace.parent_path;
    1.27 +val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
    1.28  val no_base_names   = map_naming NameSpace.no_base_names;
    1.29  val qualified_names = map_naming NameSpace.qualified_names;
    1.30 -val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
    1.31 -val restore_naming  = map_naming o K o naming_of;
    1.32  
    1.33 -val parent_path   = add_path "..";
    1.34 -val root_path     = add_path "/";
    1.35 -val absolute_path = add_path "//";
    1.36 +val absolute_path = root_path o qualified_names;
    1.37  
    1.38  fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
    1.39  
    1.40 +val restore_naming  = map_naming o K o naming_of;
    1.41 +
    1.42  
    1.43  (* hide names *)
    1.44