1.1 --- a/src/Tools/isac/BaseDefinitions/theoryC.sml	Sat Apr 03 15:27:52 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/theoryC.sml	Sun Apr 04 12:29:42 2021 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4    val cut_id: string -> id
     1.5  
     1.6    val last_isabelle_thy: theory
     1.7 +  val session_specify_names: id list
     1.8    val session_interpret_names: id list
     1.9    val get_theory: id -> theory         (* restricted to Isac_Knowledge *)
    1.10    val id_to_ctxt: id -> Proof.context
    1.11 @@ -36,11 +37,14 @@
    1.12  fun cut_id dn = hd (space_explode "." dn);
    1.13  
    1.14  val last_isabelle_thy = @{theory Complex_Main}
    1.15 -val session_interpret_names = ["Interpret", "Specify", "MathEngBasic", "Input_Descript",
    1.16 +val session_specify_names = ["Specify", "MathEngBasic", "Input_Descript",
    1.17    "ProgLang", "Auto_Prog", "Prog_Expr", "Tactical", "Prog_Tac", "Program", "ListC", "Calculate",
    1.18    "BaseDefinitions", "Know_Store"]
    1.19 +val session_interpret_names = ["Interpret"]
    1.20  fun get_thy thyID =
    1.21 -  if member op = session_interpret_names thyID
    1.22 +  if member op = session_specify_names thyID
    1.23 +  then Thy_Info.get_theory ("Specify." ^ thyID)
    1.24 +  else if member op = session_interpret_names thyID
    1.25    then Thy_Info.get_theory ("Interpret." ^ thyID)
    1.26    else Thy_Info.get_theory ("Isac." ^ thyID);
    1.27  fun get_theory thy =   

     2.1 --- a/src/Tools/isac/Interpret/Interpret.thy	Sat Apr 03 15:27:52 2021 +0200
     2.2 +++ b/src/Tools/isac/Interpret/Interpret.thy	Sun Apr 04 12:29:42 2021 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  *)
     2.5  
     2.6  theory Interpret
     2.7 -imports "~~/src/Tools/isac/Specify/Specify"
     2.8 +imports Specify.Specify
     2.9  begin
    2.10  (* removed all warnings here, only "handle _" remains *)
    2.11    ML_file istate.sml
    2.12 @@ -21,13 +21,15 @@
    2.13  
    2.14  ML \<open>
    2.15  local
    2.16 -  val all_thys = @{theory} :: Theory.ancestors_of @{theory}
    2.17 -  val session_interpret_names = map Context.theory_name 
    2.18 -    (take ((find_index (curry Context.eq_thy ThyC.last_isabelle_thy) all_thys), all_thys))
    2.19 +  val thys_known_sofar = @{theory} :: Theory.ancestors_of @{theory}
    2.20 +  val isac_thys_known_sofar = take (
    2.21 +    find_index (curry Context.eq_thy ThyC.last_isabelle_thy) thys_known_sofar,
    2.22 +    thys_known_sofar)
    2.23 +  val isac_names_known_sofar = map Context.theory_name isac_thys_known_sofar
    2.24  in
    2.25 -  val check_interpret_thys =
    2.26 -    if session_interpret_names = ThyC.session_interpret_names then ()
    2.27 -    else raise ERROR "determine ThyC.session_interpret_names from HERE"
    2.28 +  val compare_dependencies__ThyC =
    2.29 +    if isac_names_known_sofar = ThyC.session_interpret_names @ ThyC.session_specify_names then ()
    2.30 +    else raise ERROR "theory dependencies not as anticipated in ThyC"
    2.31  end
    2.32  \<close> ML \<open>
    2.33  \<close> ML \<open>

     3.1 --- a/src/Tools/isac/Knowledge/Test_Build_Thydata.thy	Sat Apr 03 15:27:52 2021 +0200
     3.2 +++ b/src/Tools/isac/Knowledge/Test_Build_Thydata.thy	Sun Apr 04 12:29:42 2021 +0200
     3.3 @@ -1,7 +1,7 @@
     3.4  (* Minimal Thydata for test/../thy-hierarchy *)
     3.5  
     3.6  theory Test_Build_Thydata
     3.7 -  imports "Interpret.ProgLang"
     3.8 +  imports "Specify.ProgLang"
     3.9  begin
    3.10  
    3.11  ML \<open>

     4.1 --- a/src/Tools/isac/ROOT	Sat Apr 03 15:27:52 2021 +0200
     4.2 +++ b/src/Tools/isac/ROOT	Sun Apr 04 12:29:42 2021 +0200
     4.3 @@ -11,22 +11,29 @@
     4.4  # file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf
     4.5  *)
     4.6  
     4.7 -(* run "./bin/isabelle build -v -b Interpret" *)
     4.8 -session Interpret in Interpret = "HOL-SPARK" +
     4.9 +(* run "./bin/isabelle build -v -b Specify" *)
    4.10 +session Specify in Specify = "HOL-SPARK" +
    4.11    description "
    4.12 -    Session covering code required for ~~/src/Tools/isac/Doc.
    4.13 +    Session covering code required for ~~/src/Tools/isac/Doc/Specify_Phase
    4.14    "
    4.15    options [document = false (** ), browser_info = true( **)]
    4.16    directories
    4.17      "../BaseDefinitions"
    4.18      "../ProgLang"
    4.19      "../MathEngBasic"
    4.20 -    "../Specify"
    4.21    theories
    4.22      "../BaseDefinitions/BaseDefinitions"
    4.23      "../ProgLang/ProgLang"
    4.24      "../MathEngBasic/MathEngBasic"
    4.25 -    "../Specify/Specify"
    4.26 +    "Specify"
    4.27 +
    4.28 +(* run "./bin/isabelle build -v -b Interpret" *)
    4.29 +session Interpret in Interpret = Specify +
    4.30 +  description "
    4.31 +    Session covering code required for ~~/src/Tools/isac/Doc/Lucas_Interpreter
    4.32 +  "
    4.33 +  options [document = false (** ), browser_info = true( **)]
    4.34 +  theories
    4.35      "Interpret"
    4.36  
    4.37  (* run "./bin/isabelle build -v -b Isac"  *)

     5.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Sat Apr 03 15:27:52 2021 +0200
     5.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Sun Apr 04 12:29:42 2021 +0200
     5.3 @@ -80,9 +80,7 @@
     5.4    "~~/test/Pure/Isar/Theory_Commands"            (* Duplicate outer syntax command "ISAC"   *)
     5.5    "~~/test/Pure/Isar/Downto_Synchronized"        (* re-defines / breaks structures      !!! *)
     5.6    \--- .. these work independently, but create problems here *)
     5.7 -(**)"~~/test/Pure/Isar/Check_Outer_Syntax"
     5.8  (**)"~~/test/Pure/Isar/Test_Parsers"
     5.9 -(**)"~~/test/Pure/Isar/Test_Parse_Term"
    5.10  (**)"~~/test/HOL/Tools/Sledgehammer/Try_Sledgehammer"
    5.11  (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
    5.12    "~~/test/Tools/isac/Specify/refine"        (* setup for refine.sml   *)