added code_stmts antiquotation from doc-src/more_antiquote.ML
authorhaftmann
Thu Sep 16 17:31:51 2010 +0200 (2010-09-16)
changeset 39480a2ed61449dcc
parent 39479 465064e8f269
child 39481 f15514acc942
added code_stmts antiquotation from doc-src/more_antiquote.ML
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_target.ML	Thu Sep 16 17:31:51 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Thu Sep 16 17:31:51 2010 +0200
     1.3 @@ -441,6 +441,43 @@
     1.4  
     1.5  fun check_code_cmd raw_cs seris thy = check_code thy (read_const_exprs thy raw_cs) seris;
     1.6  
     1.7 +local
     1.8 +
     1.9 +val parse_const_terms = Scan.repeat1 Args.term
    1.10 +  >> (fn ts => fn thy => map (Code.check_const thy) ts);
    1.11 +
    1.12 +fun parse_names category parse internalize lookup =
    1.13 +  Scan.lift (Args.parens (Args.$$$ category)) |-- Scan.repeat1 parse
    1.14 +  >> (fn xs => fn thy => fn naming => map_filter (lookup naming o internalize thy) xs);
    1.15 +  
    1.16 +val parse_consts = parse_names "consts" Args.term
    1.17 +  Code.check_const Code_Thingol.lookup_const ;
    1.18 +
    1.19 +val parse_types = parse_names "types" (Scan.lift Args.name)
    1.20 +  Sign.intern_type Code_Thingol.lookup_tyco;
    1.21 +
    1.22 +val parse_classes = parse_names "classes" (Scan.lift Args.name)
    1.23 +  Sign.intern_class Code_Thingol.lookup_class;
    1.24 +
    1.25 +val parse_instances = parse_names "instances" (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name))
    1.26 +  (fn thy => fn (raw_tyco, raw_class) => (Sign.intern_class thy raw_class, Sign.intern_type thy raw_tyco))
    1.27 +    Code_Thingol.lookup_instance;
    1.28 +
    1.29 +in
    1.30 +
    1.31 +val _ = Thy_Output.antiquotation "code_stmts"
    1.32 +  (parse_const_terms -- Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances)
    1.33 +    -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
    1.34 +  (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target, some_width)) =>
    1.35 +    let val thy = ProofContext.theory_of ctxt in
    1.36 +      present_code thy (mk_cs thy)
    1.37 +        (fn naming => maps (fn f => f thy naming) mk_stmtss)
    1.38 +        target some_width "Example" []
    1.39 +      |> Latex.output_typewriter
    1.40 +    end);
    1.41 +
    1.42 +end;
    1.43 +
    1.44  
    1.45  (** serializer configuration **)
    1.46