1.1 --- a/src/Tools/isac/Interpret/appl.sml	Thu Apr 07 16:31:05 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Fri Apr 08 15:16:08 2011 +0200
     1.3 @@ -595,8 +595,8 @@
     1.4         then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
     1.5       else
     1.6         let val thy' = get_obj g_domID pt (par_pblobj pt p);
     1.7 -       in (case parse (assoc_thy thy') ct' of
     1.8 -	       SOME ct => Appl (Take' (term_of ct))
     1.9 +       in (case parseNEW (assoc_thy thy' |> thy2ctxt) ct' of
    1.10 +	       SOME ct => Appl (Take' ct)
    1.11  	     | NONE => Notappl ("syntax error in "^ct'))
    1.12         end
    1.13  
    1.14 @@ -699,7 +699,7 @@
    1.15                Frm => (get_obj g_form pt p , [])
    1.16  	    | Res => get_obj g_result pt p;
    1.17      (*val _= tracing("### applicable_in Check_elementwise: f= "^f);*)
    1.18 -    val vp = mk_set thy pt p f ((term_of o the o (parse thy)) pred);
    1.19 +    val vp = (thy2ctxt thy, pred) |-> parseNEW |> the |> mk_set thy pt p f;
    1.20      (*val (v,p)=vp;val _=tracing("### applicable_in Check_elementwise: vp= "^
    1.21  			       pair2str(term2str v,term2str p))*)
    1.22    in case f of
    1.23 @@ -763,7 +763,7 @@
    1.24  	    (*val _= (term_of o the o (parse thy)) f';*)
    1.25  	    (*val _= tracing"### applicable_in: solve_equation_dummy";*)
    1.26  	  in if id' <> "subproblem_equation_dummy" then Notappl "no subproblem"
    1.27 -	     else if is_expliceq ((term_of o the o (parse thy)) f')
    1.28 +	     else if (thy2ctxt thy, f') |-> parseNEW |> the |> is_expliceq
    1.29  		      then Appl (Tac_ (thy, term2str f, id, "[" ^ f' ^ "]"))
    1.30  		  else error ("applicable_in: f= " ^ f') end
    1.31      | _ => Appl (Tac_ (thy, term2str f, id, term2str f)) end

     2.1 --- a/src/Tools/isac/Interpret/calchead.sml	Thu Apr 07 16:31:05 2011 +0200
     2.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Fri Apr 08 15:16:08 2011 +0200
     2.3 @@ -275,19 +275,15 @@
     2.4  (*.to an input (d,ts) find the according ori and insert the ts.*)
     2.5  (*WN.11.03: + dont take first inter<>[]*)
     2.6  fun seek_oridts ctxt sel (d,ts) [] =
     2.7 -    ("seek_oridts: input ('" ^ (Print_Mode.setmp [] (Syntax.string_of_term ctxt)
     2.8 -                             (comp_dts (d,ts))) ^
     2.9 -     "') not found in oris (typed)", (0, [], sel, d, ts) : ori,
    2.10 -     [])
    2.11 -  | seek_oridts ctxt sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
    2.12 -    if sel = sel' andalso d=d' andalso (inter op = ts ts') <> []
    2.13 -    then if sel = sel'
    2.14 -	 then ("", 
    2.15 -               (id,vat,sel,d, inter op = ts ts'):ori, 
    2.16 -               ts')
    2.17 -       else ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) (comp_dts (d,ts)))
    2.18 -         ^ " not for " ^ sel, e_ori_, [])
    2.19 -    else seek_oridts ctxt sel (d,ts) oris;
    2.20 +    ("seek_oridts: input ('" ^
    2.21 +        (Print_Mode.setmp [] (Syntax.string_of_term ctxt) (comp_dts (d,ts))) ^
    2.22 +        "') not found in oris (typed)",
    2.23 +      (0, [], sel, d, ts),
    2.24 +      [])
    2.25 +  | seek_oridts ctxt sel (d,ts) ((id, vat, sel', d', ts')::oris) =
    2.26 +    if sel = sel' andalso d = d' andalso (inter op = ts ts') <> [] then
    2.27 +      ("", (id, vat, sel, d, inter op = ts ts'), ts') else
    2.28 +      seek_oridts ctxt sel (d, ts) oris;
    2.29  
    2.30  (*.to an input (_,ts) find the according ori and insert the ts.*)
    2.31  fun seek_orits ctxt sel ts [] = 
    2.32 @@ -774,13 +770,13 @@
    2.33  (** add an item to the model; check wrt. oris and pbt **)
    2.34  (* in contrary to oris<>[] below, this part handles user-input
    2.35     extremely acceptive, i.e. accept input instead error-msg *)
    2.36 -fun appl_add ctxt sel [] ppc pbt t =
    2.37 +fun appl_add ctxt sel [] ppc pbt ct =
    2.38        let
    2.39          val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl);
    2.40 -      in case parse (ProofContext.theory_of ctxt) t of
    2.41 -          NONE => Add (i, [], false, sel, Syn t)
    2.42 -        | SOME t' =>
    2.43 -          let val (d, ts) = split_dts (term_of t');
    2.44 +      in case parseNEW ctxt ct of
    2.45 +          NONE => Add (i, [], false, sel, Syn ct)
    2.46 +        | SOME t =>
    2.47 +          let val (d, ts) = split_dts t;
    2.48            in if d = e_term then
    2.49              Add (i, [], false, sel, Mis (dsc_unknown, hd ts)) else
    2.50              (case find_first (eq1 d) pbt of
    2.51 @@ -811,8 +807,8 @@
    2.52          | SOME t => case is_known ctxt sel oris (term_of t) of
    2.53              ("", ori', all) => (case is_notyet_input ctxt ppc all ori' pbt of
    2.54                ("", itm) => Add itm
    2.55 -              | (msg, _) => Err msg)
    2.56 -          | (msg, _, _) => Err msg;
    2.57 +              | (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg))
    2.58 +          | (msg, _, _) => Err ("[error] appl_add: is_known: " ^ msg);
    2.59  (* 
    2.60  > val (msg,itm) = is_notyet_input thy ppc all ori';
    2.61  val itm = (12,[3],false,"#Relate",Cor (Const #,[#,#])) : itm

     3.1 --- a/src/Tools/isac/Interpret/inform.sml	Thu Apr 07 16:31:05 2011 +0200
     3.2 +++ b/src/Tools/isac/Interpret/inform.sml	Fri Apr 08 15:16:08 2011 +0200
     3.3 @@ -280,9 +280,9 @@
     3.4  fun appl_add' dI oris ppc pbt (sel, ct) = 
     3.5      let 
     3.6        val ctxt = assoc_thy dI |> thy2ctxt;
     3.7 -    in case parse (ProofContext.theory_of ctxt) ct of
     3.8 +    in case parseNEW ctxt ct of
     3.9  	   NONE => (0,[],false,sel, Syn ct):itm
    3.10 -	 | SOME ct => (case is_known ctxt sel oris (term_of ct) of
    3.11 +	 | SOME t => (case is_known ctxt sel oris t of
    3.12           ("", ori', all) =>
    3.13             (case is_notyet_input ctxt ppc all ori' pbt of
    3.14  	         ("",itm)  => itm

     4.1 --- a/src/Tools/isac/Interpret/mstools.sml	Thu Apr 07 16:31:05 2011 +0200
     4.2 +++ b/src/Tools/isac/Interpret/mstools.sml	Fri Apr 08 15:16:08 2011 +0200
     4.3 @@ -159,8 +159,9 @@
     4.4  structure SpecifyTools : SPECIFY_TOOLS =
     4.5  struct
     4.6  (*----------------------------------------------------------*)
     4.7 -val e_listReal = (term_of o the o (parse (Thy_Info.get_theory "Script"))) "[]::(real list)";
     4.8 -val e_listBool = (term_of o the o (parse (Thy_Info.get_theory "Script"))) "[]::(bool list)";
     4.9 +val script_parse = the o (Thy_Info.get_theory "Script" |> thy2ctxt |> parseNEW);
    4.10 +val e_listReal = script_parse "[]::(real list)";
    4.11 +val e_listBool = script_parse "[]::(bool list)";
    4.12  
    4.13  (*.take list-term apart w.r.t. handling elementwise input.*)
    4.14  fun take_apart t =

     5.1 --- a/src/Tools/isac/Interpret/ptyps.sml	Thu Apr 07 16:31:05 2011 +0200
     5.2 +++ b/src/Tools/isac/Interpret/ptyps.sml	Fri Apr 08 15:16:08 2011 +0200
     5.3 @@ -274,15 +274,12 @@
     5.4     val (thy,pbt) = (assoc_thy dI',(#ppc o get_pbt) pI');
     5.5     val (fmz, thy, pbt) = (fmz, thy, ((#ppc o get_pbt) pI));
     5.6     *)
     5.7 +
     5.8  fun prep_ori [] _ _ = ([], e_ctxt)
     5.9    | prep_ori fmz thy pbt =
    5.10        let
    5.11 -        val ctxt = ProofContext.init_global thy
    5.12 -          |> fold declare_constraints fmz;
    5.13 -        fun checked_parseNEW t = case parseNEW ctxt t of
    5.14 -              NONE => error ("prep_ori: SYNTAX ERROR in " ^ t)
    5.15 -            | SOME t' => t';
    5.16 -        val ori = map (add_field thy pbt o split_dts o checked_parseNEW) fmz
    5.17 +        val ctxt = ProofContext.init_global thy |> fold declare_constraints fmz;
    5.18 +        val ori = map (add_field thy pbt o split_dts o the o parseNEW ctxt) fmz
    5.19            |> add_variants;
    5.20          val maxv = map fst ori |> max;
    5.21          val maxv = if maxv = 0 then 1 else maxv;
    5.22 @@ -292,7 +289,6 @@
    5.23            |> map flattup;
    5.24        in (oris, ctxt) end;
    5.25  
    5.26 -
    5.27  (*-----------------------------------------^^^-(4) aus modspec.sml 23.3.02*)
    5.28  
    5.29  (*.the pattern for an item of a problems model or a methods guard.*)
    5.30 @@ -456,7 +452,7 @@
    5.31  	else del k (ptyps @ [Ptyp (k', [p], ps)]) pys;
    5.32  in del k [] ptyps end;
    5.33  
    5.34 -fun insrt d pbt [k] [] = [Ptyp (k, [pbt],[])]
    5.35 +fun insrt _ pbt [k] [] = [Ptyp (k, [pbt],[])]
    5.36  			 
    5.37    | insrt d pbt [k] ((Ptyp (k', [p], ps))::pys) =
    5.38  ((*tracing("### insert 1: ks = "^(strs2str [k])^"    k'= "^k');*)

     6.1 --- a/src/Tools/isac/Knowledge/Equation.thy	Thu Apr 07 16:31:05 2011 +0200
     6.2 +++ b/src/Tools/isac/Knowledge/Equation.thy	Fri Apr 08 15:16:08 2011 +0200
     6.3 @@ -29,6 +29,7 @@
     6.4  
     6.5  ML {*
     6.6  val thy = @{theory};
     6.7 +val ctxt = thy2ctxt thy;
     6.8  
     6.9  val univariate_equation_prls = 
    6.10      append_rls "univariate_equation_prls" e_rls 
    6.11 @@ -68,10 +69,10 @@
    6.12  				  "solveTest (x+1=2, x)");
    6.13     *)
    6.14  fun argl2dtss [Const ("Pair", _) $ eq $ bdv] =
    6.15 -    [((term_of o the o (parse thy)) "equality", [eq]),
    6.16 -     ((term_of o the o (parse thy)) "solveFor", [bdv]),
    6.17 -     ((term_of o the o (parse thy)) "solutions", 
    6.18 -      [(term_of o the o (parse thy)) "L"])
    6.19 +    [((the o (parseNEW ctxt)) "equality", [eq]),
    6.20 +     ((the o (parseNEW ctxt)) "solveFor", [bdv]),
    6.21 +     ((the o (parseNEW ctxt)) "solutions", 
    6.22 +      [(the o (parseNEW ctxt)) "L"])
    6.23       ]
    6.24    | argl2dtss _ = error "Equation.ML: wrong argument for argl2dtss";
    6.25  

     7.1 --- a/test/Tools/isac/Interpret/mathengine.sml	Thu Apr 07 16:31:05 2011 +0200
     7.2 +++ b/test/Tools/isac/Interpret/mathengine.sml	Fri Apr 08 15:16:08 2011 +0200
     7.3 @@ -35,8 +35,8 @@
     7.4  "----- in  prep_ori";
     7.5  val ctxt = ProofContext.init_global thy;
     7.6  
     7.7 -    val ctopts = map (parse thy) fmz;
     7.8 -    val dts = map (split_dts o term_of o the) ctopts;
     7.9 +val ctopts = map (parseNEW ctxt) fmz;
    7.10 +val dts = map (split_dts o the) ctopts;
    7.11  (*split_dts:
    7.12  (term * term list) list
    7.13          formulas: e.g. ((1+2)*4/3)^^^2

     8.1 --- a/test/Tools/isac/Test_Some.thy	Thu Apr 07 16:31:05 2011 +0200
     8.2 +++ b/test/Tools/isac/Test_Some.thy	Fri Apr 08 15:16:08 2011 +0200
     8.3 @@ -13,6 +13,13 @@
     8.4  parse;
     8.5  parseNEW;
     8.6  update_loc';
     8.7 +
     8.8 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
     8.9 +val (_, ctxt) = prep_ori fmz @{theory} [];
    8.10 +val to_parse = "equality (x + 1 = 2)"; 
    8.11 +parseNEW ctxt to_parse |> the;
    8.12 +parse @{theory} to_parse |> the |> term_of;
    8.13 +parseNEW ctxt "x";
    8.14  *}
    8.15  
    8.16