src/Pure/sign.ML
changeset 19013 19ad0c59fb1f
parent 18994 ce724d5bada2
child 19054 af7cc6063285
equal deleted inserted replaced
19012:2577ac76cdc6 19013:19ad0c59fb1f
    62   val add_path: string -> theory -> theory
    62   val add_path: string -> theory -> theory
    63   val parent_path: theory -> theory
    63   val parent_path: theory -> theory
    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 qualified_names: theory -> theory
    68   val qualified_names: theory -> theory
    68   val no_base_names: theory -> theory
    69   val qualified_force_prefix: string -> theory -> theory
    69   val custom_accesses: (string list -> string list list) -> 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 qualified_names = map_naming NameSpace.qualified_names;
   888 val no_base_names          = map_naming NameSpace.no_base_names;
   889 val no_base_names   = map_naming NameSpace.no_base_names;
   889 val qualified_names        = map_naming NameSpace.qualified_names;
   890 val custom_accesses = map_naming o NameSpace.custom_accesses;
   890 val qualified_force_prefix = map_naming o NameSpace.qualified_force_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 
   898 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
   898 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
   899 
   899 
   900 
   900 
   901 (* hide names *)
   901 (* hide names *)