1.1 --- a/src/HOL/IMPP/Hoare.thy	Fri May 24 23:57:24 2013 +0200
     1.2 +++ b/src/HOL/IMPP/Hoare.thy	Fri May 24 23:57:24 2013 +0200
     1.3 @@ -189,7 +189,7 @@
     1.4  apply fast
     1.5  done
     1.6  
     1.7 -lemma constant: "[| C ==> G|-{P}.c.{Q} |] ==> G|-{%Z s. P Z s & C}.c.{Q}"
     1.8 +lemma "constant": "[| C ==> G|-{P}.c.{Q} |] ==> G|-{%Z s. P Z s & C}.c.{Q}"
     1.9  apply (rule hoare_derivs.conseq)
    1.10  apply fast
    1.11  done

     2.1 --- a/src/Tools/Code/code_target.ML	Fri May 24 23:57:24 2013 +0200
     2.2 +++ b/src/Tools/Code/code_target.ML	Fri May 24 23:57:24 2013 +0200
     2.3 @@ -50,15 +50,18 @@
     2.4      -> 'a -> serialization
     2.5    val set_default_code_width: int -> theory -> theory
     2.6  
     2.7 -  val allow_abort: string -> theory -> theory
     2.8 +  type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl
     2.9 +  type const_syntax = Code_Printer.const_syntax
    2.10    type tyco_syntax = Code_Printer.tyco_syntax
    2.11 -  type const_syntax = Code_Printer.const_syntax
    2.12 +  val set_printings: (const_syntax, tyco_syntax, string, unit, unit, (string * string list)) symbol_attr_decl
    2.13 +    -> theory -> theory
    2.14 +  val add_const_syntax: string -> string -> const_syntax option -> theory -> theory
    2.15 +  val add_tyco_syntax: string -> string -> tyco_syntax option -> theory -> theory
    2.16    val add_class_syntax: string -> class -> string option -> theory -> theory
    2.17    val add_instance_syntax: string -> class * string -> unit option -> theory -> theory
    2.18 -  val add_tyco_syntax: string -> string -> tyco_syntax option -> theory -> theory
    2.19 -  val add_const_syntax: string -> string -> const_syntax option -> theory -> theory
    2.20    val add_reserved: string -> string -> theory -> theory
    2.21    val add_include: string -> string * (string * string list) option -> theory -> theory
    2.22 +  val allow_abort: string -> theory -> theory
    2.23  
    2.24    val codegen_tool: string (*theory name*) -> string (*export_code expr*) -> unit
    2.25  
    2.26 @@ -71,11 +74,19 @@
    2.27  open Basic_Code_Thingol;
    2.28  
    2.29  type literals = Code_Printer.literals;
    2.30 +type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl =
    2.31 +  (string * (string * 'a option) list, string * (string * 'b option) list,
    2.32 +    class * (string * 'c option) list, (class * class) * (string * 'd option) list,
    2.33 +    (class * string) * (string * 'e option) list,
    2.34 +    string * (string * 'f option) list) Code_Symbol.attr;
    2.35 +
    2.36  type tyco_syntax = Code_Printer.tyco_syntax;
    2.37  type const_syntax = Code_Printer.const_syntax;
    2.38  
    2.39  
    2.40 -(** abstract nonsense **)
    2.41 +(** serializations and serializer **)
    2.42 +
    2.43 +(* serialization: abstract nonsense to cover different destinies for generated code *)
    2.44  
    2.45  datatype destination = Export of Path.T option | Produce | Present of string list;
    2.46  type serialization = int -> destination -> ((string * string) list * (string -> string option)) option;
    2.47 @@ -94,28 +105,7 @@
    2.48  fun present stmt_names f = space_implode "\n\n" (map snd (fst (the (f (Present stmt_names)))));
    2.49  
    2.50  
    2.51 -(** theory data **)
    2.52 -
    2.53 -datatype symbol_syntax_data = Symbol_Syntax_Data of {
    2.54 -  class: string Symtab.table,
    2.55 -  instance: unit Symreltab.table,
    2.56 -  tyco: Code_Printer.tyco_syntax Symtab.table,
    2.57 -  const: Code_Printer.const_syntax Symtab.table
    2.58 -};
    2.59 -
    2.60 -fun make_symbol_syntax_data ((class, instance), (tyco, const)) =
    2.61 -  Symbol_Syntax_Data { class = class, instance = instance, tyco = tyco, const = const };
    2.62 -fun map_symbol_syntax_data f (Symbol_Syntax_Data { class, instance, tyco, const }) =
    2.63 -  make_symbol_syntax_data (f ((class, instance), (tyco, const)));
    2.64 -fun merge_symbol_syntax_data
    2.65 -  (Symbol_Syntax_Data { class = class1, instance = instance1, tyco = tyco1, const = const1 },
    2.66 -    Symbol_Syntax_Data { class = class2, instance = instance2, tyco = tyco2, const = const2 }) =
    2.67 -  make_symbol_syntax_data ( (* FIXME proper merge order!? prefer fst!? *)
    2.68 -    (Symtab.join (K snd) (class1, class2),
    2.69 -       Symreltab.join (K snd) (instance1, instance2)),
    2.70 -    (Symtab.join (K snd) (tyco1, tyco2),
    2.71 -       Symtab.join (K snd) (const1, const2))
    2.72 -  );
    2.73 +(* serializers: functions producing serializations *)
    2.74  
    2.75  type serializer = Token.T list
    2.76    -> {
    2.77 @@ -129,49 +119,48 @@
    2.78    -> Code_Thingol.program
    2.79    -> serialization;
    2.80  
    2.81 -datatype description = Fundamental of { serializer: serializer,
    2.82 +datatype description =
    2.83 +    Fundamental of { serializer: serializer,
    2.84        literals: literals,
    2.85        check: { env_var: string, make_destination: Path.T -> Path.T,
    2.86          make_command: string -> string } }
    2.87    | Extension of string *
    2.88        (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
    2.89  
    2.90 +
    2.91 +(** theory data **)
    2.92 +
    2.93  datatype target = Target of {
    2.94    serial: serial,
    2.95    description: description,
    2.96    reserved: string list,
    2.97 -  includes: (Pretty.T * string list) Symtab.table,
    2.98    module_alias: string Symtab.table,
    2.99 -  symbol_syntax: symbol_syntax_data
   2.100 +  printings: (Code_Printer.const_syntax, Code_Printer.tyco_syntax, string, unit, unit,
   2.101 +    (Pretty.T * string list)) Code_Symbol.data
   2.102  };
   2.103  
   2.104 -fun make_target ((serial, description), ((reserved, includes), (module_alias, symbol_syntax))) =
   2.105 +fun make_target ((serial, description), ((reserved, module_alias), printings)) =
   2.106    Target { serial = serial, description = description, reserved = reserved,
   2.107 -    includes = includes, module_alias = module_alias, symbol_syntax = symbol_syntax };
   2.108 -fun map_target f ( Target { serial, description, reserved, includes, module_alias, symbol_syntax } ) =
   2.109 -  make_target (f ((serial, description), ((reserved, includes), (module_alias, symbol_syntax))));
   2.110 +    module_alias = module_alias, printings = printings };
   2.111 +fun map_target f ( Target { serial, description, reserved, module_alias, printings } ) =
   2.112 +  make_target (f ((serial, description), ((reserved, module_alias), printings)));
   2.113  fun merge_target strict target (Target { serial = serial1, description = description,
   2.114 -  reserved = reserved1, includes = includes1,
   2.115 -  module_alias = module_alias1, symbol_syntax = symbol_syntax1 },
   2.116 +  reserved = reserved1, module_alias = module_alias1, printings = printings1 },
   2.117      Target { serial = serial2, description = _,
   2.118 -      reserved = reserved2, includes = includes2,
   2.119 -      module_alias = module_alias2, symbol_syntax = symbol_syntax2 }) =
   2.120 +      reserved = reserved2, module_alias = module_alias2, printings = printings2 }) =
   2.121    if serial1 = serial2 orelse not strict then
   2.122      make_target ((serial1, description),
   2.123        ((merge (op =) (reserved1, reserved2),
   2.124 -         (* FIXME proper merge order!? prefer fst!? *)
   2.125 -         Symtab.join (K snd) (includes1, includes2)),
   2.126 -        (Symtab.join (K snd) (module_alias1, module_alias2),
   2.127 -          merge_symbol_syntax_data (symbol_syntax1, symbol_syntax2))
   2.128 +         Symtab.join (K snd) (module_alias1, module_alias2)),
   2.129 +        (Code_Symbol.merge_data (printings1, printings2))
   2.130      ))
   2.131    else
   2.132      error ("Incompatible targets: " ^ quote target);
   2.133  
   2.134  fun the_description (Target { description, ... }) = description;
   2.135  fun the_reserved (Target { reserved, ... }) = reserved;
   2.136 -fun the_includes (Target { includes, ... }) = includes;
   2.137  fun the_module_alias (Target { module_alias , ... }) = module_alias;
   2.138 -fun the_symbol_syntax (Target { symbol_syntax = Symbol_Syntax_Data x, ... }) = x;
   2.139 +fun the_printings (Target { printings, ... }) = printings;
   2.140  
   2.141  structure Targets = Theory_Data
   2.142  (
   2.143 @@ -209,8 +198,7 @@
   2.144      thy
   2.145      |> (Targets.map o apfst o apfst o Symtab.update)
   2.146            (target, make_target ((serial (), seri), (([], Symtab.empty),
   2.147 -            (Symtab.empty, make_symbol_syntax_data ((Symtab.empty, Symreltab.empty),
   2.148 -              (Symtab.empty, Symtab.empty))))))
   2.149 +            Code_Symbol.empty_data)))
   2.150    end;
   2.151  
   2.152  fun add_target (target, seri) = put_target (target, Fundamental seri);
   2.153 @@ -227,12 +215,10 @@
   2.154  
   2.155  fun map_reserved target =
   2.156    map_target_data target o apsnd o apfst o apfst;
   2.157 -fun map_includes target =
   2.158 +fun map_module_alias target =
   2.159    map_target_data target o apsnd o apfst o apsnd;
   2.160 -fun map_module_alias target =
   2.161 -  map_target_data target o apsnd o apsnd o apfst;
   2.162 -fun map_symbol_syntax target =
   2.163 -  map_target_data target o apsnd o apsnd o apsnd o map_symbol_syntax_data;
   2.164 +fun map_printings target =
   2.165 +  map_target_data target o apsnd o apsnd;
   2.166  
   2.167  fun set_default_code_width k = (Targets.map o apsnd) (K k);
   2.168  
   2.169 @@ -277,37 +263,37 @@
   2.170      val (modify, data) = collapse_hierarchy thy target;
   2.171    in (default_width, abortable, data, modify) end;
   2.172  
   2.173 -fun activate_syntax lookup_name src_tab = Symtab.empty
   2.174 -  |> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier
   2.175 -       of SOME name => (SOME name,
   2.176 -            Symtab.update_new (name, the (Symtab.lookup src_tab thing_identifier)) tab)
   2.177 -        | NONE => (NONE, tab)) (Symtab.keys src_tab)
   2.178 +fun activate_const_syntax thy literals cs_data naming =
   2.179 +  (Symtab.empty, naming)
   2.180 +  |> fold_map (fn (c, data) => fn (tab, naming) =>
   2.181 +      case Code_Thingol.lookup_const naming c
   2.182 +       of SOME name => let
   2.183 +              val (syn, naming') =
   2.184 +                Code_Printer.activate_const_syntax thy literals c data naming
   2.185 +            in (SOME name, (Symtab.update_new (name, syn) tab, naming')) end
   2.186 +        | NONE => (NONE, (tab, naming))) cs_data
   2.187    |>> map_filter I;
   2.188  
   2.189 -fun activate_const_syntax thy literals src_tab naming = (Symtab.empty, naming)
   2.190 -  |> fold_map (fn c => fn (tab, naming) =>
   2.191 -      case Code_Thingol.lookup_const naming c
   2.192 -       of SOME name => let
   2.193 -              val (syn, naming') = Code_Printer.activate_const_syntax thy
   2.194 -                literals c (the (Symtab.lookup src_tab c)) naming
   2.195 -            in (SOME name, (Symtab.update_new (name, syn) tab, naming')) end
   2.196 -        | NONE => (NONE, (tab, naming))) (Symtab.keys src_tab)
   2.197 +fun activate_syntax lookup_name things =
   2.198 +  Symtab.empty
   2.199 +  |> fold_map (fn (thing_identifier, data) => fn tab => case lookup_name thing_identifier
   2.200 +       of SOME name => (SOME name, Symtab.update_new (name, data) tab)
   2.201 +        | NONE => (NONE, tab)) things
   2.202    |>> map_filter I;
   2.203  
   2.204 -fun activate_symbol_syntax thy literals naming
   2.205 -    class_syntax instance_syntax tyco_syntax const_syntax =
   2.206 +fun activate_symbol_syntax thy literals naming printings =
   2.207    let
   2.208 -    val (names_class, class_syntax') =
   2.209 -      activate_syntax (Code_Thingol.lookup_class naming) class_syntax;
   2.210 -    val names_inst = map_filter (Code_Thingol.lookup_instance naming)
   2.211 -      (Symreltab.keys instance_syntax);
   2.212 -    val (names_tyco, tyco_syntax') =
   2.213 -      activate_syntax (Code_Thingol.lookup_tyco naming) tyco_syntax;
   2.214 -    val (names_const, (const_syntax', _)) =
   2.215 -      activate_const_syntax thy literals const_syntax naming;
   2.216 +    val (names_const, (const_syntax, _)) =
   2.217 +      activate_const_syntax thy literals (Code_Symbol.dest_constant_data printings) naming;
   2.218 +    val (names_tyco, tyco_syntax) =
   2.219 +      activate_syntax (Code_Thingol.lookup_tyco naming) (Code_Symbol.dest_type_constructor_data printings);
   2.220 +    val (names_class, class_syntax) =
   2.221 +      activate_syntax (Code_Thingol.lookup_class naming) (Code_Symbol.dest_type_class_data printings);
   2.222 +    val names_inst = map_filter (Code_Thingol.lookup_instance naming o fst)
   2.223 +      (Code_Symbol.dest_class_instance_data printings);
   2.224    in
   2.225 -    (names_class @ names_inst @ names_tyco @ names_const,
   2.226 -      (class_syntax', tyco_syntax', const_syntax'))
   2.227 +    (names_const @ names_tyco @ names_class @ names_inst,
   2.228 +      (const_syntax, tyco_syntax, class_syntax))
   2.229    end;
   2.230  
   2.231  fun project_program thy abortable names_hidden names1 program2 =
   2.232 @@ -325,29 +311,27 @@
   2.233      val program4 = Graph.restrict (member (op =) names4) program3;
   2.234    in (names4, program4) end;
   2.235  
   2.236 -fun prepare_serializer thy abortable serializer literals reserved all_includes
   2.237 -    module_alias proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax
   2.238 -    module_name args naming proto_program names =
   2.239 +fun prepare_serializer thy abortable (serializer : serializer) literals reserved module_alias
   2.240 +    printings module_name args naming proto_program names =
   2.241    let
   2.242 -    val (names_hidden, (class_syntax, tyco_syntax, const_syntax)) =
   2.243 -      activate_symbol_syntax thy literals naming
   2.244 -        proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax;
   2.245 +    val (names_hidden, (const_syntax, tyco_syntax, class_syntax)) =
   2.246 +      activate_symbol_syntax thy literals naming printings;
   2.247      val (names_all, program) = project_program thy abortable names_hidden names proto_program;
   2.248      fun select_include (name, (content, cs)) =
   2.249        if null cs orelse exists (fn c => case Code_Thingol.lookup_const naming c
   2.250         of SOME name => member (op =) names_all name
   2.251          | NONE => false) cs
   2.252        then SOME (name, content) else NONE;
   2.253 -    val includes = map_filter select_include (Symtab.dest all_includes);
   2.254 +    val includes = map_filter select_include (Code_Symbol.dest_module_data printings);
   2.255    in
   2.256      (serializer args {
   2.257        labelled_name = Code_Thingol.labelled_name thy proto_program,
   2.258        reserved_syms = reserved,
   2.259        includes = includes,
   2.260        module_alias = if module_name = "" then Symtab.lookup module_alias else K (SOME module_name),
   2.261 -      class_syntax = Symtab.lookup class_syntax,
   2.262 +      const_syntax = Symtab.lookup const_syntax,
   2.263        tyco_syntax = Symtab.lookup tyco_syntax,
   2.264 -      const_syntax = Symtab.lookup const_syntax },
   2.265 +      class_syntax = Symtab.lookup class_syntax },
   2.266        program)
   2.267    end;
   2.268  
   2.269 @@ -358,12 +342,10 @@
   2.270       of Fundamental seri => #serializer seri;
   2.271      val reserved = the_reserved data;
   2.272      val module_alias = the_module_alias data
   2.273 -    val { class, instance, tyco, const } = the_symbol_syntax data;
   2.274      val literals = the_literals thy target;
   2.275      val (prepared_serializer, prepared_program) = prepare_serializer thy
   2.276 -      abortable serializer literals reserved (the_includes data) module_alias
   2.277 -        class instance tyco const module_name args
   2.278 -          naming (modify naming program) names
   2.279 +      abortable serializer literals reserved module_alias (the_printings data)
   2.280 +        module_name args naming (modify naming program) names
   2.281      val width = the_default default_width some_width;
   2.282    in (fn program => prepared_serializer program width, prepared_program) end;
   2.283  
   2.284 @@ -540,14 +522,13 @@
   2.285  
   2.286  (** serializer configuration **)
   2.287  
   2.288 -(* data access *)
   2.289 +(* checking and parsing *)
   2.290  
   2.291 -fun cert_class thy class =
   2.292 +fun cert_const thy const =
   2.293    let
   2.294 -    val _ = Axclass.get_info thy class;
   2.295 -  in class end;
   2.296 -
   2.297 -fun read_class thy = cert_class thy o Sign.intern_class thy;
   2.298 +    val _ = if Sign.declared_const thy const then ()
   2.299 +      else error ("No such constant: " ^ quote const);
   2.300 +  in const end;
   2.301  
   2.302  fun cert_tyco thy tyco =
   2.303    let
   2.304 @@ -557,38 +538,71 @@
   2.305  
   2.306  fun read_tyco thy = cert_tyco thy o Sign.intern_type thy;
   2.307  
   2.308 +fun cert_class thy class =
   2.309 +  let
   2.310 +    val _ = Axclass.get_info thy class;
   2.311 +  in class end;
   2.312 +
   2.313 +fun read_class thy = cert_class thy o Sign.intern_class thy;
   2.314 +
   2.315 +val parse_classrel_ident = Parse.class --| @{keyword "<"} -- Parse.class;
   2.316 +
   2.317  fun cert_inst thy (class, tyco) =
   2.318    (cert_class thy class, cert_tyco thy tyco);
   2.319  
   2.320  fun read_inst thy (raw_tyco, raw_class) =
   2.321    (read_class thy raw_class, read_tyco thy raw_tyco);
   2.322  
   2.323 -fun gen_add_syntax (mapp, upd, del) prep_x prep_syn target raw_x some_raw_syn thy =
   2.324 +val parse_inst_ident = Parse.xname --| @{keyword "::"} -- Parse.class;
   2.325 +
   2.326 +fun cert_syms thy =
   2.327 +  Code_Symbol.map_attr (apfst (cert_const thy)) (apfst (cert_tyco thy))
   2.328 +    (apfst (cert_class thy)) ((apfst o pairself) (cert_class thy)) (apfst (cert_inst thy)) I;
   2.329 +
   2.330 +fun read_syms thy =
   2.331 +  Code_Symbol.map_attr (apfst (Code.read_const thy)) (apfst (read_tyco thy))
   2.332 +    (apfst (read_class thy)) ((apfst o pairself) (read_class thy)) (apfst (read_inst thy)) I;
   2.333 +
   2.334 +fun check_const_syntax thy c syn =
   2.335 +  if Code_Printer.requires_args syn > Code.args_number thy c
   2.336 +  then error ("Too many arguments in syntax for constant " ^ quote c)
   2.337 +  else syn;
   2.338 +
   2.339 +fun check_tyco_syntax thy tyco syn =
   2.340 +  if fst syn <> Sign.arity_number thy tyco
   2.341 +  then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
   2.342 +  else syn;
   2.343 +
   2.344 +fun arrange_printings prep_const thy =
   2.345    let
   2.346 -    val x = prep_x thy raw_x;
   2.347 -    val change = case some_raw_syn
   2.348 -     of SOME raw_syn => upd (x, prep_syn thy x raw_syn)
   2.349 -      | NONE => del x;
   2.350 -  in (map_symbol_syntax target o mapp) change thy end;
   2.351 +    fun arrange check (sym, target_syns) =
   2.352 +      map (fn (target, some_syn) => (target, (sym, Option.map (check thy sym) some_syn))) target_syns;
   2.353 +  in
   2.354 +    Code_Symbol.maps_attr'
   2.355 +      (arrange check_const_syntax) (arrange check_tyco_syntax)
   2.356 +        (arrange ((K o K) I)) (arrange ((K o K) I)) (arrange ((K o K) I))
   2.357 +        (arrange (fn thy => fn _ => fn (raw_content, raw_cs) =>
   2.358 +          (Code_Printer.str raw_content, map (prep_const thy) raw_cs)))
   2.359 +  end;
   2.360  
   2.361 -fun gen_add_class_syntax prep_class =
   2.362 -  gen_add_syntax (apfst o apfst, Symtab.update, Symtab.delete_safe) prep_class ((K o K) I);
   2.363 +fun cert_printings thy = cert_syms thy #> arrange_printings cert_const thy;
   2.364  
   2.365 -fun gen_add_instance_syntax prep_inst =
   2.366 -  gen_add_syntax (apfst o apsnd, Symreltab.update, Symreltab.delete_safe) prep_inst ((K o K) I);
   2.367 +fun read_printings thy = read_syms thy #> arrange_printings Code.read_const thy;
   2.368  
   2.369 -fun gen_add_tyco_syntax prep_tyco =
   2.370 -  gen_add_syntax (apsnd o apfst, Symtab.update, Symtab.delete_safe) prep_tyco
   2.371 -    (fn thy => fn tyco => fn syn => if fst syn <> Sign.arity_number thy tyco
   2.372 -      then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
   2.373 -      else syn);
   2.374  
   2.375 -fun gen_add_const_syntax prep_const =
   2.376 -  gen_add_syntax (apsnd o apsnd, Symtab.update, Symtab.delete_safe) prep_const
   2.377 -    (fn thy => fn c => fn syn =>
   2.378 -      if Code_Printer.requires_args syn > Code.args_number thy c
   2.379 -      then error ("Too many arguments in syntax for constant " ^ quote c)
   2.380 -      else syn);
   2.381 +(* custom symbol names *)
   2.382 +
   2.383 +fun add_module_alias target (thyname, "") =
   2.384 +      map_module_alias target (Symtab.delete thyname)
   2.385 +  | add_module_alias target (thyname, modlname) =
   2.386 +      let
   2.387 +        val xs = Long_Name.explode modlname;
   2.388 +        val xs' = map (Name.desymbolize true) xs;
   2.389 +      in if xs' = xs
   2.390 +        then map_module_alias target (Symtab.update (thyname, modlname))
   2.391 +        else error ("Invalid module name: " ^ quote modlname ^ "\n"
   2.392 +          ^ "perhaps try " ^ quote (Long_Name.implode xs'))
   2.393 +      end;
   2.394  
   2.395  fun add_reserved target sym thy =
   2.396    let
   2.397 @@ -601,32 +615,41 @@
   2.398      |> map_reserved target (insert (op =) sym)
   2.399    end;
   2.400  
   2.401 -fun gen_add_include read_const target args thy =
   2.402 +
   2.403 +(* custom printings *)
   2.404 +
   2.405 +fun set_printing (target, sym_syn) = map_printings target (Code_Symbol.set_data sym_syn);
   2.406 +
   2.407 +fun gen_set_printings prep_print_decl raw_print_decls thy =
   2.408 +  fold set_printing (prep_print_decl thy raw_print_decls) thy;
   2.409 +
   2.410 +val set_printings = gen_set_printings cert_printings;
   2.411 +val set_printings_cmd = gen_set_printings read_printings;
   2.412 +
   2.413 +fun gen_add_syntax Symbol prep_x prep_syn target raw_x some_raw_syn thy =
   2.414    let
   2.415 -    fun add (name, SOME (content, raw_cs)) incls =
   2.416 -          let
   2.417 -            val _ = if Symtab.defined incls name
   2.418 -              then warning ("Overwriting existing include " ^ name)
   2.419 -              else ();
   2.420 -            val cs = map (read_const thy) raw_cs;
   2.421 -          in Symtab.update (name, (Code_Printer.str content, cs)) incls end
   2.422 -      | add (name, NONE) incls = Symtab.delete name incls;
   2.423 -  in map_includes target (add args) thy end;
   2.424 +    val x = prep_x thy raw_x;
   2.425 +  in set_printing (target, Symbol (x, Option.map (prep_syn thy x) some_raw_syn)) thy end;
   2.426  
   2.427 -val add_include = gen_add_include (K I);
   2.428 -val add_include_cmd = gen_add_include Code.read_const;
   2.429 +fun gen_add_const_syntax prep_const =
   2.430 +  gen_add_syntax Code_Symbol.Constant prep_const check_const_syntax;
   2.431  
   2.432 -fun add_module_alias target (thyname, "") =
   2.433 -      map_module_alias target (Symtab.delete thyname)
   2.434 -  | add_module_alias target (thyname, modlname) =
   2.435 -      let
   2.436 -        val xs = Long_Name.explode modlname;
   2.437 -        val xs' = map (Name.desymbolize true) xs;
   2.438 -      in if xs' = xs
   2.439 -        then map_module_alias target (Symtab.update (thyname, modlname))
   2.440 -        else error ("Invalid module name: " ^ quote modlname ^ "\n"
   2.441 -          ^ "perhaps try " ^ quote (Long_Name.implode xs'))
   2.442 -      end;
   2.443 +fun gen_add_tyco_syntax prep_tyco =
   2.444 +  gen_add_syntax Code_Symbol.Type_Constructor prep_tyco check_tyco_syntax;
   2.445 +
   2.446 +fun gen_add_class_syntax prep_class =
   2.447 +  gen_add_syntax Code_Symbol.Type_Class prep_class ((K o K) I);
   2.448 +
   2.449 +fun gen_add_instance_syntax prep_inst =
   2.450 +  gen_add_syntax Code_Symbol.Class_Instance prep_inst ((K o K) I);
   2.451 +
   2.452 +fun gen_add_include prep_const target (name, some_content) thy =
   2.453 +  gen_add_syntax Code_Symbol.Module (K I)
   2.454 +    (fn thy => fn _ => fn (raw_content, raw_cs) => (Code_Printer.str raw_content, map (prep_const thy) raw_cs))
   2.455 +    target name some_content thy;
   2.456 +
   2.457 +
   2.458 +(* abortable constants *)
   2.459  
   2.460  fun gen_allow_abort prep_const raw_c thy =
   2.461    let
   2.462 @@ -653,18 +676,19 @@
   2.463  
   2.464  in
   2.465  
   2.466 +val add_reserved = add_reserved;
   2.467 +val add_const_syntax = gen_add_const_syntax (K I);
   2.468 +val add_tyco_syntax = gen_add_tyco_syntax cert_tyco;
   2.469  val add_class_syntax = gen_add_class_syntax cert_class;
   2.470  val add_instance_syntax = gen_add_instance_syntax cert_inst;
   2.471 -val add_tyco_syntax = gen_add_tyco_syntax cert_tyco;
   2.472 -val add_const_syntax = gen_add_const_syntax (K I);
   2.473 +val add_include = gen_add_include (K I);
   2.474  val allow_abort = gen_allow_abort (K I);
   2.475 -val add_reserved = add_reserved;
   2.476 -val add_include = add_include;
   2.477  
   2.478 +val add_const_syntax_cmd = gen_add_const_syntax Code.read_const;
   2.479 +val add_tyco_syntax_cmd = gen_add_tyco_syntax read_tyco;
   2.480  val add_class_syntax_cmd = gen_add_class_syntax read_class;
   2.481  val add_instance_syntax_cmd = gen_add_instance_syntax read_inst;
   2.482 -val add_tyco_syntax_cmd = gen_add_tyco_syntax read_tyco;
   2.483 -val add_const_syntax_cmd = gen_add_const_syntax Code.read_const;
   2.484 +val add_include_cmd = gen_add_include Code.read_const;
   2.485  val allow_abort_cmd = gen_allow_abort Code.read_const;
   2.486  
   2.487  fun parse_args f args =
   2.488 @@ -687,6 +711,45 @@
   2.489         -- Scan.optional (@{keyword "file"} |-- Parse.name) ""
   2.490         -- code_expr_argsP) >> (fn seris => export_code_cmd raw_cs seris)));
   2.491  
   2.492 +fun parse_single_symbol_pragma parse_keyword parse_isa parse_target =
   2.493 +  parse_keyword |-- Parse.!!! parse_isa --| (@{keyword "\<rightharpoonup>"} || @{keyword "=>"})
   2.494 +    -- Parse.and_list1 (@{keyword "("} |-- (Parse.name --| @{keyword ")"} -- Scan.option parse_target));
   2.495 +
   2.496 +fun parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module =
   2.497 +  parse_single_symbol_pragma @{keyword "constant"} Parse.term_group parse_const
   2.498 +    >> Code_Symbol.Constant
   2.499 +  || parse_single_symbol_pragma @{keyword "type_constructor"} Parse.xname parse_tyco
   2.500 +    >> Code_Symbol.Type_Constructor
   2.501 +  || parse_single_symbol_pragma @{keyword "type_class"} Parse.xname parse_class
   2.502 +    >> Code_Symbol.Type_Class
   2.503 +  || parse_single_symbol_pragma @{keyword "class_relation"} parse_classrel_ident parse_classrel
   2.504 +    >> Code_Symbol.Class_Relation
   2.505 +  || parse_single_symbol_pragma @{keyword "class_instance"} parse_inst_ident parse_inst
   2.506 +    >> Code_Symbol.Class_Instance
   2.507 +  || parse_single_symbol_pragma @{keyword "code_module"} Parse.name parse_module
   2.508 +    >> Code_Symbol.Module;
   2.509 +
   2.510 +fun parse_symbol_pragmas parse_const parse_tyco parse_class parse_classrel parse_inst parse_module =
   2.511 +  Parse.enum1 "|" (Parse.group (fn () => "code symbol pragma")
   2.512 +    (parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module));
   2.513 +
   2.514 +val _ =
   2.515 +  Outer_Syntax.command @{command_spec "code_printing"} "declare dedicated printing for code symbols"
   2.516 +    (parse_symbol_pragmas (Code_Printer.parse_const_syntax) (Code_Printer.parse_tyco_syntax)
   2.517 +      Parse.string (Parse.minus >> K ()) (Parse.minus >> K ())
   2.518 +      (Parse.text -- Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) [])
   2.519 +      >> (Toplevel.theory o fold set_printings_cmd));
   2.520 +
   2.521 +val _ =
   2.522 +  Outer_Syntax.command @{command_spec "code_const"} "define code syntax for constant"
   2.523 +    (process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax
   2.524 +      add_const_syntax_cmd);
   2.525 +
   2.526 +val _ =
   2.527 +  Outer_Syntax.command @{command_spec "code_type"} "define code syntax for type constructor"
   2.528 +    (process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax
   2.529 +      add_tyco_syntax_cmd);
   2.530 +
   2.531  val _ =
   2.532    Outer_Syntax.command @{command_spec "code_class"} "define code syntax for class"
   2.533      (process_multi_syntax Parse.xname Parse.string
   2.534 @@ -698,14 +761,6 @@
   2.535        add_instance_syntax_cmd);
   2.536  
   2.537  val _ =
   2.538 -  Outer_Syntax.command @{command_spec "code_type"} "define code syntax for type constructor"
   2.539 -    (process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax add_tyco_syntax_cmd);
   2.540 -
   2.541 -val _ =
   2.542 -  Outer_Syntax.command @{command_spec "code_const"} "define code syntax for constant"
   2.543 -    (process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax add_const_syntax_cmd);
   2.544 -
   2.545 -val _ =
   2.546    Outer_Syntax.command @{command_spec "code_reserved"}
   2.547      "declare words as reserved for target language"
   2.548      (Parse.name -- Scan.repeat1 Parse.name

     3.1 --- a/src/Tools/Code_Generator.thy	Fri May 24 23:57:24 2013 +0200
     3.2 +++ b/src/Tools/Code_Generator.thy	Fri May 24 23:57:24 2013 +0200
     3.3 @@ -8,10 +8,11 @@
     3.4  imports Pure
     3.5  keywords
     3.6    "value" "print_codeproc" "code_thms" "code_deps" :: diag and
     3.7 -  "export_code" "code_class" "code_instance" "code_type"
     3.8 +  "export_code" "code_printing" "code_class" "code_instance" "code_type"
     3.9      "code_const" "code_reserved" "code_include" "code_modulename"
    3.10      "code_abort" "code_monad" "code_reflect" :: thy_decl and
    3.11    "datatypes" "functions" "module_name" "file" "checking"
    3.12 +  "constant" "type_constructor" "type_class" "class_relation" "class_instance" "code_module"
    3.13  begin
    3.14  
    3.15  ML_file "~~/src/Tools/value.ML"