src/Tools/Code/code_target.ML
changeset 43564 9864182c6bad
parent 43324 2b47822868e4
child 43850 7f2cbc713344
     1.1 --- a/src/Tools/Code/code_target.ML	Mon Jun 27 17:51:28 2011 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Mon Jun 27 22:20:49 2011 +0200
     1.3 @@ -60,6 +60,8 @@
     1.4    val add_include: string -> string * (string * string list) option -> theory -> theory
     1.5  
     1.6    val codegen_tool: string (*theory name*) -> string (*export_code expr*) -> unit
     1.7 +
     1.8 +  val setup: theory -> theory
     1.9  end;
    1.10  
    1.11  structure Code_Target : CODE_TARGET =
    1.12 @@ -143,7 +145,7 @@
    1.13  };
    1.14  
    1.15  fun make_target ((serial, description), ((reserved, includes), (module_alias, symbol_syntax))) =
    1.16 -  Target { serial = serial, description = description, reserved = reserved, 
    1.17 +  Target { serial = serial, description = description, reserved = reserved,
    1.18      includes = includes, module_alias = module_alias, symbol_syntax = symbol_syntax };
    1.19  fun map_target f ( Target { serial, description, reserved, includes, module_alias, symbol_syntax } ) =
    1.20    make_target (f ((serial, description), ((reserved, includes), (module_alias, symbol_syntax))));
    1.21 @@ -199,7 +201,7 @@
    1.22            | _ => true);
    1.23      val _ = if overwriting
    1.24        then warning ("Overwriting existing target " ^ quote target)
    1.25 -      else (); 
    1.26 +      else ();
    1.27    in
    1.28      thy
    1.29      |> (Targets.map o apfst o apfst o Symtab.update)
    1.30 @@ -251,7 +253,7 @@
    1.31  fun collapse_hierarchy thy =
    1.32    let
    1.33      val ((targets, _), _) = Targets.get thy;
    1.34 -    fun collapse target = 
    1.35 +    fun collapse target =
    1.36        let
    1.37          val data = case Symtab.lookup targets target
    1.38           of SOME data => data
    1.39 @@ -352,7 +354,7 @@
    1.40      val serializer = case the_description data
    1.41       of Fundamental seri => #serializer seri;
    1.42      val reserved = the_reserved data;
    1.43 -    val module_alias = the_module_alias data 
    1.44 +    val module_alias = the_module_alias data
    1.45      val { class, instance, tyco, const } = the_symbol_syntax data;
    1.46      val literals = the_literals thy target;
    1.47      val (prepared_serializer, prepared_program) = prepare_serializer thy
    1.48 @@ -396,7 +398,7 @@
    1.49      val { env_var, make_destination, make_command } =
    1.50        (#check o the_fundamental thy) target;
    1.51      fun ext_check p =
    1.52 -      let 
    1.53 +      let
    1.54          val destination = make_destination p;
    1.55          val _ = export (SOME destination) (invoke_serializer thy target (SOME 80)
    1.56            module_name args naming program names_cs);
    1.57 @@ -495,7 +497,7 @@
    1.58  fun parse_names category parse internalize lookup =
    1.59    Scan.lift (Args.parens (Args.$$$ category)) |-- Scan.repeat1 parse
    1.60    >> (fn xs => fn thy => fn naming => map_filter (lookup naming o internalize thy) xs);
    1.61 -  
    1.62 +
    1.63  val parse_consts = parse_names "consts" Args.term
    1.64    Code.check_const Code_Thingol.lookup_const ;
    1.65  
    1.66 @@ -511,15 +513,17 @@
    1.67  
    1.68  in
    1.69  
    1.70 -val _ = Thy_Output.antiquotation "code_stmts"
    1.71 -  (parse_const_terms -- Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances)
    1.72 -    -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
    1.73 -  (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target, some_width)) =>
    1.74 -    let val thy = Proof_Context.theory_of ctxt in
    1.75 -      present_code thy (mk_cs thy)
    1.76 -        (fn naming => maps (fn f => f thy naming) mk_stmtss)
    1.77 -        target some_width "Example" []
    1.78 -    end);
    1.79 +val antiq_setup =
    1.80 +  Thy_Output.antiquotation @{binding code_stmts}
    1.81 +    (parse_const_terms --
    1.82 +      Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances)
    1.83 +      -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
    1.84 +    (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target, some_width)) =>
    1.85 +      let val thy = Proof_Context.theory_of ctxt in
    1.86 +        present_code thy (mk_cs thy)
    1.87 +          (fn naming => maps (fn f => f thy naming) mk_stmtss)
    1.88 +          target some_width "Example" []
    1.89 +      end);
    1.90  
    1.91  end;
    1.92  
    1.93 @@ -745,4 +749,9 @@
    1.94      | NONE => error ("Bad directive " ^ quote cmd_expr)
    1.95    end;
    1.96  
    1.97 +
    1.98 +(** theory setup **)
    1.99 +
   1.100 +val setup = antiq_setup;
   1.101 +
   1.102  end; (*struct*)