# HG changeset patch
# User wenzelm
# Date 1606517226 -3600
# Node ID 04d5f6d769a7cd9299c0f62c28f70f9a0701b529
# Parent  5f9d661550811c2bba111626685ce6de1809dcd3
more flexible syntax for theory load commands via Isabelle/Scala;

diff -r 5f9d66155081 -r 04d5f6d769a7 NEWS
--- 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.
 
diff -r 5f9d66155081 -r 04d5f6d769a7 src/HOL/SPARK/SPARK_Setup.thy
--- 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
diff -r 5f9d66155081 -r 04d5f6d769a7 src/HOL/SPARK/Tools/spark.scala
--- /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")
+  }
+}
diff -r 5f9d66155081 -r 04d5f6d769a7 src/HOL/SPARK/etc/settings
--- /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'
diff -r 5f9d66155081 -r 04d5f6d769a7 src/Pure/Isar/keyword.scala
--- 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)
       }
 
 
diff -r 5f9d66155081 -r 04d5f6d769a7 src/Pure/Isar/outer_syntax.scala
--- 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 =
diff -r 5f9d66155081 -r 04d5f6d769a7 src/Pure/PIDE/command.scala
--- 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 _ =>
diff -r 5f9d66155081 -r 04d5f6d769a7 src/Pure/PIDE/command_span.scala
--- 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)
+          }
       }
   }
 
diff -r 5f9d66155081 -r 04d5f6d769a7 src/Pure/Thy/thy_header.scala
--- 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)) }))
         }
 
diff -r 5f9d66155081 -r 04d5f6d769a7 src/Pure/Tools/scala_project.scala
--- 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"))
 
 
diff -r 5f9d66155081 -r 04d5f6d769a7 src/Pure/build-jars
--- 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