recovered Options.default_markup, e.g. for src/Doc/antiquote_setup.ML (amending 16519cd83ed4);
authorwenzelm
Sat, 16 Dec 2017 14:24:12 +0100
changeset 67211 9e9b78b8e6ca
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
--- a/src/Pure/System/options.ML	Sat Dec 16 12:28:46 2017 +0100
+++ b/src/Pure/System/options.ML	Sat Dec 16 14:24:12 2017 +0100
@@ -29,6 +29,7 @@
   val update: string -> string -> T -> T
   val decode: XML.body -> T
   val default: unit -> T
+  val default_markup: string * Position.T -> Markup.T
   val default_typ: string -> string
   val default_bool: string -> bool
   val default_int: string -> int
@@ -188,6 +189,7 @@
     SOME options => options
   | NONE => err_no_default ());
 
+fun default_markup arg = markup (default ()) arg;
 fun default_typ name = typ (default ()) name;
 fun default_bool name = bool (default ()) name;
 fun default_int name = int (default ()) name;