1.1 --- a/src/Tools/isac/Frontend/interface.sml	Tue Nov 22 10:42:21 2016 +0100
     1.2 +++ b/src/Tools/isac/Frontend/interface.sml	Thu Nov 24 14:33:42 2016 +0100
     1.3 @@ -31,7 +31,7 @@
     1.4      val Iterator : calcID -> XML.tree
     1.5      val IteratorTEST : calcID -> iterID
     1.6      val modelProblem : calcID -> XML.tree
     1.7 -    val modifyCalcHead : calcID -> icalhd -> XML.tree
     1.8 +    val modifyCalcHead : calcID -> Inform.icalhd -> XML.tree
     1.9      val moveActiveCalcHead : calcID -> XML.tree
    1.10      val moveActiveDown : calcID -> XML.tree
    1.11      val moveActiveFormula : calcID -> pos' -> XML.tree
    1.12 @@ -70,13 +70,13 @@
    1.13     encode "^" ---> "^^^"; see Knowledge/Atools.thy;
    1.14     called for each cterm', icalhd, fmz in this interface;
    1.15     + see "fun en/decode" in xmlsrc/mathml.sml *)
    1.16 -fun encode_imodel (imodel:imodel) =
    1.17 -  let fun enc (Given ifos) = Given (map encode ifos)
    1.18 -	| enc (Find ifos) = Find (map encode ifos)
    1.19 -	| enc (Relate ifos) = Relate (map encode ifos)
    1.20 -  in map enc imodel:imodel end;
    1.21 -fun encode_icalhd ((pos', headl, imodel, pos_, spec):icalhd) =
    1.22 -  (pos', encode headl, encode_imodel imodel, pos_, spec):icalhd;
    1.23 +fun encode_imodel (imodel : Inform.imodel) =
    1.24 +  let fun enc (Inform.Given ifos) = Inform.Given (map encode ifos)
    1.25 +	| enc (Inform.Find ifos) = Inform.Find (map encode ifos)
    1.26 +	| enc (Inform.Relate ifos) = Inform.Relate (map encode ifos)
    1.27 +  in map enc imodel:Inform.imodel end;
    1.28 +fun encode_icalhd ((pos', headl, imodel, pos_, spec) : Inform.icalhd) =
    1.29 +  (pos', encode headl, encode_imodel imodel, pos_, spec) : Inform.icalhd;
    1.30  fun encode_fmz ((ifos, spec) : fmz) = (map encode ifos, spec) : fmz;
    1.31  
    1.32  
    1.33 @@ -162,7 +162,7 @@
    1.34    	  let
    1.35    	    val _= upd_tacis cI tacis
    1.36    	    val (tac, _, _) = last_elem tacis
    1.37 -  	  in fetchproposedtacticOK2xml cI tac (fetchErrorpatterns tac) end
    1.38 +  	  in fetchproposedtacticOK2xml cI tac (Inform.fetchErrorpatterns tac) end
    1.39  	| ("helpless", _) => fetchproposedtacticERROR2xml cI "helpless"
    1.40  	| ("no-fmz-spec", _) => fetchproposedtacticERROR2xml cI "no-fmz-spec"
    1.41  	| ("end-of-calculation", _) =>
    1.42 @@ -281,10 +281,10 @@
    1.43    end)
    1.44      handle _ => sysERROR2xml cI "error in kernel 8";
    1.45  
    1.46 -fun modifyCalcHead cI (ichd as ((p,_),_,_,_,_):icalhd) =
    1.47 +fun modifyCalcHead cI (ichd as ((p,_),_,_,_,_) : Inform.icalhd) =
    1.48    (let 
    1.49      val ((pt,_),_) = get_calc cI
    1.50 -    val (pt, chd as (_,p_,_,_,_,_)) = input_icalhd pt ichd
    1.51 +    val (pt, chd as (_,p_,_,_,_,_)) = Inform.input_icalhd pt ichd
    1.52    in (upd_calc cI ((pt, (p,p_)), []); modifycalcheadOK2xml cI chd) end)
    1.53      handle _ => sysERROR2xml cI "error in kernel 9";
    1.54  
    1.55 @@ -439,7 +439,7 @@
    1.56    in
    1.57      case Math_Engine.step pos cs of
    1.58  	    ("ok", cs') =>
    1.59 -	      (case inform cs' (encode ifo) of
    1.60 +	      (case Inform.inform cs' (encode ifo) of
    1.61  	        ("ok", (_(*use in DG !!!*), c, ptp as (_, p))) =>
    1.62  	          (upd_calc cI (ptp, []); upd_ipos cI 1 p;
    1.63  	          appendformulaOK2xml cI pos (if null c then pos else last_elem c) p)
    1.64 @@ -459,7 +459,7 @@
    1.65      val ((pt, _), _) = get_calc cI
    1.66      val p = get_pos cI 1
    1.67    in
    1.68 -    case inform (([], [], (pt, p)): calcstate') (encode ifo) of
    1.69 +    case Inform.inform (([], [], (pt, p)): calcstate') (encode ifo) of
    1.70  	    ("ok", (_(*tacs used for DG ?*), c, ptp' as (_, p'))) =>
    1.71  	      let
    1.72  	        val unc = if null (fst p) then p else move_up [] pt p
    1.73 @@ -653,7 +653,7 @@
    1.74    let
    1.75      val ((pt, _), _) = get_calc cI
    1.76  		val pos = get_pos cI 1;
    1.77 -		val fillpats = find_fillpatterns (pt, pos) errpatID
    1.78 +		val fillpats = Inform.find_fillpatterns (pt, pos) errpatID
    1.79    in findFillpatterns2xml cI (map #1 fillpats) end
    1.80  
    1.81  (* given a fillpatID propose a fillform to the learner on the worksheet;
    1.82 @@ -666,7 +666,7 @@
    1.83    let
    1.84      val ((pt, _), _) = get_calc cI
    1.85  		val pos = get_pos cI 1
    1.86 -    val fillforms = find_fillpatterns (pt, pos) errpatID
    1.87 +    val fillforms = Inform.find_fillpatterns (pt, pos) errpatID
    1.88    in
    1.89      case filter ((curry op = fillpatID) o
    1.90          (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms of
    1.91 @@ -690,7 +690,7 @@
    1.92      val ((pt, _), _) = get_calc cI
    1.93      val pos = get_pos cI 1;
    1.94    in
    1.95 -    case is_exactly_equal (pt, pos) ifo of
    1.96 +    case Inform.is_exactly_equal (pt, pos) ifo of
    1.97        ("ok", tac) =>
    1.98          let
    1.99          in (* cp from applyTactic *)