equal
deleted
inserted
replaced
148 fun no_check _ _ = true; |
148 fun no_check _ _ = true; |
149 |
149 |
150 fun is_keyword ctxt (name, _) = |
150 fun is_keyword ctxt (name, _) = |
151 Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name; |
151 Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name; |
152 |
152 |
153 fun check_command ctxt (name, pos) = |
153 fun check_command ctxt (name, pos) = (Outer_Syntax.check_command ctxt (name, pos); true); |
154 let |
|
155 val thy = Proof_Context.theory_of ctxt; |
|
156 val keywords = Thy_Header.get_keywords thy; |
|
157 in |
|
158 Keyword.is_command keywords name andalso |
|
159 let |
|
160 val markup = |
|
161 Token.explode keywords Position.none name |
|
162 |> maps (Outer_Syntax.command_reports thy) |
|
163 |> map (snd o fst); |
|
164 val _ = Context_Position.reports ctxt (map (pair pos) markup); |
|
165 in true end |
|
166 end; |
|
167 |
154 |
168 fun check_system_option ctxt (name, pos) = |
155 fun check_system_option ctxt (name, pos) = |
169 (Context_Position.report ctxt pos (Options.default_markup (name, pos)); true) |
156 (Context_Position.report ctxt pos (Options.default_markup (name, pos)); true) |
170 handle ERROR _ => false; |
157 handle ERROR _ => false; |
171 |
158 |