Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/xmlsrc/mathml.sml
branchdecompose-isar
changeset 42176 3573fd729e99
parent 38031 460c24a6a6ba
child 48761 4162c4f6f897
equal deleted inserted replaced
42175:97b5b13937e1 42176:3573fd729e99 
     1 (* tests for mathml.sml
 
     1 (* Title: tests for mathml.sml
 
     2    author: Walther Neuper 060311
 
     2    Author: Walther Neuper 060311
 
     3    (c) isac-team 2006
 
     3    (c) isac-team 2006
 
     4 
     4 
     5 use"../smltest/xmlsrc/mathml.sml";
 
     5 use"../smltest/xmlsrc/mathml.sml";
 
     6 use"mathml.sml";
 
     6 use"mathml.sml";
 
     7 *)
 
     7 *)
 
    23 "-----------------------------------------------------------------";
 
    23 "-----------------------------------------------------------------";
 
    24 "within struct ---------------------------------------------------";
 
    24 "within struct ---------------------------------------------------";
 
    25 "-----------------------------------------------------------------";
 
    25 "-----------------------------------------------------------------";
 
    26 (*==================================================================*)
 
    26 (*==================================================================*)
 
    27 
    27 
    28 
       
    29 "--------- encode ^^^ -> ^ ---------------------------------------";
 
    28 "--------- encode ^^^ -> ^ ---------------------------------------";
 
    30 "--------- encode ^^^ -> ^ ---------------------------------------";
 
    29 "--------- encode ^^^ -> ^ ---------------------------------------";
 
    31 "--------- encode ^^^ -> ^ ---------------------------------------";
 
    30 "--------- encode ^^^ -> ^ ---------------------------------------";
 
    32 val str = "a^^^2+b^^^2=c^^^2";
 
    31 val str = "a^^^2+b^^^2=c^^^2";
 
    33 if decode str = "a^2+b^2=c^2" then ()
 
    32 if decode str = "a^2+b^2=c^2" then ()
 
    34 else error "mathml.sml: diff.behav. in encode ^^^ -> ^";
 
    33 else error "mathml.sml: diff.behav. in encode ^^^ -> ^";
 
    35 
    34 
    36 "--------- encode < -> &lt and > -> &gt --------------------------";
 
    35 "--------- encode < -> &lt; and > -> &gt; --------------------------";
 
    37 "--------- encode < -> &lt and > -> &gt --------------------------";
 
    36 "--------- encode < -> &lt; and > -> &gt; --------------------------";
 
    38 "--------- encode < -> &lt and > -> &gt --------------------------";
 
    37 "--------- encode < -> &lt; and > -> &gt; --------------------------";
 
    39 val str = "?bdv occurs_in ?b; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n";
 
    38 val str = "?bdv occurs_in ?b; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n";
 
    40 if decode str = 
    39 if decode str = "?bdv occurs_in ?b; 0 &lt; ?n |] ==&gt; ?a / ?b ^ ?n = ?a * ?b ^ - ?n" then ()
 
    41    "?bdv occurs_in ?b; 0 &lt ?n |] ==&gt ?a / ?b ^ ?n = ?a * ?b ^ - ?n" 
    40 else error "mathml.sml: diff.behav. in encode '<' and '>'";
 
    42 then () else error "mathml.sml: diff.behav. in encode '<' and '>'";
 
       
    43 
    41 
       
    42 (*========== inhibit exn AK110725 ================================================
 
    44 "----- check 'manually' the xml-output of calling functions ------";
 
    43 "----- check 'manually' the xml-output of calling functions ------";
 
    45 formula2xml 1 (str2term )
 
    44 formula2xml 1 (str2term str);
 
    46 
    45 
       
    46 (* AK110725 
       
    47 (*str2term str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
 
       
    48                    Failed to parse term*)*)
 
       
    49 "~~~~~ fun str2term, args:"; val (str) = (str);
 
       
    50 Thy_Info.get_theory "Isac";
 
       
    51 
       
    52 parse_patt;
 
       
    53 parse_patt (Thy_Info.get_theory "Isac");
 
       
    54 (*parse_patt (Thy_Info.get_theory "Isac") str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
 
       
    55 Failed to parse term*)*)
 
       
    56 
       
    57 "~~~~~ fun parse_patt, args:"; val (thy, str) = ((Thy_Info.get_theory "Isac"), str);
 
       
    58 (thy, str) 
       
    59 |>> thy2ctxt
 
       
    60 (*|-> ProofContext.read_term_pattern (*ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
 
       
    61 Failed to parse term*)*)
 
       
    62 
       
    63 ProofContext.read_term_pattern;
 
       
    64 (@{theory "Isac"}, str) |>> thy2ctxt;
 
       
    65 "~~~~~ fun ProofContext.read_term_pattern, args:"; val () = ();
 
       
    66 (*AK110725 To be continued...*)
 
       
    67 *)
 
    47 (*==================================================================*)
 
    68 (*==================================================================*)
 
    48 "-----------------------------------------------------------------";
 
    69 "-----------------------------------------------------------------";
 
    49 "exported from struct --------------------------------------------";
 
    70 "exported from struct --------------------------------------------";
 
    50 "-----------------------------------------------------------------";
 
    71 "-----------------------------------------------------------------";
 
    51 
    72 ========== inhibit exn AK110725 ================================================*)
 
    52
wneuper/isa