1.1 --- a/src/Tools/isac/Frontend/interface.sml	Sat May 30 11:56:59 2015 +0200
     1.2 +++ b/src/Tools/isac/Frontend/interface.sml	Sat May 30 12:16:16 2015 +0200
     1.3 @@ -412,7 +412,7 @@
     1.4  	                  autocalculateOK2xml cI pold (if null c then pold else last_elem c) p
     1.5  		  	            end)
     1.6  	       end
     1.7 -      )handle _ => sysERROR2xmlTODO cI "setContext: thy_ ???")
     1.8 +      ) handle _ => sysERROR2xmlTODO cI "setContext: thy_ ???")
     1.9     | "pbl_" =>
    1.10  	     ((let
    1.11           val pI = guh2kestoreID guh
    1.12 @@ -717,44 +717,40 @@
    1.13    string contains the thy, thus it is unique as thmID, rlsID for this thy;
    1.14    take the substitution from the istate of the formula *)
    1.15  fun checkContext (cI:calcID) (pos:pos' as (p,p_)) (guh:guh) =
    1.16 -    (case (implode o (take_fromto 1 4) o Symbol.explode) guh of
    1.17 -	 "thy_" =>
    1.18 -	 if member op = [Pbl,Met] p_
    1.19 -         then message2xml cI "thy-context not to calchead"
    1.20 -	 else if pos = ([],Res) then message2xml cI "no thy-context at result"
    1.21 -	 else if no_thycontext guh then message2xml cI ("no thy-context for '"^
    1.22 -							guh ^ "'")
    1.23 -	 else let val (ptp as (pt,_),_) = get_calc cI
    1.24 -		  val is = get_istate pt pos
    1.25 -		  val subs = subs_from is "dummy" guh
    1.26 -		  val tac = guh2rewtac guh subs
    1.27 +  case (implode o (take_fromto 1 4) o Symbol.explode) guh of
    1.28 +	  "thy_" =>
    1.29 +	    if member op = [Pbl,Met] p_
    1.30 +      then message2xml cI "thy-context not to calchead"
    1.31 +      else if pos = ([],Res) then message2xml cI "no thy-context at result"
    1.32 +      else if no_thycontext guh then message2xml cI ("no thy-context for '" ^ guh ^ "'")
    1.33 +      else 
    1.34 +        ((let 
    1.35 +          val (ptp as (pt,_),_) = get_calc cI
    1.36 +    		  val is = get_istate pt pos
    1.37 +    		  val subs = subs_from is "dummy" guh
    1.38 +    		  val tac = guh2rewtac guh subs
    1.39  	      in contextthyOK2xml cI (context_thy (pt, pos) tac) end
    1.40 +        ) handle _ => sysERROR2xml cI "error in kernel")
    1.41 +    (*.match the model of a problem at pos p
    1.42 +      with the model-pattern of the problem with pblID.*)
    1.43 +  | "pbl_" =>
    1.44 +	    ((let 
    1.45 +	      val ((pt,_),_) = get_calc cI
    1.46 +  	    val pp = par_pblobj pt p
    1.47 +  	    val keID = guh2kestoreID guh
    1.48 +  	    val chd = context_pbl keID pt pp
    1.49 +	    in matchpbl2xml cI chd end
    1.50 +      ) handle _ => sysERROR2xml cI "error in kernel")
    1.51 +   | "met_" =>
    1.52 +	     ((let 
    1.53 +	       val ((pt,_),_) = get_calc cI
    1.54 +	       val pp = par_pblobj pt p
    1.55 +	       val keID = guh2kestoreID guh
    1.56 +	       val chd = context_met keID pt pp
    1.57 +	     in matchmet2xml cI chd end
    1.58 +      ) handle _ => sysERROR2xml cI "error in kernel")
    1.59 +   | str => message2xml cI ("checkContext: str = " ^ str)
    1.60  
    1.61 -       (*.match the model of a problem at pos p
    1.62 -          with the model-pattern of the problem with pblID.*)
    1.63 -(* val (cI, pos:pos' as (p,p_), guh) =
    1.64 -       (1, p, kestoreID2guh Pbl_ ["univariate","equation"]);
    1.65 -   val (cI, pos:pos' as (p,p_), guh) =
    1.66 -       (1, ([],Pbl), kestoreID2guh Pbl_ ["univariate","equation"]);
    1.67 -   val (cI, pos:pos' as (p,p_), guh) =
    1.68 -       (1, ([],Pbl), "pbl_equ_univ");
    1.69 -   *)
    1.70 -       | "pbl_" =>
    1.71 -	 let val ((pt,_),_) = get_calc cI
    1.72 -	     val pp = par_pblobj pt p
    1.73 -	     val keID = guh2kestoreID guh
    1.74 -	     val chd = context_pbl keID pt pp
    1.75 -	 in matchpbl2xml cI chd end
    1.76 -(* val (cI, pos:pos' as (p,p_), guh) =
    1.77 -       (1, ([],Pbl), kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]);
    1.78 -   *)
    1.79 -       | "met_" =>
    1.80 -	 let val ((pt,_),_) = get_calc cI
    1.81 -	     val pp = par_pblobj pt p
    1.82 -	     val keID = guh2kestoreID guh
    1.83 -	     val chd = context_met keID pt pp
    1.84 -	 in matchmet2xml cI chd end)
    1.85 -    handle _ => sysERROR2xml cI "error in kernel";
    1.86  
    1.87  (* for an errpatID find "(fillpatID, fillform)" list
    1.88    which dedicated to this errpat and which is applicable at current formula*)