284 end; |
284 end; |
285 |
285 |
286 fun gen_add_syntax_const prep_const target raw_c raw_syn thy = |
286 fun gen_add_syntax_const prep_const target raw_c raw_syn thy = |
287 let |
287 let |
288 val c = prep_const thy raw_c; |
288 val c = prep_const thy raw_c; |
289 fun check_args (syntax as (n, _)) = if n > Code_Unit.no_args thy c |
289 fun check_args (syntax as (n, _)) = if n > Code.no_args thy c |
290 then error ("Too many arguments in syntax for constant " ^ quote c) |
290 then error ("Too many arguments in syntax for constant " ^ quote c) |
291 else syntax; |
291 else syntax; |
292 in case raw_syn |
292 in case raw_syn |
293 of SOME syntax => |
293 of SOME syntax => |
294 thy |
294 thy |
317 val cs = map (read_const thy) raw_cs; |
317 val cs = map (read_const thy) raw_cs; |
318 in Symtab.update (name, (str content, cs)) incls end |
318 in Symtab.update (name, (str content, cs)) incls end |
319 | add (name, NONE) incls = Symtab.delete name incls; |
319 | add (name, NONE) incls = Symtab.delete name incls; |
320 in map_includes target (add args) thy end; |
320 in map_includes target (add args) thy end; |
321 |
321 |
322 val add_include = gen_add_include Code_Unit.check_const; |
322 val add_include = gen_add_include Code.check_const; |
323 val add_include_cmd = gen_add_include Code_Unit.read_const; |
323 val add_include_cmd = gen_add_include Code.read_const; |
324 |
324 |
325 fun add_module_alias target (thyname, modlname) = |
325 fun add_module_alias target (thyname, modlname) = |
326 let |
326 let |
327 val xs = Long_Name.explode modlname; |
327 val xs = Long_Name.explode modlname; |
328 val xs' = map (Name.desymbolize true) xs; |
328 val xs' = map (Name.desymbolize true) xs; |
361 val add_syntax_tyco = gen_add_syntax_tyco cert_tyco; |
361 val add_syntax_tyco = gen_add_syntax_tyco cert_tyco; |
362 val add_syntax_const = gen_add_syntax_const (K I); |
362 val add_syntax_const = gen_add_syntax_const (K I); |
363 val allow_abort = gen_allow_abort (K I); |
363 val allow_abort = gen_allow_abort (K I); |
364 val add_reserved = add_reserved; |
364 val add_reserved = add_reserved; |
365 |
365 |
366 val add_syntax_class_cmd = gen_add_syntax_class read_class Code_Unit.read_const; |
366 val add_syntax_class_cmd = gen_add_syntax_class read_class Code.read_const; |
367 val add_syntax_inst_cmd = gen_add_syntax_inst read_class read_tyco; |
367 val add_syntax_inst_cmd = gen_add_syntax_inst read_class read_tyco; |
368 val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco; |
368 val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco; |
369 val add_syntax_const_cmd = gen_add_syntax_const Code_Unit.read_const; |
369 val add_syntax_const_cmd = gen_add_syntax_const Code.read_const; |
370 val allow_abort_cmd = gen_allow_abort Code_Unit.read_const; |
370 val allow_abort_cmd = gen_allow_abort Code.read_const; |
371 |
371 |
372 fun the_literals thy = |
372 fun the_literals thy = |
373 let |
373 let |
374 val (targets, _) = CodeTargetData.get thy; |
374 val (targets, _) = CodeTargetData.get thy; |
375 fun literals target = case Symtab.lookup targets target |
375 fun literals target = case Symtab.lookup targets target |
385 (* montage *) |
385 (* montage *) |
386 |
386 |
387 local |
387 local |
388 |
388 |
389 fun labelled_name thy program name = case Graph.get_node program name |
389 fun labelled_name thy program name = case Graph.get_node program name |
390 of Code_Thingol.Fun (c, _) => quote (Code_Unit.string_of_const thy c) |
390 of Code_Thingol.Fun (c, _) => quote (Code.string_of_const thy c) |
391 | Code_Thingol.Datatype (tyco, _) => "type " ^ quote (Sign.extern_type thy tyco) |
391 | Code_Thingol.Datatype (tyco, _) => "type " ^ quote (Sign.extern_type thy tyco) |
392 | Code_Thingol.Datatypecons (c, _) => quote (Code_Unit.string_of_const thy c) |
392 | Code_Thingol.Datatypecons (c, _) => quote (Code.string_of_const thy c) |
393 | Code_Thingol.Class (class, _) => "class " ^ quote (Sign.extern_class thy class) |
393 | Code_Thingol.Class (class, _) => "class " ^ quote (Sign.extern_class thy class) |
394 | Code_Thingol.Classrel (sub, super) => let |
394 | Code_Thingol.Classrel (sub, super) => let |
395 val Code_Thingol.Class (sub, _) = Graph.get_node program sub |
395 val Code_Thingol.Class (sub, _) = Graph.get_node program sub |
396 val Code_Thingol.Class (super, _) = Graph.get_node program super |
396 val Code_Thingol.Class (super, _) = Graph.get_node program super |
397 in quote (Sign.extern_class thy sub ^ " < " ^ Sign.extern_class thy super) end |
397 in quote (Sign.extern_class thy sub ^ " < " ^ Sign.extern_class thy super) end |
398 | Code_Thingol.Classparam (c, _) => quote (Code_Unit.string_of_const thy c) |
398 | Code_Thingol.Classparam (c, _) => quote (Code.string_of_const thy c) |
399 | Code_Thingol.Classinst ((class, (tyco, _)), _) => let |
399 | Code_Thingol.Classinst ((class, (tyco, _)), _) => let |
400 val Code_Thingol.Class (class, _) = Graph.get_node program class |
400 val Code_Thingol.Class (class, _) = Graph.get_node program class |
401 val Code_Thingol.Datatype (tyco, _) = Graph.get_node program tyco |
401 val Code_Thingol.Datatype (tyco, _) = Graph.get_node program tyco |
402 in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end |
402 in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end |
403 |
403 |