recovered Options.default_markup, e.g. for src/Doc/antiquote_setup.ML (amending 16519cd83ed4);
authorwenzelm
Sat Dec 16 14:24:12 2017 +0100 (17 months ago)
changeset 672119e9b78b8e6ca
parent 67210 f80bdbe76934
child 67212 f5d44a01030c
recovered Options.default_markup, e.g. for src/Doc/antiquote_setup.ML (amending 16519cd83ed4);
src/Pure/System/options.ML
     1.1 --- a/src/Pure/System/options.ML	Sat Dec 16 12:28:46 2017 +0100
     1.2 +++ b/src/Pure/System/options.ML	Sat Dec 16 14:24:12 2017 +0100
     1.3 @@ -29,6 +29,7 @@
     1.4    val update: string -> string -> T -> T
     1.5    val decode: XML.body -> T
     1.6    val default: unit -> T
     1.7 +  val default_markup: string * Position.T -> Markup.T
     1.8    val default_typ: string -> string
     1.9    val default_bool: string -> bool
    1.10    val default_int: string -> int
    1.11 @@ -188,6 +189,7 @@
    1.12      SOME options => options
    1.13    | NONE => err_no_default ());
    1.14  
    1.15 +fun default_markup arg = markup (default ()) arg;
    1.16  fun default_typ name = typ (default ()) name;
    1.17  fun default_bool name = bool (default ()) name;
    1.18  fun default_int name = int (default ()) name;