55 | f2str _ = raise ERROR "f2str: uncovered case in fun.def."; |
55 | f2str _ = raise ERROR "f2str: uncovered case in fun.def."; |
56 |
56 |
57 (* create a calc-tree *) |
57 (* create a calc-tree *) |
58 fun init_calc ctxt [(model, refs as (thy_id, _, _))] = |
58 fun init_calc ctxt [(model, refs as (thy_id, _, _))] = |
59 let |
59 let |
60 val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global |
60 (*old* )val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global |
61 val ((pt, p), tacis) = Step_Specify.nxt_specify_init_calc ctxt (model, refs) |
61 ( *new*)val thy = thy_id |> ThyC.get_theory_PIDE ctxt (*^^^^^^^^^^^^^^^^^^^^^^^^^ misleading*) |
|
62 val ((pt, p), tacis) = Step_Specify.nxt_specify_init_calc_PIDE thy (model, refs) |
62 val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis |
63 val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis |
63 val f = TESTg_form ctxt (pt,p) |
64 val f = TESTg_form ctxt (pt,p) |
64 in (p, []:NEW, f, tac, Celem.Sundef, pt) end |
65 in (p, []:NEW, f, tac, Celem.Sundef, pt) end |
65 | init_calc _ _ = raise ERROR "Tess_Code.init_calc: uncovered case" |
66 | init_calc _ _ = raise ERROR "Tess_Code.init_calc: uncovered case" |
66 |
67 |