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 *)