1.1 --- a/doc-src/more_antiquote.ML	Tue Aug 31 16:23:58 2010 +0200
     1.2 +++ b/doc-src/more_antiquote.ML	Tue Aug 31 16:51:29 2010 +0200
     1.3 @@ -124,12 +124,13 @@
     1.4  in
     1.5  
     1.6  val _ = Thy_Output.antiquotation "code_stmts"
     1.7 -  (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name))
     1.8 -  (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), target) =>
     1.9 +  (parse_const_terms -- Scan.repeat parse_names
    1.10 +    -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
    1.11 +  (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target, some_width)) =>
    1.12      let val thy = ProofContext.theory_of ctxt in
    1.13        Code_Target.present_code thy (mk_cs thy)
    1.14          (fn naming => maps (fn f => f thy naming) mk_stmtss)
    1.15 -        target NONE (SOME "Example") []
    1.16 +        target some_width "Example" []
    1.17        |> typewriter
    1.18      end);
    1.19