111 local |
111 local |
112 |
112 |
113 val parse_const_terms = Scan.repeat1 Args.term |
113 val parse_const_terms = Scan.repeat1 Args.term |
114 >> (fn ts => fn thy => map (Code_Unit.check_const thy) ts); |
114 >> (fn ts => fn thy => map (Code_Unit.check_const thy) ts); |
115 val parse_consts = Scan.lift (Args.parens (Args.$$$ "consts")) |-- parse_const_terms |
115 val parse_consts = Scan.lift (Args.parens (Args.$$$ "consts")) |-- parse_const_terms |
116 >> (fn mk_cs => fn thy => fn naming => map (the o Code_Thingol.lookup_const naming) (mk_cs thy)); |
116 >> (fn mk_cs => fn thy => fn naming => map_filter (Code_Thingol.lookup_const naming) (mk_cs thy)); |
117 val parse_types = Scan.lift (Args.parens (Args.$$$ "types") |-- Scan.repeat1 Args.name) |
117 val parse_types = Scan.lift (Args.parens (Args.$$$ "types") |-- Scan.repeat1 Args.name) |
118 >> (fn tycos => fn thy => fn naming => map (the o Code_Thingol.lookup_tyco naming o Sign.intern_type thy) tycos); |
118 >> (fn tycos => fn thy => fn naming => map_filter (Code_Thingol.lookup_tyco naming o Sign.intern_type thy) tycos); |
119 val parse_classes = Scan.lift (Args.parens (Args.$$$ "classes") |-- Scan.repeat1 Args.name) |
119 val parse_classes = Scan.lift (Args.parens (Args.$$$ "classes") |-- Scan.repeat1 Args.name) |
120 >> (fn classes => fn thy => fn naming => map (the o Code_Thingol.lookup_class naming o Sign.intern_class thy) classes); |
120 >> (fn classes => fn thy => fn naming => map_filter (Code_Thingol.lookup_class naming o Sign.intern_class thy) classes); |
121 val parse_instances = Scan.lift (Args.parens (Args.$$$ "instances") |-- Scan.repeat1 (Args.name --| Args.$$$ "::" -- Args.name)) |
121 val parse_instances = Scan.lift (Args.parens (Args.$$$ "instances") |-- Scan.repeat1 (Args.name --| Args.$$$ "::" -- Args.name)) |
122 >> (fn insts => fn thy => fn naming => map (the o Code_Thingol.lookup_instance naming o apsnd (Sign.intern_type thy) o apfst (Sign.intern_class thy) o swap) insts); |
122 >> (fn insts => fn thy => fn naming => map_filter (Code_Thingol.lookup_instance naming o apsnd (Sign.intern_type thy) o apfst (Sign.intern_class thy) o swap) insts); |
123 val parse_names = parse_consts || parse_types || parse_classes || parse_instances; |
123 val parse_names = parse_consts || parse_types || parse_classes || parse_instances; |
124 |
124 |
125 fun code_stmts src ctxt ((mk_cs, mk_stmtss), target) = |
125 fun code_stmts src ctxt ((mk_cs, mk_stmtss), target) = |
126 Code_Target.code_of (ProofContext.theory_of ctxt) |
126 Code_Target.code_of (ProofContext.theory_of ctxt) |
127 target "Example" (mk_cs (ProofContext.theory_of ctxt)) |
127 target "Example" (mk_cs (ProofContext.theory_of ctxt)) |