# HG changeset patch
# User wenzelm
# Date 1513430652 -3600
# Node ID 9e9b78b8e6cac69d41d9e5a7d834febcad24410b
# Parent  f80bdbe76934ec6ddc9552dfef0638277f5df74e
recovered Options.default_markup, e.g. for src/Doc/antiquote_setup.ML (amending 16519cd83ed4);

diff -r f80bdbe76934 -r 9e9b78b8e6ca 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;