1.1 --- a/test/Tools/isac/Test_Isac.thy	Fri Jun 21 06:51:11 2013 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Fri Jun 21 08:06:16 2013 +0200
     1.3 @@ -124,14 +124,25 @@
     1.4    use "Interpret/mstools.sml"
     1.5    use "Interpret/ctree.sml"         (*!...!see(25)*)
     1.6    use "Interpret/ptyps.sml"
     1.7 -  ML {* check_unsynchronized_ref (); (*========= on error: CUT AND PASTE THIS LINE =========*) *}
     1.8 +  ML {* check_unsynchronized_ref (); (*==== trick on error: CUT AND PASTE THIS LINE =========*) *}
     1.9 +(*get_pbt not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]*)
    1.10    use "Interpret/generate.sml"
    1.11 +(*... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
    1.12    use "Interpret/calchead.sml"      (*part.*)
    1.13    use "Interpret/appl.sml"          (*!complete WEGEN INTERMED TESTCODE*)
    1.14    use "Interpret/rewtools.sml"      (*TODO/part.WN120406*)
    1.15 +(*val it = "----------- fun thy_containing_rls ---------------------": string
    1.16 +:
    1.17 + thy_containing_rls changed 1                    ...CONCERNED WITH thehier
    1.18 +*)
    1.19    use "Interpret/script.sml"        (*!TODO/part.*)
    1.20    use "Interpret/solve.sml"         (*part.*)
    1.21    use "Interpret/inform.sml"        (*part.*)
    1.22 +(*val it = "--------- embed fun check_error_patterns ------------------------": string
    1.23 +:
    1.24 +val it = "~~~~~ from inform return val:": string
    1.25 + check_error_patterns broken                     ...CONCERNED WITH thehier
    1.26 +*)
    1.27    use "Interpret/mathengine.sml"    (*!part.*)
    1.28    ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
    1.29    ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
    1.30 @@ -139,12 +150,21 @@
    1.31    use "xmlsrc/datatypes.sml"         (*TODO/part.*)
    1.32    use "xmlsrc/pbl-met-hierarchy.sml" (*TODO after 2009-2/part.*)
    1.33    use "xmlsrc/thy-hierarchy.sml"     (*TODO after 2009-2/part.*)
    1.34 +(*val it = "----------- ### thes2file ... Exception- Match raised -----------": string
    1.35 +:
    1.36 +val it = "~~~~~ fun thes2file, args:": string
    1.37 +val p = "../../tmp/": path
    1.38 +val it = (): unit
    1.39 + exception Bind raised (line 359 of "~~/test/Tools/isac/xmlsrc/thy-hierarchy.sml")
    1.40 +                                                 ...CONCERNED WITH thehier
    1.41 +*)
    1.42    use "xmlsrc/interface-xml.sml"     (*TODO after 2009-2*)
    1.43    ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
    1.44    ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
    1.45    use "Frontend/messages.sml"
    1.46    use "Frontend/states.sml"
    1.47    use "Frontend/interface.sml"
    1.48 +(*... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
    1.49    use          "print_exn_G.sml"
    1.50    ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
    1.51    ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*}