24 |
24 |
25 val export_code: bool -> string list |
25 val export_code: bool -> string list |
26 -> (((string * string) * ({physical: bool} * (Path.T * Position.T)) option) * Token.T list) list |
26 -> (((string * string) * ({physical: bool} * (Path.T * Position.T)) option) * Token.T list) list |
27 -> local_theory -> local_theory |
27 -> local_theory -> local_theory |
28 val export_code_cmd: bool -> string list |
28 val export_code_cmd: bool -> string list |
29 -> (((string * string) * ({physical: bool} * (string * Position.T)) option) * Token.T list) list |
29 -> (((string * string) * ({physical: bool} * Input.source) option) * Token.T list) list |
30 -> local_theory -> local_theory |
30 -> local_theory -> local_theory |
31 val produce_code: Proof.context -> bool -> string list |
31 val produce_code: Proof.context -> bool -> string list |
32 -> string -> string -> int option -> Token.T list -> (string list * string) list * string option list |
32 -> string -> string -> int option -> Token.T list -> (string list * string) list * string option list |
33 val present_code: Proof.context -> string list -> Code_Symbol.T list |
33 val present_code: Proof.context -> string list -> Code_Symbol.T list |
34 -> string -> string -> int option -> Token.T list -> string |
34 -> string -> string -> int option -> Token.T list -> string |
519 end; (* local *) |
519 end; (* local *) |
520 |
520 |
521 |
521 |
522 (* code generation *) |
522 (* code generation *) |
523 |
523 |
524 fun prep_destination (location, (s, pos)) = |
524 fun prep_destination (location, source) = |
525 if location = {physical = false} |
525 let |
526 then (location, Path.explode_pos (s, pos)) |
526 val s = Input.string_of source |
527 else |
527 val pos = Input.pos_of source |
528 let |
528 val delimited = Input.is_delimited source |
529 val _ = |
529 in |
530 if s = "" |
530 if location = {physical = false} |
531 then error ("Bad bad empty " ^ Markup.markup Markup.keyword2 "file" ^ " argument") |
531 then (location, Path.explode_pos (s, pos)) |
532 else (); |
532 else |
533 val _ = |
533 let |
534 legacy_feature |
534 val _ = |
535 (Markup.markup Markup.keyword1 "export_code" ^ " with " ^ |
535 if s = "" |
536 Markup.markup Markup.keyword2 "file" ^ " argument" ^ Position.here pos); |
536 then error ("Bad bad empty " ^ Markup.markup Markup.keyword2 "file" ^ " argument") |
537 val _ = Position.report pos Markup.language_path; |
537 else (); |
538 val path = #1 (Path.explode_pos (s, pos)); |
538 val _ = |
539 val _ = Position.report pos (Markup.path (Path.implode_symbolic path)); |
539 legacy_feature |
540 in (location, (path, pos)) end; |
540 (Markup.markup Markup.keyword1 "export_code" ^ " with " ^ |
|
541 Markup.markup Markup.keyword2 "file" ^ " argument" ^ Position.here pos); |
|
542 val _ = Position.report pos (Markup.language_path delimited); |
|
543 val path = #1 (Path.explode_pos (s, pos)); |
|
544 val _ = Position.report pos (Markup.path (Path.implode_symbolic path)); |
|
545 in (location, (path, pos)) end |
|
546 end; |
541 |
547 |
542 fun export_code all_public cs seris lthy = |
548 fun export_code all_public cs seris lthy = |
543 let |
549 let |
544 val program = Code_Thingol.consts_program lthy cs; |
550 val program = Code_Thingol.consts_program lthy cs; |
545 in |
551 in |
713 fun code_expr_inP (all_public, raw_cs) = |
719 fun code_expr_inP (all_public, raw_cs) = |
714 Scan.repeat (\<^keyword>\<open>in\<close> |-- Parse.!!! (Parse.name |
720 Scan.repeat (\<^keyword>\<open>in\<close> |-- Parse.!!! (Parse.name |
715 -- Scan.optional (\<^keyword>\<open>module_name\<close> |-- Parse.name) "" |
721 -- Scan.optional (\<^keyword>\<open>module_name\<close> |-- Parse.name) "" |
716 -- Scan.option |
722 -- Scan.option |
717 ((\<^keyword>\<open>file_prefix\<close> >> K {physical = false} || \<^keyword>\<open>file\<close> >> K {physical = true}) |
723 ((\<^keyword>\<open>file_prefix\<close> >> K {physical = false} || \<^keyword>\<open>file\<close> >> K {physical = true}) |
718 -- Parse.!!! (Parse.position Parse.path)) |
724 -- Parse.!!! Parse.path_input) |
719 -- code_expr_argsP)) |
725 -- code_expr_argsP)) |
720 >> (fn seri_args => export_code_cmd all_public raw_cs seri_args); |
726 >> (fn seri_args => export_code_cmd all_public raw_cs seri_args); |
721 |
727 |
722 fun code_expr_checkingP (all_public, raw_cs) = |
728 fun code_expr_checkingP (all_public, raw_cs) = |
723 (\<^keyword>\<open>checking\<close> |-- Parse.!!! |
729 (\<^keyword>\<open>checking\<close> |-- Parse.!!! |