src/Pure/sign.ML
changeset 19054 af7cc6063285
parent 19013 19ad0c59fb1f
child 19099 100bf66d7e85
equal deleted inserted replaced
19053:358c0eb6d785 19054:af7cc6063285
    64   val root_path: theory -> theory
    64   val root_path: theory -> theory
    65   val absolute_path: theory -> theory
    65   val absolute_path: theory -> theory
    66   val local_path: theory -> theory
    66   val local_path: theory -> theory
    67   val no_base_names: theory -> theory
    67   val no_base_names: theory -> theory
    68   val qualified_names: theory -> theory
    68   val qualified_names: theory -> theory
    69   val qualified_force_prefix: string -> theory -> theory
    69   val sticky_prefix: string -> theory -> theory
    70   val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
    70   val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
    71     theory -> theory
    71     theory -> theory
    72   val restore_naming: theory -> theory -> theory
    72   val restore_naming: theory -> theory -> theory
    73   val hide_classes: bool -> xstring list -> theory -> theory
    73   val hide_classes: bool -> xstring list -> theory -> theory
    74   val hide_classes_i: bool -> string list -> theory -> theory
    74   val hide_classes_i: bool -> string list -> theory -> theory
   882 val add_trrules_i = map_syn o Syntax.extend_trrules_i;
   882 val add_trrules_i = map_syn o Syntax.extend_trrules_i;
   883 
   883 
   884 
   884 
   885 (* modify naming *)
   885 (* modify naming *)
   886 
   886 
   887 val add_path               = map_naming o NameSpace.add_path;
   887 val add_path        = map_naming o NameSpace.add_path;
   888 val no_base_names          = map_naming NameSpace.no_base_names;
   888 val no_base_names   = map_naming NameSpace.no_base_names;
   889 val qualified_names        = map_naming NameSpace.qualified_names;
   889 val qualified_names = map_naming NameSpace.qualified_names;
   890 val qualified_force_prefix = map_naming o NameSpace.qualified_force_prefix;
   890 val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
   891 val set_policy             = map_naming o NameSpace.set_policy;
   891 val set_policy      = map_naming o NameSpace.set_policy;
   892 val restore_naming         = map_naming o K o naming_of;
   892 val restore_naming  = map_naming o K o naming_of;
   893 
   893 
   894 val parent_path   = add_path "..";
   894 val parent_path   = add_path "..";
   895 val root_path     = add_path "/";
   895 val root_path     = add_path "/";
   896 val absolute_path = add_path "//";
   896 val absolute_path = add_path "//";
   897 
   897