1.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml	Wed Jan 11 11:38:01 2023 +0100
     1.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml	Wed Jan 25 15:52:33 2023 +0100
     1.3 @@ -23,28 +23,35 @@
     1.4   Test_Code.init_calc @{context} [(model, refs)];
     1.5  "~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))])
     1.6    = (@{context}, [(model, refs)]);
     1.7 -    val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global
     1.8 -    val ((pt''', p'''), tacis''') = (* keep for continuation *)
     1.9 +(*old* )val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global
    1.10 +( *new*)val thy = thy_id |> ThyC.get_theory_PIDE ctxt  (*^^^^^^^^^^^^^^^^^^^^^^^^^ misleading*)
    1.11  
    1.12 -Step_Specify.nxt_specify_init_calc ctxt (model, refs);
    1.13 +(**)val return_nxt_specify_init_calc_PIDE =(**)
    1.14 +Step_Specify.nxt_specify_init_calc_PIDE thy (model, refs);
    1.15  "~~~~~ fun nxt_specify_init_calc , args:"; val (ctxt, (model, (dI, pI, mI))) = (ctxt, (model, refs));
    1.16  
    1.17 -Step_Specify.initialise ctxt (model, refs);
    1.18 +Step_Specify.initialise_PIDE thy (model, refs);
    1.19  "~~~~~ fun initialise , args:"; val (ctxt, (fmz, (dI, pI, mI))) = (ctxt, (model, refs));
    1.20 -	    val thy = ThyC.get_theory_PIDE ctxt dI
    1.21 -	    val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise *)
    1.22 +(*old* )val thy = ThyC.get_theory_PIDE ctxt dI( *old*)
    1.23 +	    val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise.refs *)
    1.24  	    val (pI, (pors, pctxt), mI) = 
    1.25 -	      if mI = ["no_met"] 
    1.26 -	      then raise error "else not covered by test"
    1.27 -	      else
    1.28 -	        let
    1.29 -	          val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
    1.30 -            val pctxt = ContextC.initialise' thy fmz;                (*..DUPLICATE ermC.parseNEW'*)
    1.31 -	        in (pI, (pors, pctxt), mI) end;
    1.32 +        if mI = ["no_met"] 
    1.33 +        then raise error "else not covered by test"
    1.34 +        else
    1.35 +          let
    1.36 +(*old* )     val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
    1.37 +(*old*)     val pctxt = ContextC.initialise' thy fmz;                (*..DUPLICATE ermC.parseNEW'*)
    1.38 +(*old*)   in (pI, (pors, pctxt), mI) end;
    1.39 +( *new*)     val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz;
    1.40 +          in (pI, (pors, pctxt), mI) end;
    1.41  
    1.42 +(*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term pctxt "r";
    1.43 +(*+*)val Free ("u", Type ("Real.real", [])) = Syntax.read_term pctxt "u";
    1.44  (*-------------------- stop step into Step_Specify.nxt_specify_init_calc ---------------------*)
    1.45 +
    1.46 +val ((pt, p), tacis) = return_nxt_specify_init_calc_PIDE(* kept for continuation *);
    1.47  "~~~~~ continue fun init_calc , args:"; val ((pt, p), tacis)
    1.48 -  = ((pt''', p'''), tacis''');
    1.49 +  = ((pt, p), tacis);
    1.50  	  val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis;
    1.51  
    1.52   Test_Code.TESTg_form ctxt (pt,p);