1.1 --- a/test/Tools/isac/BridgeLibisabelle/mathml.sml	Tue Apr 20 16:58:49 2021 +0200
     1.2 +++ b/test/Tools/isac/BridgeLibisabelle/mathml.sml	Tue Apr 20 17:10:02 2021 +0200
     1.3 @@ -7,10 +7,6 @@
     1.4  "-----------------------------------------------------------------";
     1.5  "within struct ---------------------------------------------------";
     1.6  "-----------------------------------------------------------------";
     1.7 -"--------- encode \<up> -> ^ ---------------------------------------";
     1.8 -"--------- encode < -> &lt and > -> &gt --------------------------";
     1.9 -"--------- fun rm_doublets '-4 * b \<up>\<up>\<up> 2 / (...' -----------";
    1.10 -"--------- fun decode '-4 * b \<up>\<up>\<up> 2 / (...' ----------------";
    1.11  "--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
    1.12  "--------- create testdata for TestPIDE.java#testTermTransfer ----";
    1.13  "-----------------------------------------------------------------";
    1.14 @@ -26,51 +22,6 @@
    1.15  "-----------------------------------------------------------------";
    1.16  (*==================================================================*)
    1.17  
    1.18 -"--------- encode \<up> -> ^ ---------------------------------------";
    1.19 -"--------- encode \<up> -> ^ ---------------------------------------";
    1.20 -"--------- encode \<up> -> ^ ---------------------------------------";
    1.21 -val str = "a\<up>2+b\<up>2=c\<up>2";
    1.22 -if decode str = "a\<up>2+b\<up>2=c\<up>2" then ()
    1.23 -else error "mathml.sml: diff.behav. in encode \<up> -> ^";
    1.24 -
    1.25 -"--------- encode < -> &lt; and > -> &gt; --------------------------";
    1.26 -"--------- encode < -> &lt; and > -> &gt; --------------------------";
    1.27 -"--------- encode < -> &lt; and > -> &gt; --------------------------";
    1.28 -val str = "?bdv occurs_in ?b; 0 < ?n |] ==> ?a / ?b  \<up>  ?n = ?a * ?b  \<up>  - ?n";
    1.29 -if decode str = "?bdv occurs_in ?b; 0 &lt; ?n |] ==&gt; ?a / ?b  \<up>  ?n = ?a * ?b  \<up>  - ?n" then ()
    1.30 -else error "mathml.sml: diff.behav. in encode '<' and '>'";
    1.31 -
    1.32 -(*========== inhibit exn AK110725 ================================================
    1.33 -"----- check 'manually' the xml-output of calling functions ------";
    1.34 -formula2xml 1 (TermC.str2term str);
    1.35 -
    1.36 -(* AK110725 
    1.37 -(*TermC.str2term str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b  \<up>  ?n = ?a * ?b  \<up>  - ?n"
    1.38 -                   Failed to TermC.parse term*)*)
    1.39 -"~~~~~ fun TermC.str2term, args:"; val (str) = (str);
    1.40 -ThyC.get_theory "Isac_Knowledge";
    1.41 -
    1.42 -TermC.parse_patt;
    1.43 -TermC.parse_patt (ThyC.get_theory "Isac_Knowledge");
    1.44 -(*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.45 -Failed to TermC.parse term*)*)
    1.46 -
    1.47 -"~~~~~ fun TermC.parse_patt, args:"; val (thy, str) = ((ThyC.get_theory "Isac_Knowledge"), str);
    1.48 -(thy, str) 
    1.49 -|>> ThyC.to_ctxt
    1.50 -(*|-> Proof_Context.read_term_pattern (*ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b  \<up>  ?n = ?a * ?b  \<up>  - ?n"
    1.51 -Failed to TermC.parse term*)*)
    1.52 -
    1.53 -Proof_Context.read_term_pattern;
    1.54 -(@{theory "Isac_Knowledge"}, str) |>> ThyC.to_ctxt;
    1.55 -"~~~~~ fun Proof_Context.read_term_pattern, args:"; val () = ();
    1.56 -(*AK110725 To be continued...*)
    1.57 -*)
    1.58 -(*==================================================================*)
    1.59 -"-----------------------------------------------------------------";
    1.60 -"exported from struct --------------------------------------------";
    1.61 -"-----------------------------------------------------------------";
    1.62 -========== inhibit exn AK110725 ================================================*)
    1.63  
    1.64  "--------- fun xmlstr --------------------------------------------";
    1.65  "--------- fun xmlstr --------------------------------------------";