# 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 ("<Top>", (None, "")) Graph.empty;