1.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Tue Apr 20 16:58:49 2021 +0200
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Tue Apr 20 17:10:02 2021 +0200
1.3 @@ -64,20 +64,6 @@
1.4 (**)
1.5 open Ctree
1.6 open Pos
1.7 -(* encode "Isabelle"-strings as seen by the user to the
1.8 - format accepted by Isabelle.
1.9 - encode "^" ---> "^^^"; see Knowledge/Atools.thy;
1.10 - called for each cterm', icalhd, fmz in this interface;
1.11 - + see "fun en/decode" in /mathml.sml *)
1.12 -fun encode_imodel imodel =
1.13 - let fun enc (P_Spec.Given ifos) = P_Spec.Given (map encode ifos)
1.14 - | enc (P_Spec.Find ifos) = P_Spec.Find (map encode ifos)
1.15 - | enc (P_Spec.Relate ifos) = P_Spec.Relate (map encode ifos)
1.16 - in map enc imodel:P_Spec.imodel end;
1.17 -fun encode_icalhd ((pos', headl, imodel, pos_, spec) : P_Spec.icalhd) =
1.18 - (pos', encode headl, encode_imodel imodel, pos_, spec) : P_Spec.icalhd;
1.19 -fun encode_fmz (ifos, spec) = (map encode ifos, spec);
1.20 -
1.21
1.22 (***. CalcTree .***)
1.23
1.24 @@ -97,7 +83,7 @@
1.25 compare "fun CalcTreeTEST" which does NOT decode.*)
1.26 fun CalcTree [(fmz, sp)] (*for several variants lateron*) =
1.27 ((let
1.28 - val cs = Step_Specify.nxt_specify_init_calc (encode_fmz (fmz, sp))
1.29 + val cs = Step_Specify.nxt_specify_init_calc (fmz, sp)
1.30 val cI = add_calc cs (*FIXME.WN.8.03: error-handling missing*)
1.31 in calctreeOK2xml cI end)
1.32 handle _ => sysERROR2xml 0 "error in kernel 2")
2.1 --- a/src/Tools/isac/BridgeLibisabelle/mathml.sml Tue Apr 20 16:58:49 2021 +0200
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/mathml.sml Tue Apr 20 17:10:02 2021 +0200
2.3 @@ -6,19 +6,17 @@
2.4
2.5 type xml = string; (* rm together with old code replaced by XML.tree *)
2.6
2.7 -(*.decode Isabelle-strings to the format as seen by the user (1)
2.8 +(*
2.9 EXCEPT xml-coding issues (2).
2.10 (2) have a _reverse_ method
2.11 'isac.util.parser.FormalizationDigest.decodeEntities'
2.12 called within Formula#toSMLString in java
2.13
2.14 - ad(1) decode "^^^" ---> "^"; see Knowledge/Atools.thy;
2.15 ad(2) decode "<" ---> "<", decode ">" ---> ">"
2.16 decode "&" ---> "&"
2.17 called for term2xml; + see "fun encode" below*)
2.18 fun decode (str: TermC.as_string) =
2.19 let fun dec [] = []
2.20 - | dec ("^"::"^"::"^"::cs) = "^"::(dec cs)
2.21 | dec ("&"::cs) = "&"::"a"::"m"::"p"::";"::(dec cs)
2.22 | dec ("<"::cs) = "&"::"l"::"t"::";"::(dec cs)
2.23 | dec (">"::cs) = "&"::"g"::"t"::";"::(dec cs)
3.1 --- a/test/Tools/isac/BridgeLibisabelle/mathml.sml Tue Apr 20 16:58:49 2021 +0200
3.2 +++ b/test/Tools/isac/BridgeLibisabelle/mathml.sml Tue Apr 20 17:10:02 2021 +0200
3.3 @@ -7,10 +7,6 @@
3.4 "-----------------------------------------------------------------";
3.5 "within struct ---------------------------------------------------";
3.6 "-----------------------------------------------------------------";
3.7 -"--------- encode \<up> -> ^ ---------------------------------------";
3.8 -"--------- encode < -> < and > -> > --------------------------";
3.9 -"--------- fun rm_doublets '-4 * b \<up>\<up>\<up> 2 / (...' -----------";
3.10 -"--------- fun decode '-4 * b \<up>\<up>\<up> 2 / (...' ----------------";
3.11 "--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
3.12 "--------- create testdata for TestPIDE.java#testTermTransfer ----";
3.13 "-----------------------------------------------------------------";
3.14 @@ -26,51 +22,6 @@
3.15 "-----------------------------------------------------------------";
3.16 (*==================================================================*)
3.17
3.18 -"--------- encode \<up> -> ^ ---------------------------------------";
3.19 -"--------- encode \<up> -> ^ ---------------------------------------";
3.20 -"--------- encode \<up> -> ^ ---------------------------------------";
3.21 -val str = "a\<up>2+b\<up>2=c\<up>2";
3.22 -if decode str = "a\<up>2+b\<up>2=c\<up>2" then ()
3.23 -else error "mathml.sml: diff.behav. in encode \<up> -> ^";
3.24 -
3.25 -"--------- encode < -> < and > -> > --------------------------";
3.26 -"--------- encode < -> < and > -> > --------------------------";
3.27 -"--------- encode < -> < and > -> > --------------------------";
3.28 -val str = "?bdv occurs_in ?b; 0 < ?n |] ==> ?a / ?b \<up> ?n = ?a * ?b \<up> - ?n";
3.29 -if decode str = "?bdv occurs_in ?b; 0 < ?n |] ==> ?a / ?b \<up> ?n = ?a * ?b \<up> - ?n" then ()
3.30 -else error "mathml.sml: diff.behav. in encode '<' and '>'";
3.31 -
3.32 -(*========== inhibit exn AK110725 ================================================
3.33 -"----- check 'manually' the xml-output of calling functions ------";
3.34 -formula2xml 1 (TermC.str2term str);
3.35 -
3.36 -(* AK110725
3.37 -(*TermC.str2term str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b \<up> ?n = ?a * ?b \<up> - ?n"
3.38 - Failed to TermC.parse term*)*)
3.39 -"~~~~~ fun TermC.str2term, args:"; val (str) = (str);
3.40 -ThyC.get_theory "Isac_Knowledge";
3.41 -
3.42 -TermC.parse_patt;
3.43 -TermC.parse_patt (ThyC.get_theory "Isac_Knowledge");
3.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"
3.45 -Failed to TermC.parse term*)*)
3.46 -
3.47 -"~~~~~ fun TermC.parse_patt, args:"; val (thy, str) = ((ThyC.get_theory "Isac_Knowledge"), str);
3.48 -(thy, str)
3.49 -|>> ThyC.to_ctxt
3.50 -(*|-> Proof_Context.read_term_pattern (*ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b \<up> ?n = ?a * ?b \<up> - ?n"
3.51 -Failed to TermC.parse term*)*)
3.52 -
3.53 -Proof_Context.read_term_pattern;
3.54 -(@{theory "Isac_Knowledge"}, str) |>> ThyC.to_ctxt;
3.55 -"~~~~~ fun Proof_Context.read_term_pattern, args:"; val () = ();
3.56 -(*AK110725 To be continued...*)
3.57 -*)
3.58 -(*==================================================================*)
3.59 -"-----------------------------------------------------------------";
3.60 -"exported from struct --------------------------------------------";
3.61 -"-----------------------------------------------------------------";
3.62 -========== inhibit exn AK110725 ================================================*)
3.63
3.64 "--------- fun xmlstr --------------------------------------------";
3.65 "--------- fun xmlstr --------------------------------------------";
4.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Tue Apr 20 16:58:49 2021 +0200
4.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Tue Apr 20 17:10:02 2021 +0200
4.3 @@ -64,16 +64,6 @@
4.4 "within struct ---------------------------------------------------";
4.5 (*==================================================================
4.6
4.7 -
4.8 -"--------- encode ^ -> ^^ ------------------------------";
4.9 -"--------- encode ^ -> ^^ ------------------------------";
4.10 -"--------- encode ^ -> ^^ ------------------------------";
4.11 -if encode "a \<up> 2+b \<up> 2=c \<up> 2" = "a \<up> 2+b \<up> 2=c \<up> 2" then ()
4.12 -else error "interface.sml: diff.behav. in encode ^ -> \<up> ";
4.13 -
4.14 -if (decode o encode) "a \<up> 2+b \<up> 2=c \<up> 2" = "a \<up> 2+b \<up> 2=c \<up> 2" then ()
4.15 -else error "interface.sml: diff.behav. in de/encode ^ <-> \<up> ";
4.16 -
4.17 ==================================================================*)
4.18 "exported from struct --------------------------------------------";
4.19 "exported from struct --------------------------------------------";