# HG changeset patch # User wenzelm # Date 1635953012 -3600 # Node ID 376571db0eda85eef89de37aeade507b34a565a6 # Parent eae5fa0055bdd5a43a392f0ad20c07f4e61762d5# Parent 74f044c3e5908a5299287f67593f6f073ad0b993 merged; diff -r 74f044c3e590 -r 376571db0eda lib/html/library_index_content.template --- /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 @@ + + + + + diff -r 74f044c3e590 -r 376571db0eda src/HOL/SPARK/Tools/spark.scala --- 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") } diff -r 74f044c3e590 -r 376571db0eda src/Pure/Isar/keyword.ML --- 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)); diff -r 74f044c3e590 -r 376571db0eda src/Pure/Isar/toplevel.ML --- 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 = ""; +val ignoredN = ""; +val malformedN = ""; + +fun is_ignored tr = name_of tr = ignoredN; +fun is_malformed tr = name_of tr = malformedN; fun ignored pos = - empty |> name "" |> position pos |> keep (fn _ => ()); + empty |> name ignoredN |> position pos |> keep (fn _ => ()); fun malformed pos msg = - empty |> name "" |> position pos |> keep (fn _ => error msg); + empty |> name malformedN |> position pos |> keep (fn _ => error msg); (* theory transitions *) diff -r 74f044c3e590 -r 376571db0eda src/Pure/PIDE/command.ML --- 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 \cartouche\ 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; diff -r 74f044c3e590 -r 376571db0eda src/Pure/PIDE/command_span.scala --- 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 */ diff -r 74f044c3e590 -r 376571db0eda src/Pure/PIDE/markup.ML --- 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)]; diff -r 74f044c3e590 -r 376571db0eda src/Pure/PIDE/markup.scala --- 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" diff -r 74f044c3e590 -r 376571db0eda src/Pure/PIDE/protocol.ML --- 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) => diff -r 74f044c3e590 -r 376571db0eda src/Pure/PIDE/resources.ML --- 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 *) diff -r 74f044c3e590 -r 376571db0eda src/Pure/PIDE/resources.scala --- 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)))))))))) } diff -r 74f044c3e590 -r 376571db0eda src/Pure/Thy/presentation.scala --- 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 @@
- - - - - +""" + File.read(Path.explode("~~/lib/html/library_index_content.template")) + +""" """ + HTML.footer) } diff -r 74f044c3e590 -r 376571db0eda src/Pure/Thy/thy_header.ML --- 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 --