1.1 --- a/src/Tools/isac/Frontend/interface.sml	Sat Oct 09 16:20:02 2010 +0200
     1.2 +++ b/src/Tools/isac/Frontend/interface.sml	Sun Oct 10 14:15:43 2010 +0200
     1.3 @@ -60,15 +60,15 @@
     1.4  struct
     1.5  (*------------------------------------------------------------------*)
     1.6  
     1.7 -(*.encode "Isabelle"-strings as seen by the user to the
     1.8 +(* encode "Isabelle"-strings as seen by the user to the
     1.9     format accepted by Isabelle.
    1.10     encode "^" ---> "^^^"; see Knowledge/Atools.thy;
    1.11     called for each cterm', icalhd, fmz in this interface;
    1.12 -   + see "fun decode" in xmlsrc/mathml.sml.*)
    1.13 -fun encode (str:cterm') = 
    1.14 +   + see "fun decode" in xmlsrc/mathml.sml *)
    1.15 +fun encode (str : cterm') = 
    1.16      let fun enc [] = []
    1.17 -	  | enc ("^"::cs) = "^"::"^"::"^"::(enc cs)
    1.18 -	  | enc (c::cs) = c::(enc cs)
    1.19 +	  | enc ("^" :: cs) = "^" :: "^" :: "^" :: (enc cs)
    1.20 +	  | enc (c :: cs) = c :: (enc cs)
    1.21      in (implode o enc o explode) str:cterm' end;
    1.22  fun encode_imodel (imodel:imodel) =
    1.23      let fun enc (Given ifos) = Given (map encode ifos)
    1.24 @@ -77,7 +77,7 @@
    1.25      in map enc imodel:imodel end;
    1.26  fun encode_icalhd ((pos', headl, imodel, pos_, spec):icalhd) =
    1.27      (pos', encode headl, encode_imodel imodel, pos_, spec):icalhd;
    1.28 -fun encode_fmz ((ifos, spec):fmz) = (map encode ifos, spec):fmz;
    1.29 +fun encode_fmz ((ifos, spec) : fmz) = (map encode ifos, spec) : fmz;
    1.30  
    1.31  
    1.32  (***. CalcTree .***)
    1.33 @@ -98,21 +98,7 @@
    1.34  
    1.35  (*.create a calc-tree; for calls from java: thus ^^^ decoded to ^;
    1.36     compare "fun CalcTreeTEST" which does NOT decode.*)
    1.37 -fun CalcTree
    1.38 -	[(fmz, sp):fmz] (*for several variants lateron*) =
    1.39 -(* val[(fmz,sp):fmz]=[(["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
    1.40 -             "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
    1.41 -             "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
    1.42 -             "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
    1.43 -             "boundVariable a","boundVariable b","boundVariable alpha",
    1.44 -             "interval {x::real. 0 <= x & x <= 2*r}",
    1.45 -             "interval {x::real. 0 <= x & x <= 2*r}",
    1.46 -             "interval {x::real. 0 <= x & x <= pi}",
    1.47 -             "errorBound (eps=(0::real))"],
    1.48 -       ("DiffApp.thy", ["maximum_of","function"],
    1.49 -            ["DiffApp","max_by_calculus"]))];
    1.50 -
    1.51 -   *)
    1.52 +fun CalcTree [(fmz, sp) : fmz] (*for several variants lateron*) =
    1.53  	(let val cs = nxt_specify_init_calc (encode_fmz (fmz, sp))
    1.54  	     (*FIXME.WN.8.03: error-handling missing*)
    1.55  	     val cI = add_calc cs
    1.56 @@ -586,16 +572,8 @@
    1.57  
    1.58  
    1.59  
    1.60 -(*.replace a formula with_in_ a calculation;
    1.61 -   this situation applies for initial CAS-commands, too.*)
    1.62 -(* val (cI, ifo) = (2, "-1 + x = 0");
    1.63 -   val (cI, ifo) = (1, "-1 + x = 0");
    1.64 -   val (cI, ifo) = (1, "x - 1 = 0");
    1.65 -   val (cI, ifo) = (1, "x = 1");
    1.66 -   val (cI, ifo) = (1, "solve(x+1=2,x)");
    1.67 -   val (cI, ifo) = (1, "Simplify (2*a + 3*a)");
    1.68 -   val (cI, ifo) = (1, "Diff (x^2 + x + 1, x)");
    1.69 -   *)
    1.70 +(* replace a formula with_in_ a calculation;
    1.71 +   this situation applies for initial CAS-commands, too *)
    1.72  fun replaceFormula cI (ifo:cterm') =
    1.73      (let val ((pt, _), _) = get_calc cI
    1.74  	val p = get_pos cI 1