src/Pure/Isar/attrib.ML
changeset 42358 b47d41d9f4b5
parent 42289 dafae095d733
child 42360 da8817d01e7c
     1.1 --- a/src/Pure/Isar/attrib.ML	Sat Apr 16 12:46:18 2011 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sat Apr 16 13:48:45 2011 +0200
     1.3 @@ -73,11 +73,12 @@
     1.4  
     1.5  fun print_attributes thy =
     1.6    let
     1.7 +    val ctxt = ProofContext.init_global thy;
     1.8      val attribs = Attributes.get thy;
     1.9      fun prt_attr (name, (_, comment)) = Pretty.block
    1.10        [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    1.11    in
    1.12 -    [Pretty.big_list "attributes:" (map prt_attr (Name_Space.extern_table attribs))]
    1.13 +    [Pretty.big_list "attributes:" (map prt_attr (Name_Space.extern_table ctxt attribs))]
    1.14      |> Pretty.chunks |> Pretty.writeln
    1.15    end;
    1.16  
    1.17 @@ -90,7 +91,7 @@
    1.18  val intern = Name_Space.intern o #1 o Attributes.get;
    1.19  val intern_src = Args.map_name o intern;
    1.20  
    1.21 -val extern = Name_Space.extern o #1 o Attributes.get o ProofContext.theory_of;
    1.22 +fun extern ctxt = Name_Space.extern ctxt (#1 (Attributes.get (ProofContext.theory_of ctxt)));
    1.23  
    1.24  
    1.25  (* pretty printing *)
    1.26 @@ -341,7 +342,7 @@
    1.27          Pretty.block [Pretty.str (name ^ ": " ^ Config.print_type value ^ " ="), Pretty.brk 1,
    1.28            Pretty.str (Config.print_value value)]
    1.29        end;
    1.30 -    val configs = Name_Space.extern_table (#1 (Attributes.get thy), Configs.get thy);
    1.31 +    val configs = Name_Space.extern_table ctxt (#1 (Attributes.get thy), Configs.get thy);
    1.32    in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
    1.33  
    1.34  
    1.35 @@ -408,6 +409,9 @@
    1.36    register_config Printer.show_question_marks_raw #>
    1.37    register_config Syntax.ambiguity_level_raw #>
    1.38    register_config Syntax_Trans.eta_contract_raw #>
    1.39 +  register_config Name_Space.long_names_raw #>
    1.40 +  register_config Name_Space.short_names_raw #>
    1.41 +  register_config Name_Space.unique_names_raw #>
    1.42    register_config ML_Context.trace_raw #>
    1.43    register_config ProofContext.show_abbrevs_raw #>
    1.44    register_config Goal_Display.goals_limit_raw #>