1.1 --- a/src/Tools/isac/Frontend/interface.sml	Mon Aug 06 10:38:11 2012 +0200
     1.2 +++ b/src/Tools/isac/Frontend/interface.sml	Mon Aug 06 16:19:30 2012 +0200
     1.3 @@ -181,7 +181,7 @@
     1.4  	   ("ok", (tacis, _, _)) =>
     1.5  	   let val _= upd_tacis cI tacis
     1.6  	       val (tac,_,_) = last_elem tacis
     1.7 -	   in fetchproposedtacticOK2xml cI tac end
     1.8 +	   in fetchproposedtacticOK2xml cI tac (fetchErrorpatterns tac) end
     1.9  	 | ("helpless",_) => fetchproposedtacticERROR2xml cI "helpless"
    1.10  	 | ("no-fmz-spec",_) => fetchproposedtacticERROR2xml cI "no-fmz-spec"
    1.11  	 | ("end-of-calculation",_) =>

     2.1 --- a/src/Tools/isac/Interpret/inform.sml	Mon Aug 06 10:38:11 2012 +0200
     2.2 +++ b/src/Tools/isac/Interpret/inform.sml	Mon Aug 06 16:19:30 2012 +0200
     2.3 @@ -769,6 +769,23 @@
     2.4              end
     2.5        end
     2.6  
     2.7 +(* fetch errpatIDs from an arbitrary tactic *)
     2.8 +fun fetchErrorpatterns tac =
     2.9 +  let
    2.10 +    val rlsID =
    2.11 +      case tac of
    2.12 +        Rewrite_Set rlsID => rlsID
    2.13 +      | Rewrite_Set_Inst (_, rlsID) => rlsID
    2.14 +      | _ => "list_rls" (*WN120806 "e_rls" is appropriate, but raises exn 'get_pbt not found: ?!?*)
    2.15 +    val (part, thyID) = thy_containing_rls "Isac" rlsID;
    2.16 +    val Hrls {thy_rls = (_, rls), ...} = get_the [part, thyID, "Rulesets", rlsID]
    2.17 +  in case rls of
    2.18 +        Rls {errpatts, ...} => errpatts
    2.19 +      | Seq {errpatts, ...} => errpatts
    2.20 +      | Rrls {errpatts, ...} => errpatts
    2.21 +      | Erls => []
    2.22 +  end
    2.23 +
    2.24  (*------------------------------------------------------------------(**)
    2.25  end
    2.26  open inform; 

     3.1 --- a/src/Tools/isac/Knowledge/Diff.thy	Mon Aug 06 10:38:11 2012 +0200
     3.2 +++ b/src/Tools/isac/Knowledge/Diff.thy	Mon Aug 06 16:19:30 2012 +0200
     3.3 @@ -236,7 +236,7 @@
     3.4  (*.normalisation for checking user-input.*)
     3.5  val norm_diff = 
     3.6    Rls
     3.7 -    {id="diff_rls", preconds = [], rew_ord = ("termlessI",termlessI), 
     3.8 +    {id="norm_diff", preconds = [], rew_ord = ("termlessI",termlessI), 
     3.9       erls = Erls, srls = Erls, calc = [], errpatts = [],
    3.10       rules = [Rls_ diff_rules, Rls_ norm_Poly ],
    3.11       scr = EmptyScr};

     4.1 --- a/src/Tools/isac/ProgLang/ListC.thy	Mon Aug 06 10:38:11 2012 +0200
     4.2 +++ b/src/Tools/isac/ProgLang/ListC.thy	Mon Aug 06 16:19:30 2012 +0200
     4.3 @@ -146,7 +146,7 @@
     4.4  (** rule set for evaluating listexpr in scripts **)
     4.5  val list_rls = 
     4.6    Rls{id="list_rls",preconds = [], rew_ord = ("dummy_ord",dummy_ord), 
     4.7 -      erls = e_rls, srls = Erls, calc = [], errpatts = [],
     4.8 +      erls = Erls, srls = Erls, calc = [], errpatts = [],
     4.9        rules = (*8.01: copied from*)
    4.10        [Thm ("refl", num_str @{thm refl}),  (*'a<>b -> FALSE' by fun eval_equal*)
    4.11         Thm ("o_apply", num_str @{thm o_apply}),

     5.1 --- a/src/Tools/isac/calcelems.sml	Mon Aug 06 10:38:11 2012 +0200
     5.2 +++ b/src/Tools/isac/calcelems.sml	Mon Aug 06 16:19:30 2012 +0200
     5.3 @@ -470,27 +470,16 @@
     5.4  		     next_rule=ne,attach_form=fo};
     5.5  end;
     5.6  
     5.7 -val e_rls = Rls {
     5.8 -  id = "e_rls",
     5.9 -  preconds = [],
    5.10 -  rew_ord = ("dummy_ord", dummy_ord),
    5.11 -  erls = Erls,srls = Erls,
    5.12 -  calc = [],
    5.13 -  rules = [],
    5.14 -  errpatts = [],
    5.15 -  scr = EmptyScr}: rls;
    5.16 +val e_rls =
    5.17 +  Rls {id = "e_rls", preconds = [], rew_ord = ("dummy_ord", dummy_ord), erls = Erls,
    5.18 +    srls = Erls, calc = [], rules = [], errpatts = [], scr = EmptyScr}: rls;
    5.19 +val e_rrls =
    5.20 +  Rrls {id = "e_rrls", prepat = [], rew_ord = ("dummy_ord", dummy_ord), erls = Erls,
    5.21 +    calc = [], errpatts = [], scr=e_rfuns}:rls;
    5.22  
    5.23 -val e_rrls = Rrls {
    5.24 -  id = "e_rrls",
    5.25 -		  prepat = [],
    5.26 -		  rew_ord = ("dummy_ord", dummy_ord),
    5.27 -		  erls = Erls,
    5.28 -		  calc = [],
    5.29 -		  errpatts = [],
    5.30 -	   scr=e_rfuns}:rls;
    5.31 -ruleset' := overwritel (!ruleset', [("e_rls",("Tools",e_rls)),
    5.32 -				    ("e_rrls",("Tools",e_rrls))
    5.33 -				    ]);
    5.34 +ruleset' := overwritel (!ruleset', 
    5.35 +  [("e_rls", ("Tools", e_rls)),
    5.36 +   ("e_rrls", ("Tools", e_rrls))]);
    5.37  
    5.38  fun rep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,errpatts,rules,scr}) =
    5.39    {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,

     6.1 --- a/src/Tools/isac/xmlsrc/interface-xml.sml	Mon Aug 06 10:38:11 2012 +0200
     6.2 +++ b/src/Tools/isac/xmlsrc/interface-xml.sml	Mon Aug 06 16:19:30 2012 +0200
     6.3 @@ -257,13 +257,24 @@
     6.4  	     "</SETNEXTTACTIC>\n" ^
     6.5  	     "@@@@@end@@@@@");
     6.6  
     6.7 -fun fetchproposedtacticOK2xml (cI:calcID) tac = 
     6.8 +fun fetchproposedtacticOK2xml (cI:calcID) tac _ = 
     6.9      writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
    6.10  	     "<NEXTTAC>\n" ^
    6.11  	     "  <CALCID> "^string_of_int cI^" </CALCID>\n"^
    6.12  	     tac2xml i tac^
    6.13  	     "</NEXTTAC>\n" ^
    6.14  	     "@@@@@end@@@@@");
    6.15 +(*NEW JAVA*)
    6.16 +fun fetchproposedtacticOK2xml (cI:calcID) tac (errpatIDs: errpatID list) = 
    6.17 +    writeln ("@@@@@begin@@@@@\n " ^ string_of_int cI ^ " \n" ^
    6.18 +	     "<NEXTTAC>\n" ^
    6.19 +	     "  <CALCID> " ^ string_of_int cI ^ " </CALCID>\n" ^
    6.20 +     "  <TACTICERRORPATTERNS>\n" ^
    6.21 +     id2xml (2*i) errpatIDs ^
    6.22 +	     tac2xml (2*i) tac ^
    6.23 +	     "  </TACTICERRORPATTERNS>\n" ^
    6.24 +     "</NEXTTAC>\n" ^
    6.25 +	     "@@@@@end@@@@@");
    6.26  
    6.27  fun fetchproposedtacticERROR2xml (*uI:userID*) (cI:calcID) e = 
    6.28      writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^