427 fun prep_destination "" = NONE |
427 fun prep_destination "" = NONE |
428 | prep_destination s = SOME (Path.explode s); |
428 | prep_destination s = SOME (Path.explode s); |
429 |
429 |
430 fun export_code ctxt all_public cs seris = |
430 fun export_code ctxt all_public cs seris = |
431 let |
431 let |
432 val thy = Proof_Context.theory_of ctxt; |
432 val program = Code_Thingol.consts_program ctxt cs; |
433 val program = Code_Thingol.consts_program thy cs; |
|
434 val _ = map (fn (((target_name, module_name), some_path), args) => |
433 val _ = map (fn (((target_name, module_name), some_path), args) => |
435 export_code_for ctxt some_path target_name NONE module_name args program all_public (map Constant cs)) seris; |
434 export_code_for ctxt some_path target_name NONE module_name args program all_public (map Constant cs)) seris; |
436 in () end; |
435 in () end; |
437 |
436 |
438 fun export_code_cmd all_public raw_cs seris ctxt = |
437 fun export_code_cmd all_public raw_cs seris ctxt = |
440 (Code_Thingol.read_const_exprs ctxt raw_cs) |
439 (Code_Thingol.read_const_exprs ctxt raw_cs) |
441 ((map o apfst o apsnd) prep_destination seris); |
440 ((map o apfst o apsnd) prep_destination seris); |
442 |
441 |
443 fun produce_code ctxt all_public cs target_name some_width some_module_name args = |
442 fun produce_code ctxt all_public cs target_name some_width some_module_name args = |
444 let |
443 let |
445 val thy = Proof_Context.theory_of ctxt; |
444 val program = Code_Thingol.consts_program ctxt cs; |
446 val program = Code_Thingol.consts_program thy cs; |
|
447 in produce_code_for ctxt target_name some_width some_module_name args program all_public (map Constant cs) end; |
445 in produce_code_for ctxt target_name some_width some_module_name args program all_public (map Constant cs) end; |
448 |
446 |
449 fun present_code ctxt cs syms target_name some_width some_module_name args = |
447 fun present_code ctxt cs syms target_name some_width some_module_name args = |
450 let |
448 let |
451 val thy = Proof_Context.theory_of ctxt; |
449 val program = Code_Thingol.consts_program ctxt cs; |
452 val program = Code_Thingol.consts_program thy cs; |
|
453 in present_code_for ctxt target_name some_width some_module_name args program (map Constant cs, syms) end; |
450 in present_code_for ctxt target_name some_width some_module_name args program (map Constant cs, syms) end; |
454 |
451 |
455 fun check_code ctxt all_public cs seris = |
452 fun check_code ctxt all_public cs seris = |
456 let |
453 let |
457 val thy = Proof_Context.theory_of ctxt; |
454 val program = Code_Thingol.consts_program ctxt cs; |
458 val program = Code_Thingol.consts_program thy cs; |
|
459 val _ = map (fn ((target_name, strict), args) => |
455 val _ = map (fn ((target_name, strict), args) => |
460 check_code_for ctxt target_name strict args program all_public (map Constant cs)) seris; |
456 check_code_for ctxt target_name strict args program all_public (map Constant cs)) seris; |
461 in () end; |
457 in () end; |
462 |
458 |
463 fun check_code_cmd all_public raw_cs seris ctxt = |
459 fun check_code_cmd all_public raw_cs seris ctxt = |