1.1 --- a/test/Tools/isac/Test_Isac.thy	Sat Nov 12 17:21:43 2016 +0100
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Mon Nov 14 15:51:10 2016 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4  (* Title:  All tests on isac (some outcommented since Isabelle2002-->2009-2)
     1.5     Author: Walther Neuper 101001
     1.6 -   (c) copyright due to lincense terms.
     1.7 +   (c) copyright due to license terms.
     1.8  
     1.9     Isac's tests are organised parallel to sources: 
    1.10       "~~/test/Tools/isac" has same directory structure as "~~/src/Tools/isac"
    1.11 @@ -12,10 +12,27 @@
    1.12  $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy &
    1.13  *)
    1.14  
    1.15 -(* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)
    1.16 -(* !!!!! say "OK" to the popup asking for theories to be loaded and !!!!!!!!!!!!! *)
    1.17 -(* !!!!! watch the <Theories> window for errors in the "imports" below !!!!!!!!!! *)
    1.18 -(* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)
    1.19 +section \<open>Prepare running tests\<close>
    1.20 +text \<open>
    1.21 +Isac encapsulates code as much as possible in structures without open. TODO
    1.22 +This policy conflicts with those tests, which go into functions to details
    1.23 +not declared in the signatures.
    1.24 +
    1.25 +In order to maintain these tests without changes, this has to be done before running tests:
    1.26 +* Query replace in src/Tools/isac:
    1.27 +    "--- ! aktivate for Test_Isac BEGIN ---\* )" --> "--- ! aktivate for Test_Isac BEGIN ---\*)"
    1.28 +    "( *\--- ! aktivate for Test_Isac END ---"   --> "(*\--- ! aktivate for Test_Isac END ---"
    1.29 +  This extends the signatures with some functions required for some tests.
    1.30 +* The same query replace below; this opens all structures.
    1.31 +
    1.32 +*********************** DON'T FORGET TO REVERSE THESE CHANGES AFTER TESTS ***********************
    1.33 +\<close>
    1.34 +
    1.35 +section \<open>Run the tests\<close>
    1.36 +text \<open>
    1.37 +* say "OK" to the popup asking for theories to be loaded
    1.38 +* watch the <Theories> window for errors in the "imports" below
    1.39 +\<close>
    1.40  
    1.41  theory Test_Isac imports Build_Thydata
    1.42    "ADDTESTS/accumulate-val/Thy_All"
    1.43 @@ -45,6 +62,11 @@
    1.44  begin
    1.45  
    1.46  ML {*
    1.47 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    1.48 +  open Lucin;
    1.49 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.50 +*}
    1.51 +ML {*
    1.52    KEStore_Elems.set_ref_thy @{theory};
    1.53    (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*);
    1.54  *}