1.1 --- a/src/Tools/isac/Interpret/inform.sml Mon Mar 21 00:32:53 2011 +0100
1.2 +++ b/src/Tools/isac/Interpret/inform.sml Mon Apr 04 11:05:07 2011 +0200
1.3 @@ -226,7 +226,7 @@
1.4 fun parsitm dI (itm as (i,v,b,f, Cor ((d,ts),_)):itm) =
1.5 (* val itm as (i,v,b,f, Cor ((d,ts),_)) = hd probl;
1.6 *)
1.7 - (let val t = (comp_dts (Isac "delay")) (d,ts);
1.8 + (let val t = comp_dts (d,ts);
1.9 val s = Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt dI)) t;
1.10 (*this ^ should raise the exn on unability of re-parsing dts*)
1.11 in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
1.12 @@ -237,12 +237,12 @@
1.13 (let val t = (term_of o the o (parse dI)) str
1.14 in (i,v,b,f, Par str) end handle _ => (i,v,b,f, Syn str))
1.15 | parsitm dI (itm as (i,v,_,f, Inc ((d,ts),_))) =
1.16 - (let val t = (comp_dts (Isac "delay")) (d,ts);
1.17 + (let val t = comp_dts (d,ts);
1.18 val s = Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt dI)) t;
1.19 (*this ^ should raise the exn on unability of re-parsing dts*)
1.20 in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
1.21 | parsitm dI (itm as (i,v,_,f, Sup (d,ts))) =
1.22 - (let val t = (comp_dts (Isac"delay" )) (d,ts);
1.23 + (let val t = comp_dts (d,ts);
1.24 val s = Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt dI)) t;
1.25 (*this ^ should raise the exn on unability of re-parsing dts*)
1.26 in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
1.27 @@ -279,27 +279,17 @@
1.28 *)
1.29 fun appl_add' dI oris ppc pbt (sel, ct) =
1.30 let
1.31 - val thy = assoc_thy dI;
1.32 - in case parse thy ct of
1.33 + val ctxt = assoc_thy dI |> thy2ctxt;
1.34 + in case parseNEW ctxt ct of
1.35 NONE => (0,[],false,sel, Syn ct):itm
1.36 - | SOME ct => (* val SOME ct = parse thy ct;
1.37 - *)
1.38 - (case is_known thy sel oris (term_of ct) of
1.39 - (* val ("",ori'(*ts='ct'*), all) = is_known thy sel oris (term_of ct);
1.40 - *)
1.41 - ("",ori'(*ts='ct'*), all) =>
1.42 - (case is_notyet_input thy ppc all ori' pbt of
1.43 - (* val ("",itm) = is_notyet_input thy ppc all ori' pbt;
1.44 - *)
1.45 - ("",itm) => itm
1.46 - (* val (msg,xx) = is_notyet_input thy ppc all ori' pbt;
1.47 - *)
1.48 - | (msg,_) => error ("appl_add': "^msg))
1.49 - (* val (msg,(_,_,_,d,ts),all) = is_known thy sel oris (term_of ct);
1.50 - *)
1.51 - | (msg,(i,v,_,d,ts),_) =>
1.52 - if is_e_ts ts then (i,v,false, sel, Inc ((d,ts),(e_term,[])))
1.53 - else (i,v,false,sel, Sup (d,ts)))
1.54 + | SOME t => (case is_known ctxt sel oris t of
1.55 + ("", ori', all) =>
1.56 + (case is_notyet_input ctxt ppc all ori' pbt of
1.57 + ("",itm) => itm
1.58 + | (msg,_) => error ("appl_add': " ^ msg))
1.59 + | (_, (i, v, _, d, ts), _) => if is_e_ts ts then
1.60 + (i, v, false, sel, Inc ((d, ts), (e_term, []))) else
1.61 + (i, v, false, sel, Sup (d, ts)))
1.62 end;
1.63
1.64 (*.generate preliminary itm_ from a strin (with field "#Given" etc.).*)
1.65 @@ -313,7 +303,7 @@
1.66 | SOME ct =>
1.67 (* val SOME ct = parse thy str;
1.68 *)
1.69 - let val (d,ts) = ((split_dts thy) o term_of) ct
1.70 + let val (d,ts) = (split_dts o term_of) ct
1.71 val popt = find_first (eq7 (f,d)) pbt
1.72 in case popt of
1.73 NONE => ([1](*??*), true(*??*), f, Sup (d,ts))
1.74 @@ -453,7 +443,7 @@
1.75 let val pbt = (#ppc o get_pbt) pI
1.76 val dI' = #1 (some_spec ospec spec)
1.77 val oris = if pI = #2 ospec then oris
1.78 - else prep_ori fmz_(assoc_thy"Isac") pbt;
1.79 + else prep_ori fmz_(assoc_thy"Isac") pbt |> #1;
1.80 in (Pbl, appl_adds dI' oris probl pbt
1.81 (map itms2fstr probl), meth) end else
1.82 if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)