src/Pure/Isar/attrib.ML
changeset 56025 d74fed45fa8b
parent 55998 f5f9fad3321c
child 56026 893fe12639bc
equal deleted inserted replaced
56024:0921c1dc344c 56025:d74fed45fa8b
   127 val check_src = check_src_generic o Context.Proof;
   127 val check_src = check_src_generic o Context.Proof;
   128 
   128 
   129 
   129 
   130 (* pretty printing *)
   130 (* pretty printing *)
   131 
   131 
   132 fun extern ctxt = Name_Space.extern ctxt (#1 (get_attributes (Context.Proof ctxt)));
   132 fun extern ctxt =
       
   133   Name_Space.extern ctxt (Name_Space.space_of_table (get_attributes (Context.Proof ctxt)));
   133 
   134 
   134 fun pretty_attribs _ [] = []
   135 fun pretty_attribs _ [] = []
   135   | pretty_attribs ctxt srcs =
   136   | pretty_attribs ctxt srcs =
   136       [Pretty.enum "," "[" "]" (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs)];
   137       [Pretty.enum "," "[" "]" (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs)];
   137 
   138 
   138 
   139 
   139 (* get attributes *)
   140 (* get attributes *)
   140 
   141 
   141 fun attribute_generic context =
   142 fun attribute_generic context =
   142   let val (_, tab) = get_attributes context in
   143   let val table = get_attributes context in
   143     fn src =>
   144     fn src =>
   144       let val ((name, _), pos) = Args.dest_src src in
   145       let val ((name, _), pos) = Args.dest_src src in
   145         (case Symtab.lookup tab name of
   146         (case Name_Space.lookup_key table name of
   146           NONE => error ("Undefined attribute: " ^ quote name ^ Position.here pos)
   147           NONE => error ("Undefined attribute: " ^ quote name ^ Position.here pos)
   147         | SOME (att, _) => att src)
   148         | SOME (_, (att, _)) => att src)
   148       end
   149       end
   149   end;
   150   end;
   150 
   151 
   151 val attribute = attribute_generic o Context.Proof;
   152 val attribute = attribute_generic o Context.Proof;
   152 val attribute_global = attribute_generic o Context.Theory;
   153 val attribute_global = attribute_generic o Context.Theory;
   347     fun prt (name, config) =
   348     fun prt (name, config) =
   348       let val value = Config.get ctxt config in
   349       let val value = Config.get ctxt config in
   349         Pretty.block [Pretty.mark_str name, Pretty.str (": " ^ Config.print_type value ^ " ="),
   350         Pretty.block [Pretty.mark_str name, Pretty.str (": " ^ Config.print_type value ^ " ="),
   350           Pretty.brk 1, Pretty.str (Config.print_value value)]
   351           Pretty.brk 1, Pretty.str (Config.print_value value)]
   351       end;
   352       end;
   352     val space = #1 (get_attributes (Context.Proof ctxt));
   353     val space = Name_Space.space_of_table (get_attributes (Context.Proof ctxt));
   353     val configs = Name_Space.extern_table ctxt (space, Configs.get (Proof_Context.theory_of ctxt));
   354     val configs = Name_Space.extern_table' ctxt space (Configs.get (Proof_Context.theory_of ctxt));
   354   in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
   355   in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
   355 
   356 
   356 
   357 
   357 (* concrete syntax *)
   358 (* concrete syntax *)
   358 
   359