Margin for pretty-printing is now a mutable reference.
--- 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;