21 = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"]; |
21 = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"]; |
22 |
22 |
23 Test_Code.init_calc @{context} [(model, refs)]; |
23 Test_Code.init_calc @{context} [(model, refs)]; |
24 "~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))]) |
24 "~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))]) |
25 = (@{context}, [(model, refs)]); |
25 = (@{context}, [(model, refs)]); |
26 val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global |
26 (*old* )val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global |
27 val ((pt''', p'''), tacis''') = (* keep for continuation *) |
27 ( *new*)val thy = thy_id |> ThyC.get_theory_PIDE ctxt (*^^^^^^^^^^^^^^^^^^^^^^^^^ misleading*) |
28 |
28 |
29 Step_Specify.nxt_specify_init_calc ctxt (model, refs); |
29 (**)val return_nxt_specify_init_calc_PIDE =(**) |
|
30 Step_Specify.nxt_specify_init_calc_PIDE thy (model, refs); |
30 "~~~~~ fun nxt_specify_init_calc , args:"; val (ctxt, (model, (dI, pI, mI))) = (ctxt, (model, refs)); |
31 "~~~~~ fun nxt_specify_init_calc , args:"; val (ctxt, (model, (dI, pI, mI))) = (ctxt, (model, refs)); |
31 |
32 |
32 Step_Specify.initialise ctxt (model, refs); |
33 Step_Specify.initialise_PIDE thy (model, refs); |
33 "~~~~~ fun initialise , args:"; val (ctxt, (fmz, (dI, pI, mI))) = (ctxt, (model, refs)); |
34 "~~~~~ fun initialise , args:"; val (ctxt, (fmz, (dI, pI, mI))) = (ctxt, (model, refs)); |
34 val thy = ThyC.get_theory_PIDE ctxt dI |
35 (*old* )val thy = ThyC.get_theory_PIDE ctxt dI( *old*) |
35 val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise *) |
36 val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise.refs *) |
36 val (pI, (pors, pctxt), mI) = |
37 val (pI, (pors, pctxt), mI) = |
37 if mI = ["no_met"] |
38 if mI = ["no_met"] |
38 then raise error "else not covered by test" |
39 then raise error "else not covered by test" |
39 else |
40 else |
40 let |
41 let |
41 val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*) |
42 (*old* ) val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*) |
42 val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*) |
43 (*old*) val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*) |
43 in (pI, (pors, pctxt), mI) end; |
44 (*old*) in (pI, (pors, pctxt), mI) end; |
|
45 ( *new*) val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz; |
|
46 in (pI, (pors, pctxt), mI) end; |
44 |
47 |
|
48 (*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term pctxt "r"; |
|
49 (*+*)val Free ("u", Type ("Real.real", [])) = Syntax.read_term pctxt "u"; |
45 (*-------------------- stop step into Step_Specify.nxt_specify_init_calc ---------------------*) |
50 (*-------------------- stop step into Step_Specify.nxt_specify_init_calc ---------------------*) |
|
51 |
|
52 val ((pt, p), tacis) = return_nxt_specify_init_calc_PIDE(* kept for continuation *); |
46 "~~~~~ continue fun init_calc , args:"; val ((pt, p), tacis) |
53 "~~~~~ continue fun init_calc , args:"; val ((pt, p), tacis) |
47 = ((pt''', p'''), tacis'''); |
54 = ((pt, p), tacis); |
48 val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis; |
55 val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis; |
49 |
56 |
50 Test_Code.TESTg_form ctxt (pt,p); |
57 Test_Code.TESTg_form ctxt (pt,p); |
51 "~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt,p)); |
58 "~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt,p)); |
52 val (form, _, _) = ME_Misc.pt_extract ctxt ptp; |
59 val (form, _, _) = ME_Misc.pt_extract ctxt ptp; |