# HG changeset patch
# User wenzelm
# Date 1590606164 -7200
# Node ID 8357ee06ade15619fff97fbe65867b8db42053c2
# Parent  b9fbc93f3a248cff14262436abc9bd0ed97f2db2
adapted to d25093536482;

diff -r b9fbc93f3a24 -r 8357ee06ade1 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Wed May 27 20:51:25 2020 +0200
+++ b/src/Doc/antiquote_setup.ML	Wed May 27 21:02:44 2020 +0200
@@ -143,8 +143,8 @@
   if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then name
   else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos);
 
-fun check_system_option ctxt (name, pos) =
-  (Context_Position.report ctxt pos (Options.default_markup (name, pos)); true)
+fun check_system_option ctxt arg =
+  (Completion.check_option (Options.default ()) ctxt arg; true)
     handle ERROR _ => false;
 
 val arg = enclose "{" "}" o clean_string;