72 let |
72 let |
73 val dtss = argl2dtss argl |
73 val dtss = argl2dtss argl |
74 val (pI, pits, mI, mits, pre, ctxt) = cas_input_ spec dtss |
74 val (pI, pits, mI, mits, pre, ctxt) = cas_input_ spec dtss |
75 val spec = (dI, pI, mI) |
75 val spec = (dI, pI, mI) |
76 val (pt,_) = Ctree.cappend_problem Ctree.e_ctree [] (Istate_Def.empty, ContextC.empty) |
76 val (pt,_) = Ctree.cappend_problem Ctree.e_ctree [] (Istate_Def.empty, ContextC.empty) |
77 ([], Spec.empty_spec) ([], Spec.empty_spec, hdt, ctxt) |
77 ([], Spec.empty) ([], Spec.empty, hdt, ctxt) |
78 val pt = Ctree.update_spec pt [] spec |
78 val pt = Ctree.update_spec pt [] spec |
79 val pt = Ctree.update_pbl pt [] pits |
79 val pt = Ctree.update_pbl pt [] pits |
80 val pt = Ctree.update_met pt [] mits |
80 val pt = Ctree.update_met pt [] mits |
81 in |
81 in |
82 SOME (pt, (true, Pos.Met, hdt, mits, pre, spec) : Ctree.ocalhd) |
82 SOME (pt, (true, Pos.Met, hdt, mits, pre, spec) : Ctree.ocalhd) |
99 Pos.pos' * (*the position of the calc-head in the calc-tree*) |
99 Pos.pos' * (*the position of the calc-head in the calc-tree*) |
100 TermC.as_string * (*the headline*) |
100 TermC.as_string * (*the headline*) |
101 imodel * (*the model (without Find) of the calc-head*) |
101 imodel * (*the model (without Find) of the calc-head*) |
102 Pos.pos_ * (*model belongs to Pbl or Met*) |
102 Pos.pos_ * (*model belongs to Pbl or Met*) |
103 Spec.spec; (*specification: domID, pblID, metID*) |
103 Spec.spec; (*specification: domID, pblID, metID*) |
104 val e_icalhd = (Pos.e_pos', "", [Given [""]], Pos.Pbl, Spec.empty_spec) |
104 val e_icalhd = (Pos.e_pos', "", [Given [""]], Pos.Pbl, Spec.empty) |
105 |
105 |
106 fun is_casinput (hdf : TermC.as_string) ((fmz_, spec) : Selem.fmz) = |
106 fun is_casinput (hdf : TermC.as_string) ((fmz_, spec) : Selem.fmz) = |
107 hdf <> "" andalso fmz_ = [] andalso spec = Spec.empty_spec |
107 hdf <> "" andalso fmz_ = [] andalso spec = Spec.empty |
108 |
108 |
109 (* re-parse itms with a new thy and prepare for checking with ori list *) |
109 (* re-parse itms with a new thy and prepare for checking with ori list *) |
110 fun parsitm dI (itm as (i, v, _, f, Model.Cor ((d, ts), _))) = |
110 fun parsitm dI (itm as (i, v, _, f, Model.Cor ((d, ts), _))) = |
111 (let val t = Model.comp_dts (d, ts) |
111 (let val t = Model.comp_dts (d, ts) |
112 val _ = (UnparseC.term_in_thy dI t) |
112 val _ = (UnparseC.term_in_thy dI t) |