# HG changeset patch
# User haftmann
# Date 1420789020 -3600
# Node ID f5f9993a168daceefcafcbc83c7b1e611e48bca5
# Parent  468bd3aedfa128b4b0b459e9798ced1e6103bf03
prefer option for default code printing width

diff -r 468bd3aedfa1 -r f5f9993a168d src/Doc/Classes/Setup.thy
--- a/src/Doc/Classes/Setup.thy	Fri Jan 09 08:36:59 2015 +0100
+++ b/src/Doc/Classes/Setup.thy	Fri Jan 09 08:37:00 2015 +0100
@@ -5,9 +5,7 @@
 ML_file "../antiquote_setup.ML"
 ML_file "../more_antiquote.ML"
 
-setup {*
-  Code_Target.set_default_code_width 74
-*}
+declare [[default_code_width = 74]]
 
 syntax
   "_alpha" :: "type"  ("\<alpha>")
diff -r 468bd3aedfa1 -r f5f9993a168d src/Doc/Codegen/Setup.thy
--- a/src/Doc/Codegen/Setup.thy	Fri Jan 09 08:36:59 2015 +0100
+++ b/src/Doc/Codegen/Setup.thy	Fri Jan 09 08:37:00 2015 +0100
@@ -28,9 +28,8 @@
 end
 *}
 
-setup {* Code_Target.set_default_code_width 74 *}
+declare [[default_code_width = 74]]
 
 declare [[names_unique = false]]
 
 end
-
diff -r 468bd3aedfa1 -r f5f9993a168d src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Fri Jan 09 08:36:59 2015 +0100
+++ b/src/Tools/Code/code_target.ML	Fri Jan 09 08:37:00 2015 +0100
@@ -45,7 +45,7 @@
   val serialization: (int -> Path.T option -> 'a -> unit)
     -> (Code_Symbol.T list -> int -> 'a -> (string * string) list * (Code_Symbol.T -> string option))
     -> 'a -> serialization
-  val set_default_code_width: int -> theory -> theory
+  val default_code_width: int Config.T
 
   type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl
   val set_identifiers: (string, string, string, string, string, string) symbol_attr_decl
@@ -188,21 +188,21 @@
 
 structure Targets = Theory_Data
 (
-  type T = (target * Code_Printer.data) Symtab.table * int;
-  val empty = (Symtab.empty, 80);
+  type T = (target * Code_Printer.data) Symtab.table;
+  val empty = Symtab.empty;
   val extend = I;
-  fun merge ((targets1, width1), (targets2, width2)) : T =
-    (Symtab.join (fn target_name => fn ((target1, data1), (target2, data2)) =>
+  fun merge (targets1, targets2) : T =
+    Symtab.join (fn target_name => fn ((target1, data1), (target2, data2)) =>
       if #serial target1 = #serial target2 then
       ({ serial = #serial target1, language = #language target1,
         ancestry = merge_ancestry (#ancestry target1, #ancestry target2)},
         Code_Printer.merge_data (data1, data2))
       else error ("Incompatible targets: " ^ quote target_name) 
-    ) (targets1, targets2), Int.max (width1, width2))
+    ) (targets1, targets2)
 );
 
-fun exists_target thy = Symtab.defined (fst (Targets.get thy));
-fun lookup_target_data thy = Symtab.lookup (fst (Targets.get thy));
+fun exists_target thy = Symtab.defined (Targets.get thy);
+fun lookup_target_data thy = Symtab.lookup (Targets.get thy);
 
 fun fold1 f xs = fold f (tl xs) (hd xs);
 
@@ -229,7 +229,7 @@
       else ();
   in
     thy
-    |> (Targets.map o apfst o Symtab.update) (target_name, (target, Code_Printer.empty_data))  
+    |> (Targets.map o Symtab.update) (target_name, (target, Code_Printer.empty_data))  
   end;
 
 fun add_language (target_name, language) =
@@ -259,7 +259,7 @@
     val _ = assert_target (Proof_Context.init_global thy) target_name;
   in
     thy
-    |> (Targets.map o apfst o Symtab.map_entry target_name o apsnd o Code_Printer.map_data) f
+    |> (Targets.map o Symtab.map_entry target_name o apsnd o Code_Printer.map_data) f
   end;
 
 fun map_reserved target_name =
@@ -269,11 +269,14 @@
 fun map_printings target_name =
   map_data target_name o @{apply 3 (3)};
 
-fun set_default_code_width k = (Targets.map o apsnd) (K k);
-
 
 (** serializer usage **)
 
+(* technical aside: pretty printing width *)
+
+val default_code_width = Attrib.setup_config_int @{binding "default_code_width"} (K 80);
+
+
 (* montage *)
 
 fun the_language ctxt =
@@ -285,10 +288,9 @@
 
 fun activate_target ctxt target_name =
   let
-    val thy = Proof_Context.theory_of ctxt
-    val (_, default_width) = Targets.get thy;
+    val thy = Proof_Context.theory_of ctxt;
     val (modify, target_data) = join_ancestry thy target_name;
-  in (default_width, target_data, modify) end;
+  in (target_data, modify) end;
 
 fun project_program ctxt syms_hidden syms1 program2 =
   let
@@ -326,7 +328,8 @@
 
 fun mount_serializer ctxt target_name some_width module_name args program syms =
   let
-    val (default_width, (target, data), modify) = activate_target ctxt target_name;
+    val default_width = Config.get ctxt default_code_width;
+    val ((target, data), modify) = activate_target ctxt target_name;
     val serializer = (#serializer o #language) target;
     val (prepared_serializer, (prepared_syms, prepared_program)) =
       prepare_serializer ctxt serializer