1.1 --- a/src/Tools/isac/Frontend/interface.sml	Tue Jun 25 10:46:20 2019 +0200
     1.2 +++ b/src/Tools/isac/Frontend/interface.sml	Tue Jun 25 12:48:24 2019 +0200
     1.3 @@ -443,7 +443,7 @@
     1.4    in
     1.5      case Math_Engine.step pos cs of
     1.6  	    ("ok", cs') =>
     1.7 -	      (case LucinNEW.inform cs' (encode ifo) of
     1.8 +	      (case LucinNEW.locate_input_formula cs' (encode ifo) of
     1.9  	        ("ok", (_(*use in DG !!!*), c, ptp as (_, p))) =>
    1.10  	          (upd_calc cI (ptp, []); upd_ipos cI 1 p;
    1.11  	          appendformulaOK2xml cI pos (if null c then pos else last_elem c) p)
    1.12 @@ -463,7 +463,7 @@
    1.13      val ((pt, _), _) = get_calc cI
    1.14      val p = get_pos cI 1
    1.15    in
    1.16 -    case LucinNEW.inform (([], [], (pt, p)): Chead.calcstate') (encode ifo) of
    1.17 +    case LucinNEW.locate_input_formula (([], [], (pt, p)): Chead.calcstate') (encode ifo) of
    1.18  	    ("ok", (_(*tacs used for DG ?*), c, ptp' as (_, p'))) =>
    1.19  	      let
    1.20  	        val unc = if null (fst p) then p else move_up [] pt p

     2.1 --- a/src/Tools/isac/Interpret/appl.sml	Tue Jun 25 10:46:20 2019 +0200
     2.2 +++ b/src/Tools/isac/Interpret/appl.sml	Tue Jun 25 12:48:24 2019 +0200
     2.3 @@ -116,7 +116,7 @@
     2.4    in ((scan []) o Symbol.explode) str end;
     2.5  
     2.6  (* applicability of a tacic wrt. a calc-state (ctree,pos').
     2.7 -   additionally used by next_tac in the script-interpreter for script-tacs.
     2.8 +   additionally used by determine_next_tactic.
     2.9     tests for applicability are so expensive, that results (rewrites!)
    2.10     are kept in the return-value of 'type tac_'                            *)
    2.11  fun applicable_in _ _ (Tac.Init_Proof (ct', spec)) = Chead.Appl (Tac.Init_Proof' (ct', spec))
    2.12 @@ -425,7 +425,7 @@
    2.13  		    end
    2.14    | applicable_in _ _ (Tac.Apply_Assumption cts') = 
    2.15      error ("applicable_in: not impl. for " ^ Tac.tac2str (Tac.Apply_Assumption cts'))
    2.16 -    (* 'logical' applicability wrt. script in locate: Inconsistent? *)
    2.17 +    (* 'logical' applicability wrt. script in locate_input_tactic: Inconsistent? *)
    2.18    | applicable_in _ _ (Tac.Take_Inst ct') =
    2.19      error ("applicable_in: not impl. for " ^ Tac.tac2str (Tac.Take_Inst ct'))
    2.20    | applicable_in (p, p_) pt (m as Tac.Subproblem (domID, pblID)) = 

     3.1 --- a/src/Tools/isac/Interpret/ctree-basic.sml	Tue Jun 25 10:46:20 2019 +0200
     3.2 +++ b/src/Tools/isac/Interpret/ctree-basic.sml	Tue Jun 25 12:48:24 2019 +0200
     3.3 @@ -192,7 +192,7 @@
     3.4  # generate1 does NOT set pos, because certain nodes can be lev_on OR lev_dn
     3.5                       exceptions: Begin/End_Trans
     3.6  # thus generate(1) called in
     3.7 -.# assy, locate_gen 
     3.8 +.# assy, locate_input_tactic 
     3.9  .# nxt_solv (tac_ -cases); general case: 
    3.10    val pos' = case pos' of (p,Res) => (lev_on p',Res) | _ => pos'
    3.11  # WN050220, S(604):

     4.1 --- a/src/Tools/isac/Interpret/ctree-navi.sml	Tue Jun 25 10:46:20 2019 +0200
     4.2 +++ b/src/Tools/isac/Interpret/ctree-navi.sml	Tue Jun 25 12:48:24 2019 +0200
     4.3 @@ -49,7 +49,7 @@
     4.4  fun lev_up [] = raise PTREE "lev_up []"
     4.5    | lev_up p = (drop_last p):pos;
     4.6  
     4.7 -(*040216: for inform --> embed_deriv: remains on same level TODO.WN120517 compare lev_pred*)
     4.8 +(*040216: for locate_input_formula --> embed_deriv: remains on same level TODO.WN120517 compare lev_pred*)
     4.9  fun lev_back' ([], _) = raise PTREE "lev_back': called by ([],_)"
    4.10    | lev_back' (p, _) =
    4.11      if last_elem p <= 1 then (p, Frm) 

     5.1 --- a/src/Tools/isac/Interpret/inform.sml	Tue Jun 25 10:46:20 2019 +0200
     5.2 +++ b/src/Tools/isac/Interpret/inform.sml	Tue Jun 25 12:48:24 2019 +0200
     5.3 @@ -438,7 +438,7 @@
     5.4      | _ => error "find_fillpatterns: uncovered case of get_met"
     5.5      val env = case Ctree.get_istate pt pos of
     5.6  		  Selem.ScrState (env, _, _, _, _, _) => env
     5.7 -		| _ => error "inform: uncovered case of get_istate"
     5.8 +		| _ => error "locate_input_formula: uncovered case of get_istate"
     5.9      val subst = Rtools.get_bdv_subst prog env
    5.10      val errpatthms = errpats
    5.11        |> filter ((curry op = errpatID) o (#1: Rule.errpat -> Rule.errpatID))

     6.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml	Tue Jun 25 10:46:20 2019 +0200
     6.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml	Tue Jun 25 12:48:24 2019 +0200
     6.3 @@ -5,16 +5,18 @@
     6.4  
     6.5  signature LUCAS_INTERPRETER =
     6.6  sig
     6.7 -  val next_tac : Rule.theory' * Rule.rls -> Ctree.state -> Rule.scr -> Selem.istate * 'a -> Tac.tac_ * (Selem.istate * 'a) * (term * Selem.safe)
     6.8 +  val determine_next_tactic : Rule.theory' * Rule.rls -> Ctree.state -> Rule.scr -> Selem.istate * 'a ->
     6.9 +    Tac.tac_ * (Selem.istate * 'a) * (term * Selem.safe)
    6.10  
    6.11    datatype locate = Steps of Selem.istate * Lucin.step list | NotLocatable
    6.12 -  val locate_gen : Rule.theory' * Rule.rls -> Tac.tac_ -> Ctree.state -> Rule.scr * 'a -> Selem.istate * Proof.context -> locate
    6.13 +  val locate_input_tactic : Rule.theory' * Rule.rls -> Tac.tac_ -> Ctree.state -> Rule.scr * 'a ->
    6.14 +    Selem.istate * Proof.context -> locate
    6.15  
    6.16 -  val inform : Chead.calcstate' -> string -> string * Chead.calcstate'
    6.17 -  val nxt_solv : Tac.tac_ -> Selem.istate * Proof.context -> Ctree.ctree * (Ctree.pos') -> (Tac.tac * Tac.tac_ * (Ctree.pos' * (Selem.istate * Proof.context))) list * Ctree.pos' list * (Ctree.ctree * Ctree.pos')
    6.18 -  val nxt_solve_ : Ctree.ctree * Ctree.pos' ->
    6.19 -    (Tac.tac * Tac.tac_ * (Ctree.pos' * (Selem.istate * Proof.context))) list *
    6.20 -      Ctree.pos' list * Ctree.state
    6.21 +  val locate_input_formula : Chead.calcstate' -> string -> string (*..drop*)* Chead.calcstate'
    6.22 +  val nxt_solv : Tac.tac_ -> Selem.istate * Proof.context -> Ctree.state ->
    6.23 +    (Tac.tac * Tac.tac_ * (Ctree.pos' * (Selem.istate * Proof.context))) list * Ctree.pos' list * Ctree.state
    6.24 +  val nxt_solve_ : Ctree.state ->
    6.25 +    (Tac.tac * Tac.tac_ * (Ctree.pos' * (Selem.istate * Proof.context))) list * Ctree.pos' list * Ctree.state
    6.26  
    6.27  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    6.28    type assoc
    6.29 @@ -49,7 +51,7 @@
    6.30  
    6.31  (** find the next tactic by executing the program **)
    6.32  
    6.33 -(*appy, nxt_up, nstep_up scanning for next_tac.
    6.34 +(*appy, nxt_up, nstep_up scanning for determine_next_tactic.
    6.35    search is clearly separated into (1)-(2):
    6.36    (1) appy is recursive descent;
    6.37    (2) nxt_up resumes interpretation at a location somewhere in the script;
    6.38 @@ -233,18 +235,18 @@
    6.39              (.. not true for other details ..PrfObj ??????????????????
    6.40     20.8.02: do NOT return safe (is only changed in locate !!!)
    6.41  *)
    6.42 -fun next_tac (thy,_) _ (Rule.Rfuns {next_rule, ...}) (Selem.RrlsState(f, f', rss, _), ctxt) =
    6.43 +fun determine_next_tactic (thy,_) _ (Rule.Rfuns {next_rule, ...}) (Selem.RrlsState(f, f', rss, _), ctxt) =
    6.44      if f = f'
    6.45      then (Tac.End_Detail' (f',[])(*8.6.03*), (Selem.Uistate, ctxt), 
    6.46 -    	(f', Selem.Sundef(*FIXME is no value of next_tac! vor 8.6.03*)))                (*finished*)
    6.47 +    	(f', Selem.Sundef(*FIXME is no value of determine_next_tactic! vor 8.6.03*)))        (*finished*)
    6.48      else
    6.49        (case next_rule rss f of
    6.50      	  NONE => (Tac.Empty_Tac_, (Selem.Uistate, ctxt), (Rule.e_term, Selem.Sundef))       (*helpless*)
    6.51      	| SOME (Rule.Thm thm'')(*8.6.03: muss auch f' liefern ?!!*) => 
    6.52      	    (Tac.Rewrite' (thy, "e_rew_ord", Rule.e_rls, false, thm'', f, (Rule.e_term, [(*!?!8.6.03*)])),
    6.53    	         (Selem.Uistate, ctxt), (Rule.e_term, Selem.Sundef))                          (*next stac*)
    6.54 -      | _ => error "next_tac: uncovered case next_rule")
    6.55 -  | next_tac thy (ptp as (pt, (p, _))) (sc as Rule.Prog prog) 
    6.56 +      | _ => error "determine_next_tactic: uncovered case next_rule")
    6.57 +  | determine_next_tactic thy (ptp as (pt, (p, _))) (sc as Rule.Prog prog) 
    6.58  	    (Selem.ScrState (E,l,a,v,s,_), ctxt) =
    6.59      (case if l = [] then appy thy ptp E [Celem.R] (LTool.body_of prog) NONE v
    6.60            else nstep_up thy ptp sc E l Skip_ a v of
    6.61 @@ -260,13 +262,13 @@
    6.62       | Napp _ => (Tac.Empty_Tac_, (Selem.e_istate, ctxt), (Rule.e_term, Selem.Sundef))     (*helpless*)
    6.63       | Appy (m', scrst as (_,_,_,v,_,_)) =>
    6.64           (m', (Selem.ScrState scrst, ctxt), (v, Selem.Sundef)))                      (*next stac*)
    6.65 -  | next_tac _ _ _ (is, _) = error ("next_tac: not impl for " ^ (Selem.istate2str is));
    6.66 +  | determine_next_tactic _ _ _ (is, _) = error ("determine_next_tactic: not impl for " ^ (Selem.istate2str is));
    6.67  
    6.68  (** locate an input tactic in the program **)
    6.69  
    6.70  datatype assoc =   (* ExprVal in the sense of denotational semantics               *)
    6.71    Assoc of         (* the stac is associated, strongly or weakly                   *)
    6.72 -  Selem.scrstate * (* the current; returned for next_tac etc. outside ass*         *)  
    6.73 +  Selem.scrstate * (* the current; returned for determine_next_tactic etc. outside ass*         *)  
    6.74    (Lucin.step list)      (* list of steps done until associated stac found;
    6.75  	                    initiated with the data for doing the 1st step,
    6.76                        thus the head holds these data further on,
    6.77 @@ -289,7 +291,7 @@
    6.78                     search for _applicable_ stacs, execute and generate pt        *)
    6.79  (*this constructions doesnt allow arbitrary nesting of Or !!!                    *)
    6.80  
    6.81 -(* assy, ass_up, astep_up scan for locate_gen in a script.
    6.82 +(* assy, ass_up, astep_up scan for locate_input_tactic in a script.
    6.83     search is clearly separated into (1)-(2):
    6.84     (1) assy is recursive descent;
    6.85     (2) ass_up resumes interpretation at a location somewhere in the script;
    6.86 @@ -484,12 +486,12 @@
    6.87  
    6.88  datatype locate =
    6.89    Steps of Selem.istate (* producing hd of step list (which was latest)
    6.90 -	                         for next_tac, for reporting Safe|Unsafe to DG  *)
    6.91 +	                         for determine_next_tactic, for reporting Safe|Unsafe to DG  *)
    6.92  	   * Lucin.step       (* (scrstate producing this step is in ctree !)   *) 
    6.93 -		 list               (* locate_gen may produce intermediate steps      *)
    6.94 +		 list               (* locate_input_tactic may produce intermediate steps      *)
    6.95  | NotLocatable;         (* no (m Ass m') or (m AssWeak m') found          *)
    6.96  
    6.97 -(* locate_gen tries to locate an input tac m in the script. 
    6.98 +(* locate_input_tactic tries to locate an input tac m in the script. 
    6.99     pursuing this goal the script is executed until an (m' equiv m) is found,
   6.100     or the end of the script
   6.101  args
   6.102 @@ -509,12 +511,12 @@
   6.103            NOT IMPL. -- "error: do other step before"
   6.104     NotLocatable: thus generate_hard
   6.105  *)
   6.106 -fun locate_gen (thy', _) (Tac.Rewrite' (_, ro, er, pa, thm, f, _)) (pt, p) (*TODO-LucinNEW del in script.sml*)
   6.107 +fun locate_input_tactic (thy', _) (Tac.Rewrite' (_, ro, er, pa, thm, f, _)) (pt, p) (*TODO-LucinNEW del in script.sml*)
   6.108  	    (Rule.Rfuns {locate_rule=lo,...}, _) (Selem.RrlsState (_,f'',rss,rts), _) = 
   6.109      (case lo rss f (Rule.Thm thm) of
   6.110  	    [] => NotLocatable
   6.111      | rts' => Steps (Lucin.rts2steps [] ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) rts'))
   6.112 -  | locate_gen (thy', srls) m (pt, p)
   6.113 +  | locate_input_tactic (thy', srls) m (pt, p)
   6.114  	    (scr as Rule.Prog sc, d) (Selem.ScrState (E,l,a,v,S,b), ctxt)  = 
   6.115      let val thy = Celem.assoc_thy thy';
   6.116      in case if l = [] orelse (
   6.117 @@ -530,7 +532,7 @@
   6.118  	         then
   6.119               let
   6.120                 val (po,p_) = p
   6.121 -               val po' = case p_ of Frm => po | Res => lev_on po | _ => error ("locate_gen " ^ pos_2str p_)
   6.122 +               val po' = case p_ of Frm => po | Res => lev_on po | _ => error ("locate_input_tactic " ^ pos_2str p_)
   6.123                 val (p'',c'',f'',pt'') = Generate.generate1 thy m (Selem.ScrState is, ctxt) (po',p_) pt
   6.124  	           in Steps (Selem.ScrState is, [(m, f'',pt'',p'',c'')]) end
   6.125  	         else Steps (Selem.ScrState is, ss))
   6.126 @@ -538,8 +540,8 @@
   6.127      | NasApp _ => NotLocatable
   6.128      | err => error ("not-found-in-script: NotLocatable from " ^ @{make_string} err)
   6.129      end
   6.130 -  | locate_gen _ m _ (sc,_) (is, _) = 
   6.131 -    error ("locate_gen: wrong arguments,\n tac= " ^ Tac.tac_2str m ^ ",\n " ^
   6.132 +  | locate_input_tactic _ m _ (sc,_) (is, _) = 
   6.133 +    error ("locate_input_tactic: wrong arguments,\n tac= " ^ Tac.tac_2str m ^ ",\n " ^
   6.134        "scr= " ^ Rule.scr2str sc ^ ",\n istate= " ^ Selem.istate2str is);
   6.135  
   6.136  (** locate an input formula in the program **)
   6.137 @@ -605,7 +607,7 @@
   6.138        | _ => error "nxt_solv Check_Postcond': uncovered case get_loc"
   6.139        val thy' = get_obj g_domID pt pp;
   6.140        val thy = Celem.assoc_thy thy';
   6.141 -      val (_, _, (scval, scsaf)) = next_tac (thy', srls) (pt, (p, p_)) sc loc;
   6.142 +      val (_, _, (scval, scsaf)) = determine_next_tactic (thy', srls) (pt, (p, p_)) sc loc;
   6.143      in
   6.144        if pp = []
   6.145        then 
   6.146 @@ -647,14 +649,14 @@
   6.147        let 
   6.148          val thy' = get_obj g_domID pt (par_pblobj pt p);
   6.149  	      val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
   6.150 -	      val (tac_, is, (t, _)) = next_tac (thy', srls) (pt, pos) sc is;
   6.151 +	      val (tac_, is, (t, _)) = determine_next_tactic (thy', srls) (pt, pos) sc is;
   6.152  	      (* TODO here  ^^^  return finished/helpless/ok !*)
   6.153  	    in case tac_ of
   6.154  		    Tac.End_Detail' _ => ([(Tac.End_Detail, Tac.End_Detail' (t, [(*FIXME.04*)]), (pos, is))], [], (pt, pos))
   6.155  	    | _ => nxt_solv tac_ is ptp
   6.156        end;
   6.157   
   6.158 -(* compare inform with ctree.form at current pos by nrls;
   6.159 +(* compare locate_input_formula with ctree.form at current pos by nrls;
   6.160     if found, embed the derivation generated during comparison
   6.161     if not, let the mat-engine compute the next ctree.form *)
   6.162  (* code's structure is copied from complete_solve
   6.163 @@ -704,7 +706,7 @@
   6.164     collect all the tacs applied by the way;
   6.165     if "no derivation found" then check_error_patterns.
   6.166     ALTERNATIVE: check_error_patterns _within_ compare_step seems too expensive.*)
   6.167 -fun inform (cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr =
   6.168 +fun locate_input_formula (cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr =
   6.169    case TermC.parse (Celem.assoc_thy "Isac") istr of
   6.170  	  SOME f_in =>
   6.171  	    let
   6.172 @@ -729,10 +731,10 @@
   6.173  			                 val pp = Ctree.par_pblobj pt p
   6.174  			                 val (errpats, nrls, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
   6.175  			                   {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
   6.176 -			                 | _ => error "inform: uncovered case of get_met"
   6.177 +			                 | _ => error "locate_input_formula: uncovered case of get_met"
   6.178  			                 val env = case Ctree.get_istate pt pos of
   6.179  			                   Selem.ScrState (env, _, _, _, _, _) => env
   6.180 -			                 | _ => error "inform: uncovered case of get_istate"
   6.181 +			                 | _ => error "locate_input_formula: uncovered case of get_istate"
   6.182  			               in
   6.183  			                 case Inform.check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
   6.184  			                   SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate')

     7.1 --- a/src/Tools/isac/Interpret/script.sml	Tue Jun 25 10:46:20 2019 +0200
     7.2 +++ b/src/Tools/isac/Interpret/script.sml	Tue Jun 25 12:48:24 2019 +0200
     7.3 @@ -45,7 +45,7 @@
     7.4  
     7.5  end 
     7.6  
     7.7 -(* traces the leaves (ie. non-tactical nodes) of Prog found by next_tac, see "and scr" *)   
     7.8 +(* traces the leaves (ie. non-tactical nodes) of Prog found by determine_next_tactic, see "and scr" *)   
     7.9  val trace_script = Unsynchronized.ref false; (* TODO: how are traces done in Isabelle? *)
    7.10  
    7.11  structure Lucin(**): LUCAS_INTERPRETER_DEL(**) =
    7.12 @@ -638,7 +638,7 @@
    7.13  	         val metID = get_obj g_metID pt p'
    7.14  	         val {srls,...} = Specify.get_met metID
    7.15  	       in (srls, get_loc pt (p,p_), (#scr o Specify.get_met) metID) end
    7.16 -       else (*FIXME.WN0?: get from pbl or met !!! unused for Rrls in locate_gen, next_tac*) (* 3 *)
    7.17 +       else (*FIXME.WN0?: get from pbl or met !!! unused for Rrls in locate_input_formula, determine_next_tactic*) (* 3 *)
    7.18  	       (Rule.e_rls, get_loc pt (p,p_),
    7.19  	          case rls' of
    7.20  		          Rule.Rls {scr = scr,...} => scr

     8.1 --- a/src/Tools/isac/Interpret/solve.sml	Tue Jun 25 10:46:20 2019 +0200
     8.2 +++ b/src/Tools/isac/Interpret/solve.sml	Tue Jun 25 12:48:24 2019 +0200
     8.3 @@ -134,10 +134,10 @@
     8.4  	        end	      
     8.5  	    | NONE => (*execute the first tac in the Script, compare solve m*)
     8.6  	        let
     8.7 -            val (m', (is', ctxt'), _) = LucinNEW.next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
     8.8 +            val (m', (is', ctxt'), _) = LucinNEW.determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt);
     8.9  	          val d = Rule.e_rls (*FIXME: get simplifier from domID*);
    8.10  	        in 
    8.11 -	          case LucinNEW.locate_gen (thy',srls) m' (pt,(p, Res)) (sc,d) (is', ctxt') of 
    8.12 +	          case LucinNEW.locate_input_tactic (thy',srls) m' (pt,(p, Res)) (sc,d) (is', ctxt') of 
    8.13  		          LucinNEW.Steps (_, ss as (_, _, pt', p', c') :: _) =>
    8.14  		            ("ok", (map step2taci ss, c', (pt', p')))
    8.15  		        | _ => (* NotLocatable *)
    8.16 @@ -170,7 +170,7 @@
    8.17        | _ => error "solve Check_Postcond: uncovered case get_loc"
    8.18        val thy' = get_obj g_domID pt pp;
    8.19        val thy = Celem.assoc_thy thy';
    8.20 -      val (_, _, (scval, scsaf)) = LucinNEW.next_tac (thy', srls) (pt, (p, p_)) sc loc;
    8.21 +      val (_, _, (scval, scsaf)) = LucinNEW.determine_next_tactic (thy', srls) (pt, (p, p_)) sc loc;
    8.22      in 
    8.23        if pp = [] 
    8.24        then
    8.25 @@ -218,10 +218,10 @@
    8.26  	      val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
    8.27  		    val d = Rule.e_rls; (*FIXME.WN0108: canon.simplifier for domain is missing: generate from domID?*)
    8.28  	    in
    8.29 -        case LucinNEW.locate_gen (thy', srls) m  (pt, (p, p_)) (sc, d) is of
    8.30 +        case LucinNEW.locate_input_tactic (thy', srls) m  (pt, (p, p_)) (sc, d) is of
    8.31  	        LucinNEW.Steps (_, ss as (_, _, pt', p', c') :: _) =>
    8.32  	          ("ok", (map step2taci ss, c', (pt', p')))
    8.33 -            (*27.8.02:next_tac may change to other branches in pt FIXXXXME*)
    8.34 +            (*27.8.02:determine_next_tactic may change to other branches in pt FIXXXXME*)
    8.35  	      | _ => (* NotLocatable *)
    8.36  	        let 
    8.37  	          val (p,ps, _, pt) = Generate.generate_hard (Celem.assoc_thy "Isac") m (p, p_) pt;

     9.1 --- a/src/Tools/isac/ThydataC/rule.sml	Tue Jun 25 10:46:20 2019 +0200
     9.2 +++ b/src/Tools/isac/ThydataC/rule.sml	Tue Jun 25 12:48:24 2019 +0200
     9.3 @@ -202,7 +202,7 @@
     9.4    | Rfuns of     (* for Rrls, usage see rational.sml ----- reverse rewrite -----      *)
     9.5      {init_state : (* initialise for reverse rewriting by the Interpreter              *)
     9.6        term ->         (* for this the rrlsstate is initialised:                       *)
     9.7 -      term *          (* the current formula: goes locate_gen -> next_tac via istate  *)
     9.8 +      term *          (* the current formula: goes locate_input_tactic -> determine_next_tactic via istate  *)
     9.9        term *          (* the final formula                                            *)
    9.10        rule list       (* of reverse rewrite set (#1#)                                 *)
    9.11          list *        (*   may be serveral, eg. in norm_rational                      *)

    10.1 --- a/test/Tools/isac/Interpret/inform.sml	Tue Jun 25 10:46:20 2019 +0200
    10.2 +++ b/test/Tools/isac/Interpret/inform.sml	Tue Jun 25 12:48:24 2019 +0200
    10.3 @@ -24,7 +24,7 @@
    10.4  "CAS-command:";
    10.5  "--------- CAS-command on ([],Pbl) -------------------------------";
    10.6  "--------- CAS-command on ([],Pbl) FE-interface ------------------";
    10.7 -"--------- inform [rational,simplification] ----------------------";
    10.8 +"--------- locate_input_formula [rational,simplification] ----------------------";
    10.9  "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
   10.10  "--------- Take as 1st tac, start from exp -----------------------";
   10.11  "--------- init_form, start with <NEW> (CAS input) ---------------";
   10.12 @@ -469,7 +469,7 @@
   10.13  val (p,_,f,nxt,_,pt) = 
   10.14      CalcTreeTEST [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
   10.15  val ifo = "solve(x+1=2,x)";
   10.16 -val (_,(_,c,(pt,p))) = inform ([],[],(pt,p)) "solve(x+1=2,x)";
   10.17 +val (_,(_,c,(pt,p))) = locate_input_formula ([],[],(pt,p)) "solve(x+1=2,x)";
   10.18  show_pt pt;
   10.19  val nxt = ("Apply_Method",Apply_Method ["Test","squ-equ-test-subpbl1"]);
   10.20  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   10.21 @@ -492,9 +492,9 @@
   10.22  else error "inform.sml: diff.behav. CAScmd ([],Pbl) FE-interface";
   10.23  DEconstrCalcTree 1;
   10.24  
   10.25 -"--------- inform [rational,simplification] ----------------------";
   10.26 -"--------- inform [rational,simplification] ----------------------";
   10.27 -"--------- inform [rational,simplification] ----------------------";
   10.28 +"--------- locate_input_formula [rational,simplification] ----------------------";
   10.29 +"--------- locate_input_formula [rational,simplification] ----------------------";
   10.30 +"--------- locate_input_formula [rational,simplification] ----------------------";
   10.31  reset_states ();
   10.32  CalcTree [(["Term (a * x / (b * x) + c * x / (d * x) + e / f)", "normalform N"],
   10.33  	("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
   10.34 @@ -1021,7 +1021,7 @@
   10.35     (([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))), <<=== input follos: "...+ cos(4.x^3)"
   10.36     (([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4))] *)
   10.37  
   10.38 -"~~~~~ fun inform, args:"; val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) =
   10.39 +"~~~~~ fun locate_input_formula , args:"; val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) =
   10.40    (cs', (encode ifo));
   10.41  val 	SOME f_in = parse (assoc_thy "Isac") istr
   10.42  val f_in = Thm.term_of f_in
   10.43 @@ -1044,15 +1044,15 @@
   10.44  			                   SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate')
   10.45  			                 | NONE => msg_calcstate';
   10.46  
   10.47 -"~~~~~ from inform return val:"; val () = ();
   10.48 +"~~~~~ from locate_input_formula return val:"; val () = ();
   10.49  case check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
   10.50  			  SOME errpatID => ()
   10.51  			| NONE => error "check_error_patterns broken";
   10.52  
   10.53  "--- final check:";
   10.54 -case inform cs' (encode ifo) of
   10.55 +case locate_input_formula cs' (encode ifo) of
   10.56    ("error pattern #chain-rule-diff-both#", calcstate') => ()
   10.57 -| _ => error "inform with (positive) check_error_patterns broken"
   10.58 +| _ => error "locate_input_formula with (positive) check_error_patterns broken"
   10.59  
   10.60  "--------- build fun get_fillpats --------------------------------";
   10.61  "--------- build fun get_fillpats --------------------------------";

    11.1 --- a/test/Tools/isac/Interpret/mathengine.sml	Tue Jun 25 10:46:20 2019 +0200
    11.2 +++ b/test/Tools/isac/Interpret/mathengine.sml	Tue Jun 25 12:48:24 2019 +0200
    11.3 @@ -144,7 +144,7 @@
    11.4    val ("ok", cs' as (_,_,(pt,p))) = step p cs;
    11.5    val ifo = (* encode "4^^^2" \<longrightarrow>*) "4^2";
    11.6  (*
    11.7 -  val ("no derivation found", (_,_,(pt, p))) = inform cs' ((*encode*) ifo);
    11.8 +  val ("no derivation found", (_,_,(pt, p))) = locate_input_formula cs' ((*encode*) ifo);
    11.9    here ^^^^^^^^^^^^^^^^^^^^^ should be "ok"
   11.10  *)
   11.11  
   11.12 @@ -511,7 +511,7 @@
   11.13  e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
   11.14  val thy' = get_obj g_domID pt (par_pblobj pt p);
   11.15  val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
   11.16 -val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is; (*WAS Empty_Tac_: tac_*)
   11.17 +val (tac_,is,(t,_)) = determine_next_tactic (thy',srls) (pt,pos) sc is; (*WAS Empty_Tac_: tac_*)
   11.18  case tac_ of Or_to_List' _ => ()
   11.19  | _ => error "Or_to_List broken ?"
   11.20  
   11.21 @@ -615,13 +615,13 @@
   11.22  e_metID = get_obj g_metID pt (par_pblobj pt p) = false;
   11.23            val thy' = get_obj g_domID pt (par_pblobj pt p);
   11.24  	        val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
   11.25 -	        val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is;
   11.26 +	        val (tac_,is,(t,_)) = determine_next_tactic (thy',srls) (pt,pos) sc is;
   11.27  (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*)
   11.28 -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), 
   11.29 +"~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), 
   11.30    (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
   11.31  l = [] = false;
   11.32  nstep_up thy ptp sc E l Skip_ a v (*--> Appy (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...)
   11.33 -  BUT WE FIND IN THE CODE ABOVE IN next_tac:*)
   11.34 +  BUT WE FIND IN THE CODE ABOVE IN determine_next_tactic:*)
   11.35  ;
   11.36  (*----------------------------------------------------------------------------------------------*)
   11.37  if string_of_thmI @{thm rnorm_equation_add} =  "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + - 1 * ?b = 0)"
   11.38 @@ -716,8 +716,8 @@
   11.39  (*  val cs = get_calc cI             (* we improve from the calcstate here [*] *);
   11.40      val pos as (_,p_) = get_pos cI 1 (* we improve from the calcstate here [*] *);*)
   11.41  val ("ok", cs') = step pos cs;
   11.42 -(*val ("ok", (_, c, ptp as (_,p))) = *)inform cs' (encode ifo);
   11.43 -"~~~~~ fun inform, args:"; val (cs as (_, _, ptp as (pt, pos as (p, p_))), istr) =
   11.44 +(*val ("ok", (_, c, ptp as (_,p))) = *)locate_input_formula cs' (encode ifo);
   11.45 +"~~~~~ fun locate_input_formula , args:"; val (cs as (_, _, ptp as (pt, pos as (p, p_))), istr) =
   11.46    (cs', (encode ifo));
   11.47  val SOME f_in = parse (assoc_thy "Isac") istr
   11.48  	      val f_in = Thm.term_of f_in

    12.1 --- a/test/Tools/isac/Interpret/script.sml	Tue Jun 25 10:46:20 2019 +0200
    12.2 +++ b/test/Tools/isac/Interpret/script.sml	Tue Jun 25 12:48:24 2019 +0200
    12.3 @@ -152,7 +152,7 @@
    12.4                                   (*WAS stac2tac_ TODO: no match for SubProblem*)
    12.5  val thy' = get_obj g_domID pt (par_pblobj pt p);
    12.6  val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
    12.7 -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ctree * pos'), (sc as Prog (h $ body)), 
    12.8 +"~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt,(p,_)):ctree * pos'), (sc as Prog (h $ body)), 
    12.9  	                               (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
   12.10  l; (*= [R, L, R, L, R, R]*)
   12.11  val Appy (m', scrst as (_,_,_,v,_,_)) = nstep_up thy ptp sc E l Skip_ a v;
   12.12 @@ -201,9 +201,9 @@
   12.13          val ini = init_form thy sc env;
   12.14          val p = lev_dn p;
   12.15  ini = NONE; (*true*)
   12.16 -            val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
   12.17 +            val (m', (is', ctxt'), _) = determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt);
   12.18  	            val d = e_rls (*FIXME: get simplifier from domID*);
   12.19 -"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ctree * pos'), 
   12.20 +"~~~~~ fun locate_input_tactic, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ctree * pos'), 
   12.21  	                     (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) = 
   12.22                     ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
   12.23  val thy = assoc_thy thy';

    13.1 --- a/test/Tools/isac/Knowledge/biegelinie-3.sml	Tue Jun 25 10:46:20 2019 +0200
    13.2 +++ b/test/Tools/isac/Knowledge/biegelinie-3.sml	Tue Jun 25 12:48:24 2019 +0200
    13.3 @@ -105,13 +105,13 @@
    13.4        val ini = Lucin.init_form thy sc env;
    13.5        val p = lev_dn p;
    13.6  val NONE = (*case*) ini (*of*);
    13.7 -            val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
    13.8 +            val (m', (is', ctxt'), _) = determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt);
    13.9  	          val d = Rule.e_rls (*FIXME: get simplifier from domID*);
   13.10  val Steps (_, ss as (_, _, pt', p', c') :: _) =
   13.11 -(*case*) locate_gen (thy',srls) m' (pt,(p, Res)) (sc,d) (is', ctxt') (*of*);
   13.12 +(*case*) locate_input_tactic (thy',srls) m' (pt,(p, Res)) (sc,d) (is', ctxt') (*of*);
   13.13  
   13.14  (*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt' (fst p');
   13.15 -(*+*)(*MISSING after locate_gen:*)
   13.16 +(*+*)(*MISSING after locate_input_tactic:*)
   13.17  (*+*)writeln (oris2str oris); (*[
   13.18  (1, ["1"], #Given,Streckenlast, ["q_0"]),
   13.19  (2, ["1"], #Given,FunktionsVariable, ["x"]),
   13.20 @@ -120,7 +120,7 @@
   13.21                   Biegelinie
   13.22                   AbleitungBiegelinie
   13.23  *)
   13.24 -"~~~~~ fun locate_gen , args:"; val ((thy', srls), m, (pt, p),
   13.25 +"~~~~~ fun locate_input_tactic , args:"; val ((thy', srls), m, (pt, p),
   13.26  	    (scr as Rule.Prog sc, d), (Selem.ScrState (E,l,a,v,S,b), ctxt)) =
   13.27    ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
   13.28  val thy = Celem.assoc_thy thy';

    14.1 --- a/test/Tools/isac/Knowledge/diff.sml	Tue Jun 25 10:46:20 2019 +0200
    14.2 +++ b/test/Tools/isac/Knowledge/diff.sml	Tue Jun 25 12:48:24 2019 +0200
    14.3 @@ -20,7 +20,7 @@
    14.4  "----------- autoCalculate diff after_simplification ----";
    14.5  "----------- autoCalculate differentiate_equality -------";
    14.6  "----------- tests for examples -------------------------";
    14.7 -"------------inform for x^2+x+1 -------------------------";
    14.8 +"------------locate_input_formula for x^2+x+1 -------------------------";
    14.9  "--------------------------------------------------------";
   14.10  "--------------------------------------------------------";
   14.11  "--------------------------------------------------------";
   14.12 @@ -409,9 +409,9 @@
   14.13  val subs = [(str2term "bdv", str2term "l")];
   14.14  val f = str2term "G' = d_d l (l * sqrt (7 * s ^^^ 2 - l ^^^ 2))";
   14.15  
   14.16 -"------------inform for x^2+x+1 -------------------------";
   14.17 -"------------inform for x^2+x+1 -------------------------";
   14.18 -"------------inform for x^2+x+1 -------------------------";
   14.19 +"------------locate_input_formula for x^2+x+1 -------------------------";
   14.20 +"------------locate_input_formula for x^2+x+1 -------------------------";
   14.21 +"------------locate_input_formula for x^2+x+1 -------------------------";
   14.22  reset_states ();
   14.23  CalcTree
   14.24  [(["functionTerm (x^2 + x + 1)",

    15.1 --- a/test/Tools/isac/Knowledge/inssort.sml	Tue Jun 25 10:46:20 2019 +0200
    15.2 +++ b/test/Tools/isac/Knowledge/inssort.sml	Tue Jun 25 12:48:24 2019 +0200
    15.3 @@ -118,7 +118,7 @@
    15.4  "----------- insertion sort: CAS-command -------------------------------------";
    15.5  "----------- insertion sort: CAS-command -------------------------------------";
    15.6  val (p,_,f,nxt,_,pt) = CalcTreeTEST [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
    15.7 -val (_,(_,c,(pt,p))) = inform ([],[],(pt,p)) "Sort {||1, 3, 2||}";
    15.8 +val (_,(_,c,(pt,p))) = locate_input_formula ([],[],(pt,p)) "Sort {||1, 3, 2||}";
    15.9  show_pt pt;
   15.10  val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Apply_Method",..*)
   15.11  val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    16.1 --- a/test/Tools/isac/Knowledge/polyeq.sml	Tue Jun 25 10:46:20 2019 +0200
    16.2 +++ b/test/Tools/isac/Knowledge/polyeq.sml	Tue Jun 25 12:48:24 2019 +0200
    16.3 @@ -192,11 +192,11 @@
    16.4          val thy' = get_obj g_domID pt (par_pblobj pt p);
    16.5  	        val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
    16.6  		        val d = e_rls;
    16.7 -(*locate_gen (thy',srls) m  (pt,(p,p_)) (sc,d) is;
    16.8 +(*locate_input_tactic (thy',srls) m  (pt,(p,p_)) (sc,d) is;
    16.9    WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
   16.10 -"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ctree * pos'), 
   16.11 +"~~~~~ fun locate_input_tactic, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ctree * pos'), 
   16.12  	                                   (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) = 
   16.13 -                                   ((thy',srls), m  ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_gen 2nd pattern *)
   16.14 +                                   ((thy',srls), m  ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_input_tactic 2nd pattern *)
   16.15  val thy = assoc_thy thy';
   16.16  l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
   16.17  (*WAS val NasApp _ =(astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )

    17.1 --- a/test/Tools/isac/Knowledge/rateq.sml	Tue Jun 25 10:46:20 2019 +0200
    17.2 +++ b/test/Tools/isac/Knowledge/rateq.sml	Tue Jun 25 12:48:24 2019 +0200
    17.3 @@ -103,7 +103,7 @@
    17.4  "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
    17.5  val thy' = get_obj g_domID pt (par_pblobj pt p);
    17.6  val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
    17.7 -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
    17.8 +"~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
    17.9    (sc as Prog (h $ body)),
   17.10  (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
   17.11  "~~~~~ fun nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
   17.12 @@ -292,7 +292,7 @@
   17.13  e_metID = get_obj g_metID pt (par_pblobj pt p); (* = false*)
   17.14            val thy' = get_obj g_domID pt (par_pblobj pt p);
   17.15  	        val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
   17.16 -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
   17.17 +"~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
   17.18    (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
   17.19  l = []; (* = false*)
   17.20  "~~~~~ and nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
   17.21 @@ -318,7 +318,7 @@
   17.22  nstep_up thy ptp scr E l ay a v;
   17.23  nxt_up thy ptp (Prog sc) E up ay (go up sc) a v;
   17.24  nstep_up thy ptp sc E l Skip_ a v;
   17.25 -next_tac (thy',srls) (pt,pos) sc is;
   17.26 +determine_next_tactic (thy',srls) (pt,pos) sc is;
   17.27  nxt_solve_ (pt,ip);
   17.28  step p ((pt, e_pos'),[]);
   17.29  *)

    18.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml	Tue Jun 25 10:46:20 2019 +0200
    18.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml	Tue Jun 25 12:48:24 2019 +0200
    18.3 @@ -130,7 +130,7 @@
    18.4  Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = false*);
    18.5          val thy' = get_obj g_domID pt (par_pblobj pt p);
    18.6  	      val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
    18.7 -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Rule.Prog (_ $ body)), 
    18.8 +"~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Rule.Prog (_ $ body)), 
    18.9  	    (Selem.ScrState (E,l,a,v,s,_), ctxt)) = ((thy', srls), (pt, pos), sc, is);
   18.10  l = [] (* = true*);
   18.11  "~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("HOL.Let",_) $ e $ (Abs (i,T,b))), a, v) =

    19.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml	Tue Jun 25 10:46:20 2019 +0200
    19.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml	Tue Jun 25 12:48:24 2019 +0200
    19.3 @@ -44,8 +44,8 @@
    19.4  	      val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
    19.5  		    val d = Rule.e_rls; (*FIXME.WN0108: canon.simplifier for domain is missing: generate from domID?*)
    19.6  
    19.7 -locate_gen (thy',srls) m  (pt,(p, p_)) (sc,d) is;  (* assy: call by ([3], Pbl)*)
    19.8 -"~~~~~ fun locate_gen, args:"; val ((thy', srls), m, (pt, p),
    19.9 +locate_input_tactic (thy',srls) m  (pt,(p, p_)) (sc,d) is;  (* assy: call by ([3], Pbl)*)
   19.10 +"~~~~~ fun locate_input_tactic, args:"; val ((thy', srls), m, (pt, p),
   19.11  	    (scr as Rule.Prog (_ $ body),d), (Selem.ScrState (E,l,a,v,S,b), ctxt)) =
   19.12    ((thy',srls), m,  (pt,(p, p_)), (sc,d), is);
   19.13  val thy = Celem.assoc_thy thy';
   19.14 @@ -109,9 +109,9 @@
   19.15          val thy' = get_obj g_domID pt (par_pblobj pt p);
   19.16  	      val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
   19.17  
   19.18 -(* isabisac17: val (tac_, is, (t, _)) = Lucin.next_tac (thy', srls) (pt, pos) sc is;
   19.19 +(* isabisac17: val (tac_, is, (t, _)) = determine_next_tactic (thy', srls) (pt, pos) sc is;
   19.20  go: no [L,L,R] *)
   19.21 -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Prog (_ $ body)), 
   19.22 +"~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Prog (_ $ body)), 
   19.23  	    (ScrState (E,l,a,v,s,_), ctxt) ) = ((thy', srls), (pt, pos), sc, is);
   19.24  (*if*) l = [] = false;
   19.25  

    20.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml	Tue Jun 25 10:46:20 2019 +0200
    20.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml	Tue Jun 25 12:48:24 2019 +0200
    20.3 @@ -34,8 +34,8 @@
    20.4  	      val thy' = get_obj g_domID pt (par_pblobj pt p);
    20.5  	      val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
    20.6  		      val d = e_rls; (*FIXME.WN0108: canon.simplifier for domain is missing: generate from domID?*)
    20.7 -(*val Steps (is', ss as (m',f',pt',p',c')::_) = locate_gen (thy',srls) m  (pt,(p,p_)) (sc,d) is;*)
    20.8 -"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ctree * pos'), 
    20.9 +(*val Steps (is', ss as (m',f',pt',p',c')::_) = locate_input_tactic (thy',srls) m  (pt,(p,p_)) (sc,d) is;*)
   20.10 +"~~~~~ fun locate_input_tactic, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ctree * pos'), 
   20.11  	                   (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
   20.12                     ((thy',srls), m,  (pt,(p,p_)), (sc,d), is);
   20.13  val thy = assoc_thy thy';

    21.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml	Tue Jun 25 10:46:20 2019 +0200
    21.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml	Tue Jun 25 12:48:24 2019 +0200
    21.3 @@ -64,7 +64,7 @@
    21.4  "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
    21.5  val thy' = get_obj g_domID pt (par_pblobj pt p);
    21.6  val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
    21.7 -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ctree * pos'), (sc as Prog (h $ body)), 
    21.8 +"~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt,(p,_)):ctree * pos'), (sc as Prog (h $ body)), 
    21.9  	                               (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
   21.10  val ctxt = get_ctxt pt pos;
   21.11  val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";

    22.1 --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml	Tue Jun 25 10:46:20 2019 +0200
    22.2 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml	Tue Jun 25 12:48:24 2019 +0200
    22.3 @@ -46,7 +46,7 @@
    22.4  e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
    22.5  val thy' = get_obj g_domID pt (par_pblobj pt p);
    22.6  val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
    22.7 -val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is;
    22.8 +val (tac_,is,(t,_)) = determine_next_tactic (thy',srls) (pt,pos) sc is;
    22.9  ;tac_; (* = Check_Postcond' *)
   22.10  "~~~~~ fun nxt_solv, args:"; val ((Check_Postcond' (pI,_)), _, (pt, pos as (p,p_))) =
   22.11                                   (tac_, is, ptp);
   22.12 @@ -62,7 +62,7 @@
   22.13          val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_); 
   22.14          val thy' = get_obj g_domID pt pp;
   22.15          val thy = assoc_thy thy';
   22.16 -        val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc loc;
   22.17 +        val (_,_,(scval,scsaf)) = determine_next_tactic (thy',srls) (pt,(p,p_)) sc loc;
   22.18  ;pp = []; (*false*)
   22.19              val ppp = par_pblobj pt (lev_up p);
   22.20  	          val thy' = get_obj g_domID pt ppp;

    23.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml	Tue Jun 25 10:46:20 2019 +0200
    23.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml	Tue Jun 25 12:48:24 2019 +0200
    23.3 @@ -55,7 +55,7 @@
    23.4  "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
    23.5  val thy' = get_obj g_domID pt (par_pblobj pt p);
    23.6  val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
    23.7 -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), (sc as Prog (h $ body)),
    23.8 +"~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), (sc as Prog (h $ body)),
    23.9  (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
   23.10  val ctxt = get_ctxt pt pos
   23.11  val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";

    24.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml	Tue Jun 25 10:46:20 2019 +0200
    24.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml	Tue Jun 25 12:48:24 2019 +0200
    24.3 @@ -110,9 +110,9 @@
    24.4  (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = false  isabisac = ?*);
    24.5          val thy' = get_obj g_domID pt (par_pblobj pt p);
    24.6  	      val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
    24.7 -(*	    val (tac_, is, (t, _)) =*) next_tac (thy', srls) (pt, pos) sc is;
    24.8 +(*	    val (tac_, is, (t, _)) =*) determine_next_tactic (thy', srls) (pt, pos) sc is;
    24.9  ;
   24.10 -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Rule.Prog (_ $ body)), 
   24.11 +"~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Rule.Prog (_ $ body)), 
   24.12  	    (Selem.ScrState (E,l,a,v,s,_), ctxt)) = ((thy', srls), (pt, pos), sc, is);
   24.13  (*if*) l = [] (* = true *);
   24.14  appy thy ptp E [Celem.R] body NONE v;

    25.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml	Tue Jun 25 10:46:20 2019 +0200
    25.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml	Tue Jun 25 12:48:24 2019 +0200
    25.3 @@ -566,9 +566,9 @@
    25.4        val thy = assoc_thy thy';
    25.5        val d = e_rls;
    25.6      val Steps [(m',f',pt',p',c',s')] = 
    25.7 -	     locate_gen thy' m  (pt,(p,p_)) (sc,d) is;
    25.8 +	     locate_input_tactic thy' m  (pt,(p,p_)) (sc,d) is;
    25.9           val is' = get_istate pt' p';
   25.10 -	 next_tac thy' (pt'(*'*),p') sc is';  
   25.11 +	 determine_next_tactic thy' (pt'(*'*),p') sc is';  
   25.12  
   25.13  
   25.14  

    26.1 --- a/test/Tools/isac/Test_Isac.thy	Tue Jun 25 10:46:20 2019 +0200
    26.2 +++ b/test/Tools/isac/Test_Isac.thy	Tue Jun 25 12:48:24 2019 +0200
    26.3 @@ -93,7 +93,8 @@
    26.4                           in case of errors here consider ~~/./xtest-to-coding.sh      *)
    26.5    open Kernel;
    26.6    open Math_Engine;            CalcTreeTEST;
    26.7 -  open Lucin;                  appy;
    26.8 +  open Lucin;                  itms2args;
    26.9 +  open LucinNEW;               appy;
   26.10    open Inform;                 cas_input;
   26.11    open Rtools;                 trtas2str;
   26.12    open Chead;                  pt_extract;
   26.13 @@ -242,13 +243,13 @@
   26.14    ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml"
   26.15    ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml"
   26.16    ML \<open>"%%%%%%%%%%%%%%%%% end ADDTESTS %%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
   26.17 -ML \<open>
   26.18 -\<close> ML \<open>
   26.19 -\<close> ML \<open>
   26.20 -\<close>
   26.21    ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
   26.22    ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>
   26.23    ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
   26.24 +ML \<open>
   26.25 +\<close> ML \<open>
   26.26 +\<close> ML \<open>
   26.27 +\<close>
   26.28  
   26.29  section \<open>history of tests\<close>
   26.30  text \<open>