src/Pure/codegen.ML
changeset 13886 0b243f6e257e
parent 13753 38b76f457b9c
child 14105 85d1a908f024
equal deleted inserted replaced
13885:de6fac7d5351 13886:0b243f6e257e
     9 signature CODEGEN =
     9 signature CODEGEN =
    10 sig
    10 sig
    11   val quiet_mode : bool ref
    11   val quiet_mode : bool ref
    12   val message : string -> unit
    12   val message : string -> unit
    13   val mode : string list ref
    13   val mode : string list ref
       
    14   val margin : int ref
    14 
    15 
    15   datatype 'a mixfix =
    16   datatype 'a mixfix =
    16       Arg
    17       Arg
    17     | Ignore
    18     | Ignore
    18     | Pretty of Pretty.T
    19     | Pretty of Pretty.T
    55 
    56 
    56 val quiet_mode = ref true;
    57 val quiet_mode = ref true;
    57 fun message s = if !quiet_mode then () else writeln s;
    58 fun message s = if !quiet_mode then () else writeln s;
    58 
    59 
    59 val mode = ref ([] : string list);
    60 val mode = ref ([] : string list);
       
    61 
       
    62 val margin = ref 80;
    60 
    63 
    61 (**** Mixfix syntax ****)
    64 (**** Mixfix syntax ****)
    62 
    65 
    63 datatype 'a mixfix =
    66 datatype 'a mixfix =
    64     Arg
    67     Arg
   425 
   428 
   426 
   429 
   427 fun output_code gr xs = implode (map (snd o Graph.get_node gr)
   430 fun output_code gr xs = implode (map (snd o Graph.get_node gr)
   428   (rev (Graph.all_preds gr xs)));
   431   (rev (Graph.all_preds gr xs)));
   429 
   432 
   430 fun gen_generate_code prep_term thy = Pretty.setmp_margin 80 (fn xs =>
   433 fun gen_generate_code prep_term thy = Pretty.setmp_margin (!margin) (fn xs =>
   431   let
   434   let
   432     val sg = sign_of thy;
   435     val sg = sign_of thy;
   433     val gr = Graph.new_node ("<Top>", (None, "")) Graph.empty;
   436     val gr = Graph.new_node ("<Top>", (None, "")) Graph.empty;
   434     val (gr', ps) = foldl_map (fn (gr, (s, t)) => apsnd (pair s)
   437     val (gr', ps) = foldl_map (fn (gr, (s, t)) => apsnd (pair s)
   435       (invoke_codegen thy "<Top>" false (gr, t)))
   438       (invoke_codegen thy "<Top>" false (gr, t)))