# HG changeset patch # User wenzelm # Date 1368375616 -7200 # Node ID 449fbf64f4a5c838db8a30f418b2d5b8dcc772c8 # Parent 5b1ac9843f0276d3e0de752e8b6a810fdf3e90c7 tuned signature; diff -r 5b1ac9843f02 -r 449fbf64f4a5 src/Pure/ML/ml_antiquote.ML --- a/src/Pure/ML/ml_antiquote.ML Sun May 12 17:56:53 2013 +0200 +++ b/src/Pure/ML/ml_antiquote.ML Sun May 12 18:20:16 2013 +0200 @@ -68,7 +68,7 @@ inline (Binding.name "make_string") (Scan.succeed ml_make_string) #> value (Binding.name "option_default") (Scan.lift Args.name >> (fn name => - let val typ = Options.typ (Options.default ()) name + let val typ = Options.default_typ name in "fn () => Options.default_" ^ typ ^ " " ^ ML_Syntax.print_string name end)) #> value (Binding.name "binding") diff -r 5b1ac9843f02 -r 449fbf64f4a5 src/Pure/ProofGeneral/preferences.ML --- a/src/Pure/ProofGeneral/preferences.ML Sun May 12 17:56:53 2013 +0200 +++ b/src/Pure/ProofGeneral/preferences.ML Sun May 12 18:20:16 2013 +0200 @@ -58,8 +58,7 @@ fun options_pref option_name pgip_name descr : preference = let - val options = Options.default (); - val typ = Options.typ options option_name; + val typ = Options.default_typ option_name; val pgiptype = if typ = Options.boolT then PgipTypes.Pgipbool else if typ = Options.intT then PgipTypes.Pgipint (NONE, NONE) diff -r 5b1ac9843f02 -r 449fbf64f4a5 src/Pure/System/options.ML --- a/src/Pure/System/options.ML Sun May 12 17:56:53 2013 +0200 +++ b/src/Pure/System/options.ML Sun May 12 18:20:16 2013 +0200 @@ -26,6 +26,7 @@ val update: string -> string -> T -> T val decode: XML.body -> T val default: unit -> T + val default_typ: string -> string val default_bool: string -> bool val default_int: string -> int val default_real: string -> real @@ -159,6 +160,7 @@ SOME options => options | NONE => err_no_default ()); +fun default_typ name = typ (default ()) name; fun default_bool name = bool (default ()) name; fun default_int name = int (default ()) name; fun default_real name = real (default ()) name;