# HG changeset patch
# User haftmann
# Date 1284651111 -7200
# Node ID a2ed61449dcc59f1c4c77feafebbdb68b11b7b2e
# Parent  465064e8f2691c934fc2ab5c02946abdf9174d25
added code_stmts antiquotation from doc-src/more_antiquote.ML

diff -r 465064e8f269 -r a2ed61449dcc src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Thu Sep 16 17:31:51 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Thu Sep 16 17:31:51 2010 +0200
@@ -441,6 +441,43 @@
 
 fun check_code_cmd raw_cs seris thy = check_code thy (read_const_exprs thy raw_cs) seris;
 
+local
+
+val parse_const_terms = Scan.repeat1 Args.term
+  >> (fn ts => fn thy => map (Code.check_const thy) ts);
+
+fun parse_names category parse internalize lookup =
+  Scan.lift (Args.parens (Args.$$$ category)) |-- Scan.repeat1 parse
+  >> (fn xs => fn thy => fn naming => map_filter (lookup naming o internalize thy) xs);
+  
+val parse_consts = parse_names "consts" Args.term
+  Code.check_const Code_Thingol.lookup_const ;
+
+val parse_types = parse_names "types" (Scan.lift Args.name)
+  Sign.intern_type Code_Thingol.lookup_tyco;
+
+val parse_classes = parse_names "classes" (Scan.lift Args.name)
+  Sign.intern_class Code_Thingol.lookup_class;
+
+val parse_instances = parse_names "instances" (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name))
+  (fn thy => fn (raw_tyco, raw_class) => (Sign.intern_class thy raw_class, Sign.intern_type thy raw_tyco))
+    Code_Thingol.lookup_instance;
+
+in
+
+val _ = Thy_Output.antiquotation "code_stmts"
+  (parse_const_terms -- Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances)
+    -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
+  (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target, some_width)) =>
+    let val thy = ProofContext.theory_of ctxt in
+      present_code thy (mk_cs thy)
+        (fn naming => maps (fn f => f thy naming) mk_stmtss)
+        target some_width "Example" []
+      |> Latex.output_typewriter
+    end);
+
+end;
+
 
 (** serializer configuration **)