1.1 --- a/src/Pure/Tools/scala_project.scala	Fri Mar 12 13:25:51 2021 +0100
     1.2 +++ b/src/Pure/Tools/scala_project.scala	Fri Mar 12 15:22:39 2021 +0100
     1.3 @@ -74,6 +74,7 @@
     1.4        "src/Tools/jEdit/src-base/" -> Path.explode("isabelle.jedit_base"),
     1.5        "src/Tools/jEdit/src/" -> Path.explode("isabelle.jedit"),
     1.6        "src/HOL/SPARK/Tools" -> Path.explode("isabelle.spark"),
     1.7 +      "src/Tools/isac/etc" -> Path.explode("isabelle.isac"),
     1.8        "src/HOL/Tools/Nitpick" -> Path.explode("isabelle.nitpick"))
     1.9  
    1.10  

     2.1 --- a/src/Pure/build-jars	Fri Mar 12 13:25:51 2021 +0100
     2.2 +++ b/src/Pure/build-jars	Fri Mar 12 15:22:39 2021 +0100
     2.3 @@ -10,6 +10,7 @@
     2.4  
     2.5  declare -a SOURCES=(
     2.6    src/HOL/SPARK/Tools/spark.scala
     2.7 +  src/Tools/isac/etc/isac.scala
     2.8    src/HOL/Tools/Nitpick/kodkod.scala
     2.9    src/Pure/Admin/afp.scala
    2.10    src/Pure/Admin/build_csdp.scala

     3.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy	Fri Mar 12 13:25:51 2021 +0100
     3.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy	Fri Mar 12 15:22:39 2021 +0100
     3.3 @@ -11,7 +11,8 @@
     3.4  (** )"~~/src/Tools/isac/MathEngine/MathEngine"  ( *activate after devel.of BridgeJEdit*)
     3.5  (**) "HOL-SPARK.SPARK"                             (*remove after devel.of BridgeJEdit*)
     3.6  keywords
     3.7 -(** )"Example" :: thy_load (**) (isac_example) (** ) "spark_vc" :: thy_goal *)
     3.8 +(*WAS "Example" :: thy_load ("str")  ..in Isabelle2020*)
     3.9 +(** ) "Example" :: thy_load (isac_example) (*Unknown load command specification: "isac_example"*)
    3.10    and( **)"Problem" :: thy_decl (* root-problem + recursively in Solution;
    3.11                                 "spark_vc" :: thy_goal *)
    3.12    and "Specification" "Model" "References" :: diag
    3.13 @@ -122,7 +123,7 @@
    3.14  (** )
    3.15  val _ =                                                  
    3.16    Outer_Syntax.command \<^command_keyword>\<open>Example\<close> "start a Calculation from a Formalise-file"
    3.17 -    (Resources.provide_parse_files "Example" -- Parse.parname
    3.18 +    (Resources.provide_parse_files (Command_Span.extensions ["str"]) -- Parse.parname
    3.19        >> (Toplevel.theory o           (*vvvvvvvvvvvvvvvvvvvv--- HACK makes test independent from session Isac*)
    3.20          (Preliminary.load_formalisation @{theory Biegelinie} ParseC.formalisation)) );
    3.21  ( **)

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/isac/BridgeJEdit/isac.scala	Fri Mar 12 15:22:39 2021 +0100
     4.3 @@ -0,0 +1,18 @@
     4.4 +/*  Title:      src/Tools/isac/BridgeJEdit/isac.scala <-- HOL/SPARK/Tools/spark.scala
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Scala support for Isac.
     4.8 +*/
     4.9 +
    4.10 +package isabelle.isac
    4.11 +
    4.12 +import isabelle._
    4.13 +
    4.14 +
    4.15 +object ISAC
    4.16 +{
    4.17 +  class Load_Command1 extends Command_Span.Load_Command("isac_example")
    4.18 +  {
    4.19 +    override val extensions: List[String] = List("str")
    4.20 +  }
    4.21 +}