1.1 --- a/src/Tools/isac/Interpret/script.sml	Sat Nov 12 17:21:43 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Mon Nov 14 15:51:10 2016 +0100
     1.3 @@ -15,10 +15,10 @@
     1.4      theory' * rls -> ptree * pos' -> scr -> istate * 'a -> tac_ * (istate * 'a) * (term * safe)
     1.5    val locate_gen : (*diss: locate-function*)
     1.6      theory' * rls -> tac_ -> ptree * pos' -> scr * 'a -> istate * Proof.context -> locate
     1.7 +
     1.8 +(* can these functions be local to Lucin or part of LItools ? *)
     1.9    val sel_rules : ptree -> pos' -> tac list 
    1.10    val init_form : 'a -> scr -> (term * term) list -> term option
    1.11 -  val formal_args : term -> term list
    1.12 -
    1.13    val tac_2tac : tac_ -> tac
    1.14    val init_scrstate : theory -> itm list -> metID -> istate * Proof.context * scr
    1.15    val from_pblobj' : theory' -> pos * pos_ -> ptree -> rls * (istate * Proof.context) * scr
    1.16 @@ -27,16 +27,32 @@
    1.17    val rule2thm'' : rule -> thm''
    1.18    val rule2rls' : rule -> string
    1.19  
    1.20 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    1.21 +  datatype asap = Aundef | AssOnly | AssGen
    1.22 +  datatype appy_ = Napp_ | Skip_
    1.23    val itms2args : 'a -> metID -> itm list -> term list
    1.24 +  val get_stac : 'a -> term -> term option 
    1.25 +  val handle_leaf : string -> theory' -> rls -> env -> term option -> term -> term -> 
    1.26 +    term option * stacexpr
    1.27 +  val formal_args : term -> term list
    1.28 +  val go : loc_ -> term -> term
    1.29 +  val id_of_scr : term -> string
    1.30 +  type appy
    1.31 +  val appy : theory' * rls -> ptree * pos' -> env -> lrd list -> term -> term option -> term -> appy
    1.32 +  val sel_appl_atomic_tacs : ptree -> pos' -> tac list
    1.33 +  val nstep_up : theory' * rls -> ptree * pos' -> scr -> env -> lrd list -> appy_ -> 
    1.34 +    term option -> term -> appy
    1.35 +  val upd_env_opt : env -> term option * term -> env
    1.36 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.37  end 
    1.38  
    1.39 +(* traces the leaves (ie. non-tactical nodes) of Prog found by next_tac, see "and scr" *)   
    1.40 +val trace_script = Unsynchronized.ref false; (* TODO: how are traces done in Isabelle? *)
    1.41 +
    1.42  (**)
    1.43 -structure Lucin: LUCAS_INTERPRETER(**) =
    1.44 +structure Lucin(*: LUCAS_INTERPRETER*) =
    1.45  struct
    1.46  (**)
    1.47 -(* traces the leaves (ie. non-tactical nodes) of Prog found by next_tac, see "and scr" *)   
    1.48 -val trace_script = Unsynchronized.ref false;
    1.49 -
    1.50  (* data for creating a new node in ctree; designed for use as:
    1.51     fun ass* scrstate steps = / ... case ass* scrstate steps of /
    1.52     Assoc (scrstate, steps) => ... ass* scrstate steps *)

     2.1 --- a/test/Tools/isac/Test_Isac.thy	Sat Nov 12 17:21:43 2016 +0100
     2.2 +++ b/test/Tools/isac/Test_Isac.thy	Mon Nov 14 15:51:10 2016 +0100
     2.3 @@ -1,6 +1,6 @@
     2.4  (* Title:  All tests on isac (some outcommented since Isabelle2002-->2009-2)
     2.5     Author: Walther Neuper 101001
     2.6 -   (c) copyright due to lincense terms.
     2.7 +   (c) copyright due to license terms.
     2.8  
     2.9     Isac's tests are organised parallel to sources: 
    2.10       "~~/test/Tools/isac" has same directory structure as "~~/src/Tools/isac"
    2.11 @@ -12,10 +12,27 @@
    2.12  $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy &
    2.13  *)
    2.14  
    2.15 -(* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)
    2.16 -(* !!!!! say "OK" to the popup asking for theories to be loaded and !!!!!!!!!!!!! *)
    2.17 -(* !!!!! watch the <Theories> window for errors in the "imports" below !!!!!!!!!! *)
    2.18 -(* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)
    2.19 +section \<open>Prepare running tests\<close>
    2.20 +text \<open>
    2.21 +Isac encapsulates code as much as possible in structures without open. TODO
    2.22 +This policy conflicts with those tests, which go into functions to details
    2.23 +not declared in the signatures.
    2.24 +
    2.25 +In order to maintain these tests without changes, this has to be done before running tests:
    2.26 +* Query replace in src/Tools/isac:
    2.27 +    "--- ! aktivate for Test_Isac BEGIN ---\* )" --> "--- ! aktivate for Test_Isac BEGIN ---\*)"
    2.28 +    "( *\--- ! aktivate for Test_Isac END ---"   --> "(*\--- ! aktivate for Test_Isac END ---"
    2.29 +  This extends the signatures with some functions required for some tests.
    2.30 +* The same query replace below; this opens all structures.
    2.31 +
    2.32 +*********************** DON'T FORGET TO REVERSE THESE CHANGES AFTER TESTS ***********************
    2.33 +\<close>
    2.34 +
    2.35 +section \<open>Run the tests\<close>
    2.36 +text \<open>
    2.37 +* say "OK" to the popup asking for theories to be loaded
    2.38 +* watch the <Theories> window for errors in the "imports" below
    2.39 +\<close>
    2.40  
    2.41  theory Test_Isac imports Build_Thydata
    2.42    "ADDTESTS/accumulate-val/Thy_All"
    2.43 @@ -45,6 +62,11 @@
    2.44  begin
    2.45  
    2.46  ML {*
    2.47 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    2.48 +  open Lucin;
    2.49 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    2.50 +*}
    2.51 +ML {*
    2.52    KEStore_Elems.set_ref_thy @{theory};
    2.53    (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*);
    2.54  *}