adapted to d25093536482;
authorwenzelm
Wed, 27 May 2020 21:02:44 +0200
changeset 72140 8357ee06ade1
parent 72139 b9fbc93f3a24
child 72141 3867734b9a40
adapted to d25093536482;
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;