--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/html/library_index_content.template Wed Nov 03 16:23:32 2021 +0100
@@ -0,0 +1,54 @@
+ <ul>
+ <li>Higher-Order Logic</li>
+
+ <li style="list-style: none">
+ <ul>
+ <li><a href="HOL/index.html">HOL (Higher-Order Logic)</a>
+ is a version of classical higher-order logic resembling
+ that of the <a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/">HOL System</a>.
+ </li>
+ </ul>
+ </li>
+ </ul>
+
+ <ul>
+ <li>First-Order Logic</li>
+
+ <li style="list-style: none">
+ <ul>
+ <li><a href="FOL/index.html">FOL (Many-sorted First-Order Logic)</a>
+ provides basic classical and intuitionistic first-order logic. It is
+ polymorphic.
+ </li>
+
+ <li><a href="ZF/index.html">ZF (Set Theory)</a>
+ offers a formulation of Zermelo-Fraenkel set theory on top of FOL.
+ </li>
+
+ <li><a href="CCL/index.html">CCL (Classical Computational Logic)</a></li>
+
+ <li><a href="LCF/index.html">LCF (Logic of Computable Functions)</a></li>
+
+ <li><a href="FOLP/index.html">FOLP (FOL with Proof Terms)</a></li>
+ </ul>
+ </li>
+ </ul>
+
+ <ul>
+ <li>Miscellaneous</li>
+
+ <li style="list-style: none">
+ <ul>
+ <li><a href="Sequents/index.html">Sequents (first-order, modal and linear logics)</a></li>
+
+ <li><a href="CTT/index.html">CTT (Constructive Type Theory)</a>
+ is an extensional version of Martin-Löf's Type Theory.</li>
+
+ <li><a href="Cube/index.html">Cube (The Lambda Cube)</a></li>
+
+ <li><a href="Pure/index.html">The Pure logical framework</a></li>
+
+ <li><a href="Doc/index.html">Sources of Documentation</a></li>
+ </ul>
+ </li>
+ </ul>
--- a/src/HOL/SPARK/Tools/spark.scala Wed Nov 03 10:55:05 2021 +0000
+++ b/src/HOL/SPARK/Tools/spark.scala Wed Nov 03 16:23:32 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 10:55:05 2021 +0000
+++ b/src/Pure/Isar/keyword.ML Wed Nov 03 16:23:32 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/Isar/toplevel.ML Wed Nov 03 10:55:05 2021 +0000
+++ b/src/Pure/Isar/toplevel.ML Wed Nov 03 16:23:32 2021 +0100
@@ -48,6 +48,7 @@
val keep': (bool -> state -> unit) -> transition -> transition
val keep_proof: (state -> unit) -> transition -> transition
val is_ignored: transition -> bool
+ val is_malformed: transition -> bool
val ignored: Position.T -> transition
val malformed: Position.T -> string -> transition
val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
@@ -416,13 +417,17 @@
else if is_skipped_proof st then ()
else warning "No proof state");
-fun is_ignored tr = name_of tr = "<ignored>";
+val ignoredN = "<ignored>";
+val malformedN = "<malformed>";
+
+fun is_ignored tr = name_of tr = ignoredN;
+fun is_malformed tr = name_of tr = malformedN;
fun ignored pos =
- empty |> name "<ignored>" |> position pos |> keep (fn _ => ());
+ empty |> name ignoredN |> position pos |> keep (fn _ => ());
fun malformed pos msg =
- empty |> name "<malformed>" |> position pos |> keep (fn _ => error msg);
+ empty |> name malformedN |> position pos |> keep (fn _ => error msg);
(* theory transitions *)
--- a/src/Pure/PIDE/command.ML Wed Nov 03 10:55:05 2021 +0000
+++ b/src/Pure/PIDE/command.ML Wed Nov 03 16:23:32 2021 +0100
@@ -154,11 +154,16 @@
if null verbatim then ()
else legacy_feature ("Old-style {* verbatim *} token -- use \<open>cartouche\<close> instead" ^
Position.here_list verbatim);
- in
- if exists #1 token_reports
- then Toplevel.malformed (#1 (Token.core_range_of span)) "Malformed command syntax"
- else Outer_Syntax.parse_span thy init (resolve_files master_dir blobs_info span)
- end;
+
+ val core_range = Token.core_range_of span;
+ val tr =
+ if exists #1 token_reports
+ then Toplevel.malformed (#1 core_range) "Malformed command syntax"
+ else Outer_Syntax.parse_span thy init (resolve_files master_dir blobs_info span);
+ val _ =
+ if Toplevel.is_ignored tr orelse Toplevel.is_malformed tr then ()
+ else Position.report (#1 core_range) (Markup.command_span (Toplevel.name_of tr));
+ in tr end;
end;
--- a/src/Pure/PIDE/command_span.scala Wed Nov 03 10:55:05 2021 +0000
+++ b/src/Pure/PIDE/command_span.scala Wed Nov 03 16:23:32 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 10:55:05 2021 +0000
+++ b/src/Pure/PIDE/markup.ML Wed Nov 03 16:23:32 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
@@ -157,6 +158,7 @@
val descriptionN: string
val inputN: string val input: bool -> Properties.T -> T
val command_keywordN: string val command_keyword: T
+ val command_spanN: string val command_span: string -> T
val commandN: string val command_properties: T -> T
val keywordN: string val keyword_properties: T -> T
val stringN: string val string: T
@@ -476,6 +478,7 @@
(* misc entities *)
+val load_commandN = "load_command";
val bash_functionN = "bash_function";
val scala_functionN = "scala_function";
val system_optionN = "system_option";
@@ -590,6 +593,7 @@
(* outer syntax *)
val (command_keywordN, command_keyword) = markup_elem "command_keyword";
+val (command_spanN, command_span) = markup_string "command_span" nameN;
val commandN = "command"; val command_properties = properties [(kindN, commandN)];
val keywordN = "keyword"; val keyword_properties = properties [(kindN, keywordN)];
--- a/src/Pure/PIDE/markup.scala Wed Nov 03 10:55:05 2021 +0000
+++ b/src/Pure/PIDE/markup.scala Wed Nov 03 16:23:32 2021 +0100
@@ -414,6 +414,9 @@
/* outer syntax */
+ val COMMAND_SPAN = "command_span"
+ val Command_Span = new Markup_String(COMMAND_SPAN, NAME)
+
val COMMAND = "command"
val KEYWORD = "keyword"
val KEYWORD1 = "keyword1"
--- a/src/Pure/PIDE/protocol.ML Wed Nov 03 10:55:05 2021 +0000
+++ b/src/Pure/PIDE/protocol.ML Wed Nov 03 16:23:32 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 10:55:05 2021 +0000
+++ b/src/Pure/PIDE/resources.ML Wed Nov 03 16:23:32 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 10:55:05 2021 +0000
+++ b/src/Pure/PIDE/resources.scala Wed Nov 03 16:23:32 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/presentation.scala Wed Nov 03 10:55:05 2021 +0000
+++ b/src/Pure/Thy/presentation.scala Wed Nov 03 16:23:32 2021 +0100
@@ -279,60 +279,8 @@
</table>
</center>
<hr />
- <ul>
- <li>Higher-Order Logic</li>
-
- <li style="list-style: none">
- <ul>
- <li><a href="HOL/index.html">HOL (Higher-Order Logic)</a>
- is a version of classical higher-order logic resembling
- that of the <a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/">HOL System</a>.
- </li>
- </ul>
- </li>
- </ul>
-
- <ul>
- <li>First-Order Logic</li>
-
- <li style="list-style: none">
- <ul>
- <li><a href="FOL/index.html">FOL (Many-sorted First-Order Logic)</a>
- provides basic classical and intuitionistic first-order logic. It is
- polymorphic.
- </li>
-
- <li><a href="ZF/index.html">ZF (Set Theory)</a>
- offers a formulation of Zermelo-Fraenkel set theory on top of FOL.
- </li>
-
- <li><a href="CCL/index.html">CCL (Classical Computational Logic)</a></li>
-
- <li><a href="LCF/index.html">LCF (Logic of Computable Functions)</a></li>
-
- <li><a href="FOLP/index.html">FOLP (FOL with Proof Terms)</a></li>
- </ul>
- </li>
- </ul>
-
- <ul>
- <li>Miscellaneous</li>
-
- <li style="list-style: none">
- <ul>
- <li><a href="Sequents/index.html">Sequents (first-order, modal and linear logics)</a></li>
-
- <li><a href="CTT/index.html">CTT (Constructive Type Theory)</a>
- is an extensional version of Martin-Löf's Type Theory.</li>
-
- <li><a href="Cube/index.html">Cube (The Lambda Cube)</a></li>
-
- <li><a href="Pure/index.html">The Pure logical framework</a></li>
-
- <li><a href="Doc/index.html">Sources of Documentation</a></li>
- </ul>
- </li>
- </ul>
+""" + File.read(Path.explode("~~/lib/html/library_index_content.template")) +
+"""
</body>
""" + HTML.footer)
}
--- a/src/Pure/Thy/thy_header.ML Wed Nov 03 10:55:05 2021 +0000
+++ b/src/Pure/Thy/thy_header.ML Wed Nov 03 16:23:32 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 --