equal
deleted
inserted
replaced
141 |
141 |
142 fun check_keyword ctxt (name, pos) = |
142 fun check_keyword ctxt (name, pos) = |
143 if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then name |
143 if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then name |
144 else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos); |
144 else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos); |
145 |
145 |
146 fun check_system_option ctxt (name, pos) = |
146 fun check_system_option ctxt arg = |
147 (Context_Position.report ctxt pos (Options.default_markup (name, pos)); true) |
147 (Completion.check_option (Options.default ()) ctxt arg; true) |
148 handle ERROR _ => false; |
148 handle ERROR _ => false; |
149 |
149 |
150 val arg = enclose "{" "}" o clean_string; |
150 val arg = enclose "{" "}" o clean_string; |
151 |
151 |
152 fun entity check markup binding index = |
152 fun entity check markup binding index = |