2 * @author Walther Neuper
3 * Copyright (c) due to license terms
4 * Created on Jul 14, 2015
5 * Institute for Softwaretechnology, Graz University of Technology, Austria.
7 * From now on isac-java is a Scala Project.
8 * When ConvertXML.scala was not recognized switiching "Scala Nature"
9 * off and on again helped.
12 package isac.bridge.xml
14 import isac.util.formulae.Position
15 import isac.bridge.CChanged
18 import isabelle.Markup
19 import java.util.ArrayList
20 import java.util.Vector
21 import java.math.BigInteger
22 import scala.math.BigInt
23 import scala.collection.JavaConverters._
27 def xml_to_VectorInteger (t: XML.Tree): Vector[java.lang.Integer] = t match { //Java <-- XML(Scala)
28 case XML.Elem(Markup("INTLIST", Nil), is) => {
29 val v = new java.util.Vector[java.lang.Integer];
30 is.foreach { case (XML.Elem(Markup("INT", Nil), List(XML.Text(i)))) => v.add(new java.lang.Integer(i)) }
33 case _ => throw new IllegalArgumentException("xml_to_VectorInteger exn")
36 //===== convert results of JSystem.invoke(Operations.* using Java <-- XML(Scala) =============
37 //----- step 1 -----------------------
38 def calc_tree_out(t: XML.Tree): java.lang.Integer = t match {
40 XML.Elem(Markup("CALCTREE", Nil), List(
41 XML.Elem(Markup("CALCID", Nil), List(XML.Text(i)))))
43 case //...should not occur, thus thrown away already here:
44 XML.Elem(Markup("SYSERROR", Nil), List(
45 XML.Elem(Markup("CALCID", Nil), List(XML.Text(i))),
46 XML.Elem(Markup("CALCID", Nil), List(XML.Text(msg)))))
47 => throw new IllegalArgumentException("calc_tree_out SYSERROR")
48 case _ => throw new IllegalArgumentException("calc_tree_out exn")
51 //----- step 2 -----------------------
52 def iterator_out(t: XML.Tree): IntIntCompound = t match {
54 XML.Elem(Markup("ADDUSER", Nil), List(
55 XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid))),
56 XML.Elem(Markup("USERID", Nil), List(XML.Text(userid)))))
57 => new IntIntCompound(new java.lang.Integer(calcid), new java.lang.Integer(userid))
58 case _ => throw new IllegalArgumentException("iterator_out exn")
61 //----- step 3 -----------------------
62 def move_active_root_out(t: XML.Tree): IntPosition = t match {
64 XML.Elem (Markup("CALCITERATOR", Nil), List(
65 XML.Elem (Markup("CALCID", Nil), List(
67 XML.Elem(Markup("POSITION", Nil), List(
68 is, XML.Elem(Markup("POS", Nil), List(XML.Text(kind)))))))
69 => new IntPosition(new java.lang.Integer(calcid),
70 new Position(xml_to_VectorInteger(is), kind))
71 case _ => throw new IllegalArgumentException("move_active_root_out exn")
74 //----- step 4 ----------------------------------------------------------------
75 //----- step 6 ----------------------------------------------------------------
76 //----- step 7 ----------------------------------------------------------------
77 def auto_calc_out(t: XML.Tree): IntCChanged = t match {
79 XML.Elem(Markup("AUTOCALC", Nil), List(
80 XML.Elem(Markup("CALCID", Nil), List(XML.Text (calcid))),
81 XML.Elem(Markup("CALCCHANGED", Nil), List(
82 XML.Elem(Markup("UNCHANGED", Nil), List(
83 unc_is, XML.Elem(Markup("POS", Nil), List(XML.Text(unc_kind))))),
84 XML.Elem(Markup("DELETED", Nil), List(
85 del_is, XML.Elem(Markup("POS", Nil), List(XML.Text(del_kind))))),
86 XML.Elem(Markup("GENERATED", Nil), List(
87 gen_is, XML.Elem(Markup("POS", Nil), List(XML.Text(gen_kind)))))))))
88 => new IntCChanged(new java.lang.Integer(calcid), new CChanged(
89 new Position(xml_to_VectorInteger(unc_is), unc_kind),
90 new Position(xml_to_VectorInteger(del_is), del_kind),
91 new Position(xml_to_VectorInteger(gen_is), gen_kind)))
92 case _ => throw new IllegalArgumentException("auto_calc_out exn")
94 //----- step 10 ---------------------------------------------------------------
95 def ref_formula_out(t: XML.Tree): java.lang.Object = t match {
97 XML.Elem(Markup("REFFORMULA", Nil), List(
98 XML.Elem(Markup("CALCID", Nil), List(XML.Text (calcid))),
99 XML.Elem(Markup("CALCFORMULA", Nil), List(
100 XML.Elem(Markup("POSITION", Nil), List(
101 form_ints, XML.Elem(Markup("POS", Nil), List(XML.Text(form_kind))))),
102 XML.Elem(Markup("FORMULA", Nil), List(
103 XML.Elem(Markup("MATHML", Nil), List(
104 XML.Elem(Markup("ISA", Nil), List(XML.Text(form_isa)))))))))))
105 => new IntCalcFormCompound(new java.lang.Integer(calcid),
106 xml_to_VectorInteger(form_ints), form_kind, form_isa)
108 //this becomes cumbersome without import CalcHead .. Model .. ModelItemList
109 //thus we shift ConvertXML to isac-java
111 // XML.Elem(Markup("REFFORMULA", Nil), List(
112 // XML.Elem(Markup("CALCID", Nil), List(XML.Text (calcid))),
113 // XML.Elem(Markup("CALCHEAD", !!!!!!!!!!!!!!!!!!!!!!!!), List(
114 // XML.Elem(Markup("POSITION", Nil), List(
115 // form_ints, XML.Elem(Markup("POS", Nil), List(XML.Text(form_kind))))),
116 // XML.Elem(Markup("HEAD", Nil), List(
117 // XML.Elem(Markup("MATHML", Nil), List(
118 // XML.Elem(Markup("ISA", Nil), List(XML.Text(form_isa)))))))))))
121 // => new IntCalcHeadCompound(new java.lang.Integer(calcid),
122 // head_status, xml_to_VectorInteger(head_ints), head_kind, form_isa, head_isa,
123 // xml_to_VectorString(givens), xml_to_VectorString(wheres), xml_to_VectorString(finds), xml_to_VectorString(relates),
124 // belongsto, xml_to_VectorString(thy), xml_to_VectorString(pbl), xml_to_VectorString(met))
125 case _ => throw new IllegalArgumentException("ref_formula_out exn")
128 //----- step 13 ---------------------------------------------------------------
129 def del_calc_out(t: XML.Tree): java.lang.Integer = t match {
131 XML.Elem(Markup("DELCALC", Nil), List(
132 XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid)))))
133 => new java.lang.Integer(calcid)
134 case _ => throw new IllegalArgumentException("del_calc_out exn")