src/Pure/sign.ML
changeset 72283 4ed33ea8d957
parent 71466 b1f3e86a4745
child 72288 f8d28617ea08
equal deleted inserted replaced
72282:912f13865596 72283:4ed33ea8d957
   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;