1.1 --- a/test/Pure/Isar/README	Thu Oct 22 14:03:40 2020 +0200
     1.2 +++ b/test/Pure/Isar/README	Thu Oct 22 15:40:41 2020 +0200
     1.3 @@ -19,4 +19,4 @@
     1.4  Test_Parsers_Cookbook.thy Work along book: Scan strings, Scan token list, Scan.optional,
     1.5                            recursive parsers
     1.6  Theory_Commands.thy       original from Makarius 2020 + Isac example
     1.7 -^^^^^^^^^^^^^^^^^^^<----- ML_file "~~/src/Tools/isac/BridgeJEdit/parseC.sml"
     1.8 +^^^^^^^^^^^^^^^^^^^<----- ML_file    "~~/src/Tools/isac/BridgeJEdit/parseC.sml"

     2.1 --- a/test/Tools/isac/Test_Isac.thy	Thu Oct 22 14:03:40 2020 +0200
     2.2 +++ b/test/Tools/isac/Test_Isac.thy	Thu Oct 22 15:40:41 2020 +0200
     2.3 @@ -73,6 +73,14 @@
     2.4  (**)"~~/test/Tools/isac/ADDTESTS/session-get_theory/Foo"
     2.5  (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
     2.6     ADDTESTS/------------------------------------------- see end of tests *)
     2.7 +(*/--- these work directly from Pure, but create problems here ..
     2.8 +  "~~/test/Pure/Isar/Keyword_ISAC.thy"           (* Malformed theory import, "keywords" ?!? *)
     2.9 +  "~~/test/Pure/Isar/Test_Parse_Isac.thy"        (* Malformed theory import, "keywords" ?!? *)
    2.10 +  "~~/test/Pure/Isar/Test_Parsers_Cookbook.thy"  (* Malformed theory import             ?!? *)
    2.11 +  "~~/test/Pure/Isar/Theory_Commands"            (*Duplicate outer syntax command "ISAC"    *)
    2.12 +  \--- .. these work independently, but create problems here *)
    2.13 +(**)"~~/test/Pure/Isar/Check_Outer_Syntax"
    2.14 +(** )"~~/test/Pure/Isar/Downto_Synchorinzed"( *TODO: errors to resolve*)
    2.15  (**)"~~/test/Pure/Isar/Test_Parsers"
    2.16  (**)"~~/test/Pure/Isar/Test_Parse_Term"
    2.17  (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
    2.18 @@ -231,7 +239,6 @@
    2.19  subsection \<open>further functionality alongside batch build sequence\<close>
    2.20    ML_file "MathEngBasic/thmC.sml"
    2.21    ML_file "MathEngBasic/rewrite.sml"
    2.22 -(*ML_file "MathEngBasic/mstools.sml"*)
    2.23    ML_file "MathEngBasic/tactic.sml"
    2.24    ML_file "MathEngBasic/ctree.sml"
    2.25    ML_file "MathEngBasic/calculation.sml"
    2.26 @@ -276,6 +283,8 @@
    2.27  (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
    2.28    ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
    2.29  
    2.30 +  ML_file "BridgeJEdit/parseC.sml"
    2.31 +
    2.32    ML_file "Knowledge/delete.sml"
    2.33    ML_file "Knowledge/descript.sml"
    2.34    ML_file "Knowledge/simplify.sml"

     3.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Thu Oct 22 14:03:40 2020 +0200
     3.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Thu Oct 22 15:40:41 2020 +0200
     3.3 @@ -73,12 +73,14 @@
     3.4  (**)"~~/test/Tools/isac/ADDTESTS/session-get_theory/Foo"
     3.5  (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
     3.6     ADDTESTS/------------------------------------------- see end of tests *)
     3.7 -(*/--- these work independently, but create problems here ..
     3.8 +(*/--- these work directly from Pure, but create problems here ..
     3.9    "~~/test/Pure/Isar/Keyword_ISAC.thy"           (* Malformed theory import, "keywords" ?!? *)
    3.10 -  "~~/test/Pure/Isar/Keywords_Diag.thy"          (* Malformed theory import, "keywords" ?!? *)
    3.11    "~~/test/Pure/Isar/Test_Parse_Isac.thy"        (* Malformed theory import, "keywords" ?!? *)
    3.12    "~~/test/Pure/Isar/Test_Parsers_Cookbook.thy"  (* Malformed theory import             ?!? *)
    3.13 +  "~~/test/Pure/Isar/Theory_Commands"            (*Duplicate outer syntax command "ISAC"    *)
    3.14    \--- .. these work independently, but create problems here *)
    3.15 +(**)"~~/test/Pure/Isar/Check_Outer_Syntax"
    3.16 +(** )"~~/test/Pure/Isar/Downto_Synchorinzed"( *TODO: errors to resolve*)
    3.17  (**)"~~/test/Pure/Isar/Test_Parsers"
    3.18  (**)"~~/test/Pure/Isar/Test_Parse_Term"
    3.19  (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
    3.20 @@ -311,7 +313,7 @@
    3.21    ML_file "Knowledge/polyminus.sml"
    3.22    ML_file "Knowledge/vect.sml"
    3.23    ML_file "Knowledge/diffapp.sml"        (* postponed to dev. specification | TP-prog. *)
    3.24 -  ML_file "Knowledge/biegelinie-1.sml" 
    3.25 +  ML_file "Knowledge/biegelinie-1.sml"
    3.26  (*ML_file "Knowledge/biegelinie-2.sml"                                          Test_Isac_Short*)
    3.27  (*ML_file "Knowledge/biegelinie-3.sml"                                          Test_Isac_Short*)
    3.28    ML_file "Knowledge/biegelinie-4.sml"
    3.29 @@ -332,7 +334,7 @@
    3.30    ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
    3.31    ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>
    3.32    ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
    3.33 -ML \<open> 
    3.34 +ML \<open>
    3.35  \<close> ML \<open>
    3.36  \<close> ML \<open>
    3.37  \<close> ML \<open>