1.1 --- a/doc-src/more_antiquote.ML	Mon Mar 09 20:29:45 2009 +0100
     1.2 +++ b/doc-src/more_antiquote.ML	Mon Mar 09 20:34:11 2009 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      Doc/more_antiquote.ML
     1.5 +(*  Title:      doc-src/more_antiquote.ML
     1.6      Author:     Florian Haftmann, TU Muenchen
     1.7  
     1.8  More antiquotations.
     1.9 @@ -12,15 +12,13 @@
    1.10  structure More_Antiquote : MORE_ANTIQUOTE =
    1.11  struct
    1.12  
    1.13 -structure O = ThyOutput;
    1.14 -
    1.15  (* printing typewriter lines *)
    1.16  
    1.17  fun typewriter s =
    1.18    let
    1.19      val parse = Scan.repeat
    1.20        (Scan.this_string "\n" |-- Scan.succeed "\\\\\n\\hspace*{0pt}"
    1.21 -        || (Scan.this_string " " 
    1.22 +        || (Scan.this_string " "
    1.23            || Scan.this_string "."
    1.24            || Scan.this_string ","
    1.25            || Scan.this_string ":"
    1.26 @@ -66,9 +64,8 @@
    1.27  
    1.28  in
    1.29  
    1.30 -val _ = O.add_commands
    1.31 -  [("class", ThyOutput.args (Scan.lift Args.name) (K pr_class)),
    1.32 -    ("type", ThyOutput.args (Scan.lift Args.name) (K pr_type))]
    1.33 +val _ = ThyOutput.antiquotation "class" (Scan.lift Args.name) (pr_class o #context);
    1.34 +val _ = ThyOutput.antiquotation "type" (Scan.lift Args.name) (pr_type o #context);
    1.35  
    1.36  end;
    1.37  
    1.38 @@ -96,12 +93,12 @@
    1.39      val thms = Code_Wellsorted.eqns funcgr const
    1.40        |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
    1.41        |> map (holize o no_vars ctxt o AxClass.overload thy);
    1.42 -  in ThyOutput.output_list pretty_thm src ctxt thms end;
    1.43 +  in ThyOutput.output (ThyOutput.maybe_pretty_source (pretty_thm ctxt) src thms) end;
    1.44  
    1.45  in
    1.46  
    1.47 -val _ = O.add_commands
    1.48 -  [("code_thms", ThyOutput.args Args.term pretty_code_thm)];
    1.49 +val _ = ThyOutput.antiquotation "code_thms" Args.term
    1.50 +  (fn {source, context, ...} => pretty_code_thm source context);
    1.51  
    1.52  end;
    1.53  
    1.54 @@ -120,21 +117,20 @@
    1.55      >> (fn classes => fn thy => fn naming => map_filter (Code_Thingol.lookup_class naming o Sign.intern_class thy) classes);
    1.56    val parse_instances = Scan.lift (Args.parens (Args.$$$ "instances") |-- Scan.repeat1 (Args.name --| Args.$$$ "::" -- Args.name))
    1.57      >> (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);
    1.58 -  val parse_names = parse_consts || parse_types || parse_classes || parse_instances; 
    1.59 -
    1.60 -  fun code_stmts src ctxt ((mk_cs, mk_stmtss), target) =
    1.61 -    Code_Target.code_of (ProofContext.theory_of ctxt)
    1.62 -      target "Example" (mk_cs (ProofContext.theory_of ctxt))
    1.63 -        (fn naming => maps (fn f => f (ProofContext.theory_of ctxt) naming) mk_stmtss)
    1.64 -    |> typewriter;
    1.65 +  val parse_names = parse_consts || parse_types || parse_classes || parse_instances;
    1.66  
    1.67  in
    1.68  
    1.69 -val _ = O.add_commands
    1.70 -  [("code_stmts", O.args
    1.71 -      (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name))
    1.72 -        code_stmts)]
    1.73 -
    1.74 -end
    1.75 +val _ = ThyOutput.antiquotation "code_stmts"
    1.76 +  (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name))
    1.77 +  (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), target) =>
    1.78 +    let val thy = ProofContext.theory_of ctxt in
    1.79 +      Code_Target.code_of thy
    1.80 +        target "Example" (mk_cs thy)
    1.81 +        (fn naming => maps (fn f => f thy naming) mk_stmtss)
    1.82 +      |> typewriter
    1.83 +    end);
    1.84  
    1.85  end;
    1.86 +
    1.87 +end;