--- a/src/HOL/SPARK/Tools/spark.scala Wed Nov 03 12:04:22 2021 +0100
+++ b/src/HOL/SPARK/Tools/spark.scala Wed Nov 03 14:26:13 2021 +0100
@@ -11,12 +11,12 @@
object SPARK
{
- class Load_Command1 extends Command_Span.Load_Command("spark_vcg")
+ class Load_Command1 extends Command_Span.Load_Command("spark_vcg", Scala_Project.here)
{
override val extensions: List[String] = List("vcg", "fdl", "rls")
}
- class Load_Command2 extends Command_Span.Load_Command("spark_siv")
+ class Load_Command2 extends Command_Span.Load_Command("spark_siv", Scala_Project.here)
{
override val extensions: List[String] = List("siv", "fdl", "rls")
}
--- a/src/Pure/Isar/keyword.ML Wed Nov 03 12:04:22 2021 +0100
+++ b/src/Pure/Isar/keyword.ML Wed Nov 03 14:26:13 2021 +0100
@@ -38,7 +38,8 @@
val prf_script_asm_goal: string
val before_command: string
val quasi_command: string
- type spec = string * string list
+ type spec = {kind: string, load_command: string * Position.T, tags: string list}
+ val command_spec: string * string list -> spec
val no_spec: spec
val before_command_spec: spec
val quasi_command_spec: spec
@@ -133,13 +134,16 @@
(* specifications *)
-type spec = string * string list;
+type spec = {kind: string, load_command: string * Position.T, tags: string list};
+
+fun command_spec (kind, tags) : spec =
+ {kind = kind, load_command = ("", Position.none), tags = tags};
-val no_spec: spec = ("", []);
-val before_command_spec: spec = (before_command, []);
-val quasi_command_spec: spec = (quasi_command, []);
-val document_heading_spec: spec = ("document_heading", ["document"]);
-val document_body_spec: spec = ("document_body", ["document"]);
+val no_spec = command_spec ("", []);
+val before_command_spec = command_spec (before_command, []);
+val quasi_command_spec = command_spec (quasi_command, []);
+val document_heading_spec = command_spec ("document_heading", ["document"]);
+val document_body_spec = command_spec ("document_body", ["document"]);
type entry =
{pos: Position.T,
@@ -147,7 +151,7 @@
kind: string,
tags: string list};
-fun check_spec pos (kind, tags) : entry =
+fun check_spec pos ({kind, tags, ...}: spec) : entry =
if not (member (op =) command_kinds kind) then
error ("Unknown outer syntax keyword kind " ^ quote kind)
else {pos = pos, id = serial (), kind = kind, tags = tags};
@@ -186,7 +190,7 @@
Symtab.merge (K true) (commands1, commands2));
val add_keywords =
- fold (fn ((name, pos), spec as (kind, _)) => map_keywords (fn (minor, major, commands) =>
+ fold (fn ((name, pos), spec as {kind, ...}: spec) => map_keywords (fn (minor, major, commands) =>
if kind = "" orelse kind = before_command orelse kind = quasi_command then
let
val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
@@ -202,7 +206,7 @@
add_keywords o map (fn name => ((name, Position.none), no_spec));
val add_major_keywords =
- add_keywords o map (fn name => ((name, Position.none), (diag, [])));
+ add_keywords o map (fn name => ((name, Position.none), command_spec (diag, [])));
val no_major_keywords =
map_keywords (fn (minor, _, _) => (minor, Scan.empty_lexicon, Symtab.empty));
--- a/src/Pure/PIDE/command_span.scala Wed Nov 03 12:04:22 2021 +0100
+++ b/src/Pure/PIDE/command_span.scala Wed Nov 03 14:26:13 2021 +0100
@@ -21,10 +21,13 @@
}
sealed case class Loaded_Files(files: List[String], index: Int)
- class Load_Command(val name: String) extends Isabelle_System.Service
+ abstract class Load_Command(val name: String, val here: Scala_Project.Here)
+ extends Isabelle_System.Service
{
override def toString: String = name
+ def position: Position.T = here.position
+
def extensions: List[String] = Nil
def loaded_files(tokens: List[(Token, Int)]): Loaded_Files =
@@ -38,8 +41,10 @@
}
}
+ object Load_Command_Default extends Load_Command("", Scala_Project.here)
+
lazy val load_commands: List[Load_Command] =
- new Load_Command("") :: Isabelle_System.make_services(classOf[Load_Command])
+ Load_Command_Default :: Isabelle_System.make_services(classOf[Load_Command])
/* span kind */
--- a/src/Pure/PIDE/markup.ML Wed Nov 03 12:04:22 2021 +0100
+++ b/src/Pure/PIDE/markup.ML Wed Nov 03 14:26:13 2021 +0100
@@ -85,6 +85,7 @@
val wordsN: string val words: T
val hiddenN: string val hidden: T
val deleteN: string val delete: T
+ val load_commandN: string
val bash_functionN: string
val scala_functionN: string
val system_optionN: string
@@ -476,6 +477,7 @@
(* misc entities *)
+val load_commandN = "load_command";
val bash_functionN = "bash_function";
val scala_functionN = "scala_function";
val system_optionN = "system_option";
--- a/src/Pure/PIDE/protocol.ML Wed Nov 03 12:04:22 2021 +0100
+++ b/src/Pure/PIDE/protocol.ML Wed Nov 03 14:26:13 2021 +0100
@@ -120,7 +120,8 @@
(pair (list (pair string (pair string (list string))))
(list YXML.string_of_body)))) a;
val imports' = map (rpair Position.none) imports;
- val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords;
+ val keywords' =
+ map (fn (x, y) => ((x, Position.none), Keyword.command_spec y)) keywords;
val header = Thy_Header.make (name, Position.none) imports' keywords';
in Document.Deps {master = master, header = header, errors = errors} end,
fn (a :: b, c) =>
--- a/src/Pure/PIDE/resources.ML Wed Nov 03 12:04:22 2021 +0100
+++ b/src/Pure/PIDE/resources.ML Wed Nov 03 14:26:13 2021 +0100
@@ -13,6 +13,7 @@
session_chapters: (string * string) list,
bibtex_entries: (string * string list) list,
command_timings: Properties.T list,
+ load_commands: (string * Position.T) list,
scala_functions: (string * (bool * Position.T)) list,
global_theories: (string * string) list,
loaded_theories: string list} -> unit
@@ -24,6 +25,7 @@
val check_session: Proof.context -> string * Position.T -> string
val session_chapter: string -> string
val last_timing: Toplevel.transition -> Time.time
+ val check_load_command: Proof.context -> string * Position.T -> string
val scala_functions: unit -> string list
val check_scala_function: Proof.context -> string * Position.T -> string * bool
val master_directory: theory -> Path.T
@@ -104,6 +106,7 @@
session_chapters = Symtab.empty: string Symtab.table,
bibtex_entries = Symtab.empty: string list Symtab.table,
timings = empty_timings,
+ load_commands = []: (string * Position.T) list,
scala_functions = Symtab.empty: (bool * Position.T) Symtab.table},
{global_theories = Symtab.empty: string Symtab.table,
loaded_theories = Symtab.empty: unit Symtab.table});
@@ -113,7 +116,7 @@
fun init_session
{session_positions, session_directories, session_chapters, bibtex_entries,
- command_timings, scala_functions, global_theories, loaded_theories} =
+ command_timings, load_commands, scala_functions, global_theories, loaded_theories} =
Synchronized.change global_session_base
(fn _ =>
({session_positions = sort_by #1 (map (apsnd make_entry) session_positions),
@@ -123,6 +126,7 @@
session_chapters = Symtab.make session_chapters,
bibtex_entries = Symtab.make bibtex_entries,
timings = make_timings command_timings,
+ load_commands = load_commands,
scala_functions = Symtab.make scala_functions},
{global_theories = Symtab.make global_theories,
loaded_theories = Symtab.make_set loaded_theories}));
@@ -130,14 +134,15 @@
fun init_session_yxml yxml =
let
val (session_positions, (session_directories, (session_chapters, (bibtex_entries,
- (command_timings, (scala_functions, (global_theories, loaded_theories))))))) =
+ (command_timings, (load_commands, (scala_functions, (global_theories, loaded_theories)))))))) =
YXML.parse_body yxml |>
let open XML.Decode in
(pair (list (pair string properties))
(pair (list (pair string string)) (pair (list (pair string string))
(pair (list (pair string (list string))) (pair (list properties)
- (pair (list (pair string (pair bool properties)))
- (pair (list (pair string string)) (list string))))))))
+ (pair (list (pair string properties))
+ (pair (list (pair string (pair bool properties)))
+ (pair (list (pair string string)) (list string)))))))))
end;
in
init_session
@@ -146,6 +151,7 @@
session_chapters = session_chapters,
bibtex_entries = bibtex_entries,
command_timings = command_timings,
+ load_commands = (map o apsnd) Position.of_properties load_commands,
scala_functions = (map o apsnd o apsnd) Position.of_properties scala_functions,
global_theories = global_theories,
loaded_theories = loaded_theories}
@@ -176,6 +182,9 @@
fun last_timing tr = get_timings (get_session_base1 #timings) tr;
+fun check_load_command ctxt arg =
+ Completion.check_entity Markup.load_commandN (get_session_base1 #load_commands) ctxt arg;
+
(* Scala functions *)
@@ -238,9 +247,14 @@
val imports_of = #imports o Files.get;
fun begin_theory master_dir {name, imports, keywords} parents =
- Theory.begin_theory name parents
- |> map_files (fn _ => (Path.explode (Path.implode_symbolic master_dir), imports, []))
- |> Thy_Header.add_keywords keywords;
+ let
+ val thy =
+ Theory.begin_theory name parents
+ |> map_files (fn _ => (Path.explode (Path.implode_symbolic master_dir), imports, []))
+ |> Thy_Header.add_keywords keywords;
+ val ctxt = Proof_Context.init_global thy;
+ val _ = List.app (ignore o check_load_command ctxt o #load_command o #2) keywords;
+ in thy end;
(* theory files *)
--- a/src/Pure/PIDE/resources.scala Wed Nov 03 12:04:22 2021 +0100
+++ b/src/Pure/PIDE/resources.scala Wed Nov 03 14:26:13 2021 +0100
@@ -39,16 +39,18 @@
pair(list(pair(string, string)),
pair(list(pair(string, list(string))),
pair(list(properties),
+ pair(list(pair(string, properties)),
pair(list(pair(string, pair(bool, properties))),
- pair(list(pair(string, string)), list(string))))))))(
+ pair(list(pair(string, string)), list(string)))))))))(
(sessions_structure.session_positions,
(sessions_structure.dest_session_directories,
(sessions_structure.session_chapters,
(sessions_structure.bibtex_entries,
(command_timings,
+ (Command_Span.load_commands.map(cmd => (cmd.name, cmd.position)),
(Scala.functions.map(fun => (fun.name, (fun.multi, fun.position))),
(session_base.global_theories.toList,
- session_base.loaded_theories.keys)))))))))
+ session_base.loaded_theories.keys))))))))))
}
--- a/src/Pure/Thy/thy_header.ML Wed Nov 03 12:04:22 2021 +0100
+++ b/src/Pure/Thy/thy_header.ML Wed Nov 03 14:26:13 2021 +0100
@@ -85,9 +85,9 @@
((subparagraphN, \<^here>), Keyword.document_heading_spec),
((textN, \<^here>), Keyword.document_body_spec),
((txtN, \<^here>), Keyword.document_body_spec),
- ((text_rawN, \<^here>), (Keyword.document_raw, ["document"])),
- ((theoryN, \<^here>), (Keyword.thy_begin, ["theory"])),
- (("ML", \<^here>), (Keyword.thy_decl, ["ML"]))];
+ ((text_rawN, \<^here>), Keyword.command_spec (Keyword.document_raw, ["document"])),
+ ((theoryN, \<^here>), Keyword.command_spec (Keyword.thy_begin, ["theory"])),
+ (("ML", \<^here>), Keyword.command_spec (Keyword.thy_decl, ["ML"]))];
(* theory data *)
@@ -132,11 +132,13 @@
else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 Parse.theory_name);
val load_command =
- Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
+ Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.position Parse.name) --| Parse.$$$ ")")
+ ("", Position.none);
val keyword_spec =
Parse.group (fn () => "outer syntax keyword specification")
- ((Parse.name --| load_command) -- Document_Source.old_tags);
+ ((Parse.name -- load_command) -- Document_Source.old_tags) >>
+ (fn ((a, b), c) => {kind = a, load_command = b, tags = c});
val keyword_decl =
Scan.repeat1 Parse.string_position --