--- a/src/HOL/SPARK/Tools/spark_commands.ML Fri Nov 27 19:56:30 2020 +0100
+++ b/src/HOL/SPARK/Tools/spark_commands.ML Fri Nov 27 21:59:23 2020 +0100
@@ -94,13 +94,13 @@
val _ =
Outer_Syntax.command \<^command_keyword>\<open>spark_open_vcg\<close>
"open a new SPARK environment and load a SPARK-generated .vcg file"
- (Resources.provide_parse_files "spark_open_vcg" -- Parse.parname
+ (Resources.provide_parse_files (Resources.extensions ["vcg", "fdl", "rls"]) -- Parse.parname
>> (Toplevel.theory o spark_open Fdl_Lexer.vcg_header));
val _ =
Outer_Syntax.command \<^command_keyword>\<open>spark_open\<close>
"open a new SPARK environment and load a SPARK-generated .siv file"
- (Resources.provide_parse_files "spark_open" -- Parse.parname
+ (Resources.provide_parse_files (Resources.extensions ["siv", "fdl", "rls"]) -- Parse.parname
>> (Toplevel.theory o spark_open Fdl_Lexer.siv_header));
val pfun_type = Scan.option