option "goals_limit", with more uniform description;

--- a/etc/options	Mon May 13 13:01:10 2013 +0200
+++ b/etc/options	Mon May 13 13:23:13 2013 +0200
@@ -14,6 +14,9 @@
 option document_graph : bool = false
   -- "generate session graph image for document"
 
+option goals_limit : int = 10
+  -- "maximum number of subgoals to be printed"
+
 option show_question_marks : bool = true
   -- "show leading question mark of schematic variables"
 

--- a/src/Doc/IsarRef/Document_Preparation.thy	Mon May 13 13:01:10 2013 +0200
+++ b/src/Doc/IsarRef/Document_Preparation.thy	Mon May 13 13:23:13 2013 +0200
@@ -358,7 +358,7 @@
   or indentation for pretty printing of display material.
 
   \item @{antiquotation_option_def goals_limit}~@{text "= nat"}
-  determines the maximum number of goals to be printed (for goal-based
+  determines the maximum number of subgoals to be printed (for goal-based
   antiquotation).
 
   \item @{antiquotation_option_def source}~@{text "= bool"} prints the

--- a/src/Doc/IsarRef/Inner_Syntax.thy	Mon May 13 13:01:10 2013 +0200
+++ b/src/Doc/IsarRef/Inner_Syntax.thy	Mon May 13 13:23:13 2013 +0200
@@ -213,7 +213,7 @@
   might look at terms more discretely.
 
   \item @{attribute goals_limit} controls the maximum number of
-  subgoals to be shown in goal output.
+  subgoals to be printed.
 
   \item @{attribute show_main_goal} controls whether the main result
   to be proven should be displayed.  This information might be

--- a/src/Pure/Isar/isar_syn.ML	Mon May 13 13:01:10 2013 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon May 13 13:23:13 2013 +0200
@@ -975,7 +975,7 @@
   Outer_Syntax.improper_command @{command_spec "pr"} "print current proof state (if present)"
     (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
       Toplevel.keep (fn state =>
-       (case limit of NONE => () | SOME n => Goal_Display.goals_limit_default := n;
+       (case limit of NONE => () | SOME n => Options.default_put_int "goals_limit" n;
         Toplevel.quiet := false;
         Print_Mode.with_modes modes (Toplevel.print_state true) state))));
 

--- a/src/Pure/ProofGeneral/preferences.ML	Mon May 13 13:01:10 2013 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Mon May 13 13:23:13 2013 +0200
@@ -159,9 +159,9 @@
     "Print terms eta-contracted"];
 
 val advanced_display_preferences =
- [nat_pref Goal_Display.goals_limit_default
+ [options_pref "goals_limit"
     "goals-limit"
-    "Setting for maximum number of goals printed",
+    "Setting for maximum number of subgoals to be printed",
   print_depth_pref,
   options_pref "show_question_marks"
     "show-question-marks"

--- a/src/Pure/goal_display.ML	Mon May 13 13:01:10 2013 +0200
+++ b/src/Pure/goal_display.ML	Mon May 13 13:23:13 2013 +0200
@@ -7,7 +7,6 @@
 
 signature GOAL_DISPLAY =
 sig
-  val goals_limit_default: int Unsynchronized.ref
   val goals_limit_raw: Config.raw
   val goals_limit: int Config.T
   val show_main_goal_default: bool Unsynchronized.ref
@@ -26,8 +25,7 @@
 structure Goal_Display: GOAL_DISPLAY =
 struct
 
-val goals_limit_default = Unsynchronized.ref 10;
-val goals_limit_raw = Config.declare "goals_limit" (fn _ => Config.Int (! goals_limit_default));
+val goals_limit_raw = Config.declare_option "goals_limit";
 val goals_limit = Config.int goals_limit_raw;
 
 val show_main_goal_default = Unsynchronized.ref false;