1.1 --- a/src/HOL/SPARK/Tools/spark_commands.ML	Fri Mar 12 12:48:55 2021 +0100
     1.2 +++ b/src/HOL/SPARK/Tools/spark_commands.ML	Fri Mar 12 13:25:51 2021 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  Isar commands for handling SPARK/Ada verification conditions.
     1.5  *)
     1.6  
     1.7 -structure SPARK_Commands: sig end =
     1.8 +structure SPARK_Commands(** ): sig end( *make funs visible for tests *) =
     1.9  struct
    1.10  
    1.11  fun spark_open header (files, prfx) thy =

     2.1 --- a/test/Pure/Isar/Check_Outer_Syntax.thy	Fri Mar 12 12:48:55 2021 +0100
     2.2 +++ b/test/Pure/Isar/Check_Outer_Syntax.thy	Fri Mar 12 13:25:51 2021 +0100
     2.3 @@ -379,7 +379,8 @@
     2.4      "open a new SPARK environment and load a SPARK-generated .vcg file"*)
     2.5  (*  /============================================================ 3rd arg of Outer_Syntax.command*)
     2.6      (
     2.7 -        Resources.provide_parse_files "spark_open" -- Parse.parname
     2.8 +        Resources.provide_parse_files (Command_Span.extensions ["vcg", "fdl", "rls"])
     2.9 +          -- Parse.parname
    2.10        >>
    2.11          (Toplevel.theory o spark_open (*Fdl_Lexer.*)siv_header)
    2.12      );
    2.13 @@ -388,21 +389,23 @@
    2.14    (Toplevel.transition -> Toplevel.transition) parser -> unit
    2.15  (*\--------------- 3rd arg of .command -------------/*)
    2.16  \<close> ML \<open>
    2.17 -(Resources.provide_parse_files "spark_open" -- Parse.parname
    2.18 - >> (Toplevel.theory o spark_open (*Fdl_Lexer.*)siv_header)
    2.19 -)     : Token.T list -> (Toplevel.transition -> Toplevel.transition) * Token.T list
    2.20 +(        Resources.provide_parse_files (Command_Span.extensions ["vcg", "fdl", "rls"])
    2.21 +          -- Parse.parname
    2.22 +      >> (Toplevel.theory o spark_open (*Fdl_Lexer.*)siv_header)
    2.23 +)          : Token.T list -> (Toplevel.transition -> Toplevel.transition) * Token.T list
    2.24  \<close> ML \<open>
    2.25  \<close> ML \<open> (* decompose 3rd arg of Outer_Syntax.command with respect to >> *)
    2.26  op >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
    2.27  (*      \---1st arg---/   \---2nd--/    \---result--/ *)
    2.28  
    2.29  \<close> ML \<open> (*================= 1st arg of >> instantiates types..*)
    2.30 -val xxx = Resources.provide_parse_files "spark_open" -- Parse.parname
    2.31 +val xxx = Resources.provide_parse_files (Command_Span.extensions ["vcg", "fdl", "rls"])
    2.32 +          -- Parse.parname
    2.33     :                 ((theory -> Token.file list * theory) * string) parser;
    2.34  xxx: Token.T list -> ((theory -> Token.file list * theory) * string) * Token.T list;
    2.35  (*                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
    2.36  \<close> ML \<open>
    2.37 -Resources.provide_parse_files "spark_open":
    2.38 +Resources.provide_parse_files (Command_Span.extensions ["vcg", "fdl", "rls"]):
    2.39                        (theory -> Token.file list * theory) parser;
    2.40  (*                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^           *)
    2.41  Parse.parname:       (                                       string) parser;
    2.42 @@ -481,7 +484,8 @@
    2.43  (* input from Isabelle/jEdit -----------------------------------------------------------^^^^^^^^^^^^                                                   [] iff successful *)
    2.44  \<close> ML \<open>
    2.45  \<close> ML \<open> (* and now we show how the third argument of Outer_Syntax.command is constructed and start from *1* above *)
    2.46 -Resources.provide_parse_files "spark_open" -- Parse.parname                   (*..1st arg of >>*)
    2.47 +     Resources.provide_parse_files (Command_Span.extensions ["vcg", "fdl", "rls"])  
    2.48 +       -- Parse.parname                                                       (*..1st arg of >>*)
    2.49    >> (Toplevel.theory o spark_open (*Fdl_Lexer.*)siv_header) :                (*..2nd arg of >>*)
    2.50  (*^^ result..*) Token.T list -> (Toplevel.transition -> Toplevel.transition) * Token.T list;
    2.51  \<close> ML \<open>
    2.52 @@ -493,7 +497,7 @@
    2.53  (*^^ result..*) Token.T list -> (Toplevel.transition -> Toplevel.transition) * Token.T list (*..                 'a -> 'd * 'c *);
    2.54  \<close> ML \<open>
    2.55  \<close> ML \<open>
    2.56 -Resources.provide_parse_files "spark_open" -- Parse.parname:                  (*..1st arg of >>*)
    2.57 +Resources.provide_parse_files (Command_Span.extensions ["vcg", "fdl", "rls"]) -- Parse.parname: (*..1st arg of >>*)
    2.58      (Token.T list -> ((theory -> Token.file list * theory) * string) * Token.T list)
    2.59  (*                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
    2.60  \<close> ML \<open> (* provide_parse_files..  ~~~~~~~~~~~~~~~~~~~~~~~~,   ~~~~~~--- ..Parse.parname *)
    2.61 @@ -611,4 +615,4 @@
    2.62  \<close> ML \<open>
    2.63  \<close>
    2.64  
    2.65 -end
    2.66 \ No newline at end of file
    2.67 +end