--- a/src/HOL/SPARK/Tools/spark_commands.ML Sat Nov 28 13:49:46 2020 +0100
+++ b/src/HOL/SPARK/Tools/spark_commands.ML Sat Nov 28 14:25:27 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 (Resources.extensions ["vcg", "fdl", "rls"]) -- Parse.parname
+ (Resources.provide_parse_files (Command_Span.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 (Resources.extensions ["siv", "fdl", "rls"]) -- Parse.parname
+ (Resources.provide_parse_files (Command_Span.extensions ["siv", "fdl", "rls"]) -- Parse.parname
>> (Toplevel.theory o spark_open Fdl_Lexer.siv_header));
val pfun_type = Scan.option