src/Pure/sign.ML
changeset 71353 25b872d1d421
parent 70549 b2bedb022a75
child 71466 b1f3e86a4745
equal deleted inserted replaced
71352:7db80bd16f1c 71353:25b872d1d421
   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 private_scope: Binding.scope -> theory -> theory
   114   val private_scope: Binding.scope -> theory -> theory
   114   val private: Position.T -> theory -> theory
   115   val private: Position.T -> theory -> theory
   115   val qualified_scope: Binding.scope -> theory -> theory
   116   val qualified_scope: Binding.scope -> theory -> theory
   116   val qualified: Position.T -> theory -> theory
   117   val qualified: Position.T -> theory -> theory
   117   val concealed: theory -> theory
   118   val concealed: theory -> theory
   522 val mandatory_path = map_naming o Name_Space.mandatory_path;
   523 val mandatory_path = map_naming o Name_Space.mandatory_path;
   523 val qualified_path = map_naming oo Name_Space.qualified_path;
   524 val qualified_path = map_naming oo Name_Space.qualified_path;
   524 
   525 
   525 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);
   526 
   527 
       
   528 fun theory_naming thy = thy |> map_naming (Name_Space.set_theory_name (Context.theory_name thy));
       
   529 
   527 val private_scope = map_naming o Name_Space.private_scope;
   530 val private_scope = map_naming o Name_Space.private_scope;
   528 val private = map_naming o Name_Space.private;
   531 val private = map_naming o Name_Space.private;
   529 val qualified_scope = map_naming o Name_Space.qualified_scope;
   532 val qualified_scope = map_naming o Name_Space.qualified_scope;
   530 val qualified = map_naming o Name_Space.qualified;
   533 val qualified = map_naming o Name_Space.qualified;
   531 val concealed = map_naming Name_Space.concealed;
   534 val concealed = map_naming Name_Space.concealed;