--- a/NEWS Fri Nov 27 21:59:23 2020 +0100
+++ b/NEWS Fri Nov 27 23:47:06 2020 +0100
@@ -272,6 +272,13 @@
"isabelle_scala_tools" and "isabelle_file_format": minor
INCOMPATIBILITY.
+* The syntax of theory load commands (for auxiliary files) is now
+specified in Isabelle/Scala, as instance of class
+isabelle.Command_Span.Load_Command registered via isabelle_scala_service
+in etc/settings. This allows more flexible schemes than just a list of
+file extensions. Minor INCOMPATIBILITY, e.g. see theory
+HOL-SPARK.SPARK_Setup to emulate the old behaviour.
+
* Isabelle server allows user-defined commands via
isabelle_scala_service.
--- a/src/HOL/SPARK/SPARK_Setup.thy Fri Nov 27 21:59:23 2020 +0100
+++ b/src/HOL/SPARK/SPARK_Setup.thy Fri Nov 27 23:47:06 2020 +0100
@@ -9,8 +9,8 @@
imports
"HOL-Library.Word"
keywords
- "spark_open_vcg" :: thy_load ("vcg", "fdl", "rls") and
- "spark_open" :: thy_load ("siv", "fdl", "rls") and
+ "spark_open_vcg" :: thy_load (spark_vcg) and
+ "spark_open" :: thy_load (spark_siv) and
"spark_proof_functions" "spark_types" "spark_end" :: thy_decl and
"spark_vc" :: thy_goal and
"spark_status" :: diag
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Tools/spark.scala Fri Nov 27 23:47:06 2020 +0100
@@ -0,0 +1,23 @@
+/* Title: HOL/SPARK/Tools/spark.scala
+ Author: Makarius
+
+Scala support for HOL-SPARK.
+*/
+
+package isabelle.spark
+
+import isabelle._
+
+
+object SPARK
+{
+ class Load_Command1 extends Command_Span.Load_Command("spark_vcg")
+ {
+ override val extensions: List[String] = List("vcg", "fdl", "rls")
+ }
+
+ class Load_Command2 extends Command_Span.Load_Command("spark_siv")
+ {
+ override val extensions: List[String] = List("siv", "fdl", "rls")
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/etc/settings Fri Nov 27 23:47:06 2020 +0100
@@ -0,0 +1,4 @@
+# -*- shell-script -*- :mode=shellscript:
+
+isabelle_scala_service 'isabelle.spark.SPARK$Load_Command1'
+isabelle_scala_service 'isabelle.spark.SPARK$Load_Command2'
--- a/src/Pure/Isar/keyword.scala Fri Nov 27 21:59:23 2020 +0100
+++ b/src/Pure/Isar/keyword.scala Fri Nov 27 23:47:06 2020 +0100
@@ -110,13 +110,13 @@
{
val none: Spec = Spec("")
}
- sealed case class Spec(kind: String, exts: List[String] = Nil, tags: List[String] = Nil)
+ sealed case class Spec(kind: String, load_command: String = "", tags: List[String] = Nil)
{
def is_none: Boolean = kind == ""
override def toString: String =
kind +
- (if (exts.isEmpty) "" else " (" + commas_quote(exts) + ")") +
+ (if (load_command.isEmpty) "" else " (" + quote(load_command) + ")") +
(if (tags.isEmpty) "" else tags.map(quote).mkString(" % ", " % ", ""))
}
@@ -127,16 +127,20 @@
class Keywords private(
val kinds: Map[String, String] = Map.empty,
- val load_commands: Map[String, List[String]] = Map.empty)
+ val load_commands: Map[String, String] = Map.empty)
{
override def toString: String =
{
val entries =
for ((name, kind) <- kinds.toList.sortBy(_._1)) yield {
- val exts = load_commands.getOrElse(name, Nil)
+ val load_decl =
+ load_commands.get(name) match {
+ case Some(load_command) => " (" + quote(load_command) + ")"
+ case None => ""
+ }
val kind_decl =
if (kind == "") ""
- else " :: " + quote(kind) + (if (exts.isEmpty) "" else " (" + commas_quote(exts) + ")")
+ else " :: " + quote(kind) + load_decl
quote(name) + kind_decl
}
entries.mkString("keywords\n ", " and\n ", "")
@@ -167,14 +171,14 @@
/* add keywords */
- def + (name: String, kind: String = "", exts: List[String] = Nil): Keywords =
+ def + (name: String, kind: String = "", load_command: String = ""): Keywords =
{
val kinds1 = kinds + (name -> kind)
val load_commands1 =
if (kind == THY_LOAD) {
if (!Symbol.iterator(name).forall(Symbol.is_ascii))
error("Bad theory load command " + quote(name))
- load_commands + (name -> exts)
+ load_commands + (name -> load_command)
}
else load_commands
new Keywords(kinds1, load_commands1)
@@ -187,8 +191,8 @@
keywords + Symbol.decode(name) + Symbol.encode(name)
else
keywords +
- (Symbol.decode(name), spec.kind, spec.exts) +
- (Symbol.encode(name), spec.kind, spec.exts)
+ (Symbol.decode(name), spec.kind, spec.load_command) +
+ (Symbol.encode(name), spec.kind, spec.load_command)
}
--- a/src/Pure/Isar/outer_syntax.scala Fri Nov 27 21:59:23 2020 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Fri Nov 27 23:47:06 2020 +0100
@@ -56,16 +56,16 @@
/* keywords */
- def + (name: String, kind: String = "", exts: List[String] = Nil): Outer_Syntax =
+ def + (name: String, kind: String = "", load_command: String = ""): Outer_Syntax =
new Outer_Syntax(
- keywords + (name, kind, exts), rev_abbrevs, language_context, has_tokens = true)
+ keywords + (name, kind, load_command), rev_abbrevs, language_context, has_tokens = true)
def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
(this /: keywords) {
case (syntax, (name, spec)) =>
syntax +
- (Symbol.decode(name), spec.kind, spec.exts) +
- (Symbol.encode(name), spec.kind, spec.exts)
+ (Symbol.decode(name), spec.kind, spec.load_command) +
+ (Symbol.encode(name), spec.kind, spec.load_command)
}
@@ -133,7 +133,7 @@
/* load commands */
- def load_command(name: String): Option[List[String]] =
+ def load_command(name: String): Option[String] =
keywords.load_commands.get(name)
def has_load_commands(text: String): Boolean =
--- a/src/Pure/PIDE/command.scala Fri Nov 27 21:59:23 2020 +0100
+++ b/src/Pure/PIDE/command.scala Fri Nov 27 23:47:06 2020 +0100
@@ -415,26 +415,30 @@
// inlined errors
case Thy_Header.THEORY =>
val reader = Scan.char_reader(Token.implode(span.content))
- val imports_pos = resources.check_thy_reader(node_name, reader).imports_pos
+ val header = resources.check_thy_reader(node_name, reader)
+ val imports_pos = header.imports_pos
val raw_imports =
try {
val read_imports = Thy_Header.read(reader, Token.Pos.none).imports
if (imports_pos.length == read_imports.length) read_imports else error("")
}
- catch { case exn: Throwable => List.fill(imports_pos.length)("") }
+ catch { case _: Throwable => List.fill(imports_pos.length)("") }
- val errors =
+ val errs1 =
for { ((import_name, pos), s) <- imports_pos zip raw_imports if !can_import(import_name) }
yield {
val completion =
if (Thy_Header.is_base_name(s)) resources.complete_import_name(node_name, s) else Nil
- val msg =
- "Bad theory import " +
- Markup.Path(import_name.node).markup(quote(import_name.toString)) +
- Position.here(pos) + Completion.report_theories(pos, completion)
- Exn.Exn[Command.Blob](ERROR(msg))
+ "Bad theory import " +
+ Markup.Path(import_name.node).markup(quote(import_name.toString)) +
+ Position.here(pos) + Completion.report_theories(pos, completion)
}
- (errors, -1)
+ val errs2 =
+ for {
+ (_, spec) <- header.keywords
+ if !Command_Span.load_commands.exists(_.name == spec.load_command)
+ } yield { "Unknown load command specification: " + quote(spec.load_command) }
+ ((errs1 ::: errs2).map(msg => Exn.Exn[Command.Blob](ERROR(msg))), -1)
// auxiliary files
case _ =>
--- a/src/Pure/PIDE/command_span.scala Fri Nov 27 21:59:23 2020 +0100
+++ b/src/Pure/PIDE/command_span.scala Fri Nov 27 23:47:06 2020 +0100
@@ -18,13 +18,25 @@
val no_loaded_files: Loaded_Files = (Nil, -1)
- def loaded_files(exts: List[String], tokens: List[(Token, Int)]): Loaded_Files =
- tokens.collectFirst({ case (t, i) if t.is_embedded => (t.content, i) }) match {
- case Some((file, i)) =>
- if (exts.isEmpty) (List(file), i)
- else (exts.map(ext => file + "." + ext), i)
- case None => no_loaded_files
- }
+ class Load_Command(val name: String) extends Isabelle_System.Service
+ {
+ override def toString: String = name
+
+ def extensions: List[String] = Nil
+
+ def loaded_files(tokens: List[(Token, Int)]): Loaded_Files =
+ tokens.collectFirst({ case (t, i) if t.is_embedded => (t.content, i) }) match {
+ case Some((file, i)) =>
+ extensions match {
+ case Nil => (List(file), i)
+ case exts => (exts.map(ext => file + "." + ext), i)
+ }
+ case None => no_loaded_files
+ }
+ }
+
+ lazy val load_commands: List[Load_Command] =
+ new Load_Command("") :: Isabelle_System.make_services(classOf[Load_Command])
/* span kind */
@@ -107,8 +119,12 @@
def loaded_files(syntax: Outer_Syntax): Loaded_Files =
syntax.load_command(name) match {
- case Some(exts) => isabelle.Command_Span.loaded_files(exts, clean_arguments)
case None => no_loaded_files
+ case Some(a) =>
+ load_commands.find(_.name == a) match {
+ case Some(load_command) => load_command.loaded_files(clean_arguments)
+ case None => error("Undefined load command function: " + a)
+ }
}
}
--- a/src/Pure/Thy/thy_header.scala Fri Nov 27 21:59:23 2020 +0100
+++ b/src/Pure/Thy/thy_header.scala Fri Nov 27 23:47:06 2020 +0100
@@ -7,8 +7,6 @@
package isabelle
-import scala.annotation.tailrec
-import scala.collection.mutable
import scala.util.parsing.input.Reader
import scala.util.matching.Regex
@@ -131,13 +129,15 @@
{
val header: Parser[Thy_Header] =
{
- val loaded_files =
- $$$("(") ~! (rep1sep(name, $$$(",")) <~ $$$(")")) ^^ { case _ ~ x => x } |
- success(Nil)
+ def load_command =
+ ($$$("(") ~! (name <~ $$$(")")) ^^ { case _ ~ x => x }) | success("")
+
+ def load_command_spec(kind: String) =
+ (if (kind == Keyword.THY_LOAD) load_command else success("")) ^^ (x => (kind, x))
val keyword_spec =
- atom("outer syntax keyword specification", _.is_name) ~ loaded_files ~ tags ^^
- { case x ~ y ~ z => Keyword.Spec(x, y, z) }
+ (atom("outer syntax keyword specification", _.is_name) >> load_command_spec) ~ tags ^^
+ { case (x, y) ~ z => Keyword.Spec(x, y, z) }
val keyword_decl =
rep1(string) ~
@@ -166,7 +166,7 @@
Thy_Header((f(name), pos),
imports.map({ case (a, b) => (f(a), b) }),
keywords.map({ case (a, Keyword.Spec(b, c, d)) =>
- (f(a), Keyword.Spec(f(b), c.map(f), d.map(f))) }),
+ (f(a), Keyword.Spec(f(b), f(c), d.map(f))) }),
abbrevs.map({ case (a, b) => (f(a), f(b)) }))
}
--- a/src/Pure/Tools/scala_project.scala Fri Nov 27 21:59:23 2020 +0100
+++ b/src/Pure/Tools/scala_project.scala Fri Nov 27 23:47:06 2020 +0100
@@ -58,6 +58,7 @@
"src/Tools/VSCode/" -> Path.explode("isabelle.vscode"),
"src/Tools/jEdit/src-base/" -> Path.explode("isabelle.jedit_base"),
"src/Tools/jEdit/src/" -> Path.explode("isabelle.jedit"),
+ "src/HOL/SPARK/Tools" -> Path.explode("isabelle.spark"),
"src/HOL/Tools/Nitpick" -> Path.explode("isabelle.nitpick"))
--- a/src/Pure/build-jars Fri Nov 27 21:59:23 2020 +0100
+++ b/src/Pure/build-jars Fri Nov 27 23:47:06 2020 +0100
@@ -9,6 +9,7 @@
## sources
declare -a SOURCES=(
+ src/HOL/SPARK/Tools/spark.scala
src/HOL/Tools/Nitpick/kodkod.scala
src/Pure/Admin/afp.scala
src/Pure/Admin/build_csdp.scala