1.1 --- a/test/Tools/isac/BridgeLibisabelle/mathml.sml Mon Apr 19 20:44:18 2021 +0200
1.2 +++ b/test/Tools/isac/BridgeLibisabelle/mathml.sml Tue Apr 20 16:58:44 2021 +0200
1.3 @@ -7,10 +7,10 @@
1.4 "-----------------------------------------------------------------";
1.5 "within struct ---------------------------------------------------";
1.6 "-----------------------------------------------------------------";
1.7 -"--------- encode ^^^ -> ^ ---------------------------------------";
1.8 +"--------- encode \<up> -> ^ ---------------------------------------";
1.9 "--------- encode < -> < and > -> > --------------------------";
1.10 -"--------- fun rm_doublets '-4 * b ^^^^^^^^^ 2 / (...' -----------";
1.11 -"--------- fun decode '-4 * b ^^^^^^^^^ 2 / (...' ----------------";
1.12 +"--------- fun rm_doublets '-4 * b \<up>\<up>\<up> 2 / (...' -----------";
1.13 +"--------- fun decode '-4 * b \<up>\<up>\<up> 2 / (...' ----------------";
1.14 "--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
1.15 "--------- create testdata for TestPIDE.java#testTermTransfer ----";
1.16 "-----------------------------------------------------------------";
1.17 @@ -26,18 +26,18 @@
1.18 "-----------------------------------------------------------------";
1.19 (*==================================================================*)
1.20
1.21 -"--------- encode ^^^ -> ^ ---------------------------------------";
1.22 -"--------- encode ^^^ -> ^ ---------------------------------------";
1.23 -"--------- encode ^^^ -> ^ ---------------------------------------";
1.24 -val str = "a^^^2+b^^^2=c^^^2";
1.25 -if decode str = "a^2+b^2=c^2" then ()
1.26 -else error "mathml.sml: diff.behav. in encode ^^^ -> ^";
1.27 +"--------- encode \<up> -> ^ ---------------------------------------";
1.28 +"--------- encode \<up> -> ^ ---------------------------------------";
1.29 +"--------- encode \<up> -> ^ ---------------------------------------";
1.30 +val str = "a\<up>2+b\<up>2=c\<up>2";
1.31 +if decode str = "a\<up>2+b\<up>2=c\<up>2" then ()
1.32 +else error "mathml.sml: diff.behav. in encode \<up> -> ^";
1.33
1.34 "--------- encode < -> < and > -> > --------------------------";
1.35 "--------- encode < -> < and > -> > --------------------------";
1.36 "--------- encode < -> < and > -> > --------------------------";
1.37 -val str = "?bdv occurs_in ?b; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n";
1.38 -if decode str = "?bdv occurs_in ?b; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n" then ()
1.39 +val str = "?bdv occurs_in ?b; 0 < ?n |] ==> ?a / ?b \<up> ?n = ?a * ?b \<up> - ?n";
1.40 +if decode str = "?bdv occurs_in ?b; 0 < ?n |] ==> ?a / ?b \<up> ?n = ?a * ?b \<up> - ?n" then ()
1.41 else error "mathml.sml: diff.behav. in encode '<' and '>'";
1.42
1.43 (*========== inhibit exn AK110725 ================================================
1.44 @@ -45,20 +45,20 @@
1.45 formula2xml 1 (TermC.str2term str);
1.46
1.47 (* AK110725
1.48 -(*TermC.str2term str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
1.49 +(*TermC.str2term str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b \<up> ?n = ?a * ?b \<up> - ?n"
1.50 Failed to TermC.parse term*)*)
1.51 "~~~~~ fun TermC.str2term, args:"; val (str) = (str);
1.52 ThyC.get_theory "Isac_Knowledge";
1.53
1.54 TermC.parse_patt;
1.55 TermC.parse_patt (ThyC.get_theory "Isac_Knowledge");
1.56 -(*TermC.parse_patt (ThyC.get_theory "Isac_Knowledge") str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
1.57 +(*TermC.parse_patt (ThyC.get_theory "Isac_Knowledge") str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b \<up> ?n = ?a * ?b \<up> - ?n"
1.58 Failed to TermC.parse term*)*)
1.59
1.60 "~~~~~ fun TermC.parse_patt, args:"; val (thy, str) = ((ThyC.get_theory "Isac_Knowledge"), str);
1.61 (thy, str)
1.62 |>> ThyC.to_ctxt
1.63 -(*|-> Proof_Context.read_term_pattern (*ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
1.64 +(*|-> Proof_Context.read_term_pattern (*ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b \<up> ?n = ?a * ?b \<up> - ?n"
1.65 Failed to TermC.parse term*)*)
1.66
1.67 Proof_Context.read_term_pattern;
1.68 @@ -72,32 +72,6 @@
1.69 "-----------------------------------------------------------------";
1.70 ========== inhibit exn AK110725 ================================================*)
1.71
1.72 -"--------- fun rm_doublets '-4 * b ^^^^^^^^^ 2 / (...' -----------";
1.73 -"--------- fun rm_doublets '-4 * b ^^^^^^^^^ 2 / (...' -----------";
1.74 -"--------- fun rm_doublets '-4 * b ^^^^^^^^^ 2 / (...' -----------";
1.75 -val c = "^";
1.76 -val cs = ["^", "^", "^", "d", "e"];
1.77 -if rm_doublets c [] cs = Symbol.explode "^de"
1.78 -then () else error "rm_doublets '^^^de' CHANGED";
1.79 -
1.80 -val cs = ["a", "b", "^", "^", "^", "d", "e"];
1.81 -if rm_doublets c [] cs = Symbol.explode "ab^de"
1.82 -then () else error "rm_doublets 'ab^^^de' CHANGED";
1.83 -
1.84 -val cstr =
1.85 -"-4 * b ^^^^^^^^^ 2 / (a + b) + 4 * a ^^^^^^^^^ 2 / (a + b) -4 * b ^ 2 / (a + b) + 4 * a ^ 2 / (a + b)";
1.86 -val cs = Symbol.explode cstr;
1.87 -if rm_doublets c [] cs = Symbol.explode
1.88 - "-4 * b ^ 2 / (a + b) + 4 * a ^ 2 / (a + b) -4 * b ^ 2 / (a + b) + 4 * a ^ 2 / (a + b)"
1.89 -then () else error "rm_doublets '-4 * b ^^^^^..' CHANGED";
1.90 -
1.91 -"--------- fun decode '-4 * b ^^^^^^^^^ 2 / (...' ----------------";
1.92 -"--------- fun decode '-4 * b ^^^^^^^^^ 2 / (...' ----------------";
1.93 -"--------- fun decode '-4 * b ^^^^^^^^^ 2 / (...' ----------------";
1.94 -if encode cstr =
1.95 -"-4 * b ^^^ 2 / (a + b) + 4 * a ^^^ 2 / (a + b) -4 * b ^^^ 2 / (a + b) + 4 * a ^^^ 2 / (a + b)"
1.96 -then () else error "encode '-4 * b ^^^^^..' CHANGED";
1.97 -
1.98 "--------- fun xmlstr --------------------------------------------";
1.99 "--------- fun xmlstr --------------------------------------------";
1.100 "--------- fun xmlstr --------------------------------------------";
1.101 @@ -143,7 +117,7 @@
1.102 *** . . Type (Real.real,[])
1.103 *** . . ]
1.104 *** . ]
1.105 -with this ^^^ build the typ ...*)
1.106 +with this \<up> build the typ ...*)
1.107 Type ("fun", [
1.108 Type ("Real.real", []),
1.109 Type ("fun", [
1.110 @@ -159,7 +133,7 @@
1.111 *** . . Type (HOL.bool,[])
1.112 *** . . ]
1.113 *** . ]
1.114 -with this ^^^ build the typ ...*)
1.115 +with this \<up> build the typ ...*)
1.116 Type ("fun", [
1.117 Type ("Real.real", []),
1.118 Type ("fun", [