src/Pure/codegen.ML
changeset 13886 0b243f6e257e
parent 13753 38b76f457b9c
child 14105 85d1a908f024
--- 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;