# HG changeset patch # User berghofe # Date 1048937333 -3600 # Node ID 0b243f6e257e8a795a311c2c12eb27632c8a33f1 # Parent de6fac7d5351bca776482cee352cbb931c700547 Margin for pretty-printing is now a mutable reference. diff -r de6fac7d5351 -r 0b243f6e257e src/Pure/codegen.ML --- a/src/Pure/codegen.ML Wed Mar 26 12:25:56 2003 +0100 +++ b/src/Pure/codegen.ML Sat Mar 29 12:28:53 2003 +0100 @@ -11,6 +11,7 @@ val quiet_mode : bool ref val message : string -> unit val mode : string list ref + val margin : int ref datatype 'a mixfix = Arg @@ -58,6 +59,8 @@ val mode = ref ([] : string list); +val margin = ref 80; + (**** Mixfix syntax ****) datatype 'a mixfix = @@ -427,7 +430,7 @@ fun output_code gr xs = implode (map (snd o Graph.get_node gr) (rev (Graph.all_preds gr xs))); -fun gen_generate_code prep_term thy = Pretty.setmp_margin 80 (fn xs => +fun gen_generate_code prep_term thy = Pretty.setmp_margin (!margin) (fn xs => let val sg = sign_of thy; val gr = Graph.new_node ("", (None, "")) Graph.empty;