--- a/doc-src/more_antiquote.ML Tue Aug 31 16:23:58 2010 +0200
+++ b/doc-src/more_antiquote.ML Tue Aug 31 16:51:29 2010 +0200
@@ -124,12 +124,13 @@
in
val _ = Thy_Output.antiquotation "code_stmts"
- (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name))
- (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), target) =>
+ (parse_const_terms -- Scan.repeat parse_names
+ -- 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
Code_Target.present_code thy (mk_cs thy)
(fn naming => maps (fn f => f thy naming) mk_stmtss)
- target NONE (SOME "Example") []
+ target some_width "Example" []
|> typewriter
end);