--- 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;