wneuper@4757
|
1 |
/*
|
wneuper@4757
|
2 |
* @author Walther Neuper
|
wneuper@4757
|
3 |
* Copyright (c) due to license terms
|
wneuper@4757
|
4 |
* Created on Jul 14, 2015
|
wneuper@4757
|
5 |
* Institute for Softwaretechnology, Graz University of Technology, Austria.
|
wneuper@4757
|
6 |
*
|
wneuper@4757
|
7 |
* When ConvertXML.scala was not recognized switiching "Scala Nature"
|
wneuper@4757
|
8 |
* off and on again helped.
|
wneuper@4757
|
9 |
*/
|
wneuper@4757
|
10 |
|
wneuper@4757
|
11 |
package isac.bridge.xml
|
wneuper@4757
|
12 |
|
wneuper@4759
|
13 |
import isac.bridge.CChanged
|
wneuper@4788
|
14 |
import isac.bridge.CEvent
|
wneuper@4788
|
15 |
import isac.bridge.CMessage
|
wneuper@4932
|
16 |
import isac.gui.mawen.scalaterm.Util
|
wneuper@5070
|
17 |
import isac.gui.mawen.syntax.Syntax_Phases
|
wneuper@4759
|
18 |
import isac.util.Formalization
|
wneuper@4759
|
19 |
import isac.util.formulae.CalcFormula
|
wneuper@4759
|
20 |
import isac.util.formulae.CalcHead
|
wneuper@4759
|
21 |
import isac.util.formulae.CalcHeadSimpleID
|
wneuper@4825
|
22 |
import isac.util.formulae.ContextMethod
|
wneuper@4825
|
23 |
import isac.util.formulae.ContextProblem
|
wneuper@4789
|
24 |
import isac.util.formulae.ContextTheory
|
wneuper@4759
|
25 |
import isac.util.formulae.Formula
|
wneuper@4789
|
26 |
import isac.util.formulae.FormulaPair
|
wneuper@4759
|
27 |
import isac.util.formulae.HierarchyKey
|
wneuper@4789
|
28 |
import isac.util.formulae.KEStoreKey
|
wneuper@4759
|
29 |
import isac.util.formulae.ModelItem
|
wneuper@4759
|
30 |
import isac.util.formulae.ModelItemList
|
wneuper@4759
|
31 |
import isac.util.formulae.Model
|
wneuper@4757
|
32 |
import isac.util.formulae.Position
|
wneuper@4789
|
33 |
import isac.util.formulae.Reference
|
wneuper@4758
|
34 |
import isac.util.formulae.Specification
|
wneuper@4810
|
35 |
import isac.util.tactics.TermTactic
|
wneuper@4771
|
36 |
import isac.util.tactics.Rewrite
|
wneuper@4771
|
37 |
import isac.util.tactics.RewriteInst
|
wneuper@4771
|
38 |
import isac.util.tactics.RewriteSet
|
wneuper@4771
|
39 |
import isac.util.tactics.RewriteSetInst
|
wneuper@4771
|
40 |
import isac.util.tactics.SimpleTactic
|
wneuper@4771
|
41 |
import isac.util.tactics.StringListTactic
|
wneuper@4771
|
42 |
import isac.util.tactics.SubProblemTactic
|
wneuper@4771
|
43 |
import isac.util.tactics.SubstituteTactic
|
wneuper@4771
|
44 |
import isac.util.tactics.Tactic
|
wneuper@4771
|
45 |
import isac.util.tactics.Theorem
|
wneuper@4892
|
46 |
import isac.util.Variant
|
wneuper@4757
|
47 |
|
walther@5239
|
48 |
import edu.tum.cs.isabelle.api.XML
|
walther@5239
|
49 |
import edu.tum.cs.isabelle.pure._ // for Term
|
walther@5239
|
50 |
import edu.tum.cs.isabelle._ // for Codec
|
wneuper@4848
|
51 |
|
wneuper@4757
|
52 |
import java.util.ArrayList
|
wneuper@4757
|
53 |
import java.util.Vector
|
wneuper@4757
|
54 |
import java.math.BigInteger
|
wneuper@4757
|
55 |
import scala.math.BigInt
|
wneuper@4757
|
56 |
import scala.collection.JavaConverters._
|
wneuper@4757
|
57 |
|
wneuper@4758
|
58 |
/**
|
wneuper@4758
|
59 |
* conversion XML <--> Java-objects in isac-java used by libisabelle;
|
wneuper@4758
|
60 |
* analogous to isabisac/src/Tools/isac/xmlsrc/datatypes.sml.
|
wneuper@4758
|
61 |
*/
|
wneuper@4757
|
62 |
object DataTypes {
|
wneuper@4758
|
63 |
|
wneuper@4759
|
64 |
/**
|
wneuper@4759
|
65 |
* auxiliary methods, both directions
|
wneuper@4759
|
66 |
**/
|
wneuper@4757
|
67 |
|
wneuper@4757
|
68 |
def xml_of_int (i: scala.math.BigInt): XML.Tree = {
|
wneuper@4848
|
69 |
XML.Elem(("INT", Nil), List(XML.Text(i.toString)))
|
wneuper@4757
|
70 |
}
|
wneuper@4757
|
71 |
def xml_to_int (t: XML.Tree): scala.math.BigInt = t match {
|
wneuper@4848
|
72 |
case XML.Elem(("INT", Nil), List(XML.Text(i))) => BigInt(i)
|
wneuper@4757
|
73 |
case _ => throw new IllegalArgumentException("xml_to_int exn")
|
wneuper@4757
|
74 |
}
|
wneuper@4758
|
75 |
def xml_of_ints (is: List[scala.math.BigInt]): XML.Tree = {
|
wneuper@4848
|
76 |
XML.Elem(("INTLIST", Nil), is map xml_of_int)
|
wneuper@4757
|
77 |
}
|
wneuper@4758
|
78 |
def xml_to_ints (t: XML.Tree): List[scala.math.BigInt] = t match {
|
wneuper@4848
|
79 |
case XML.Elem(("INTLIST", Nil), is) => is map xml_to_int
|
wneuper@4757
|
80 |
case _ => throw new IllegalArgumentException("xml_to_ints exn")
|
wneuper@4757
|
81 |
}
|
wneuper@4757
|
82 |
def xml_of_pos (ints: List[scala.math.BigInt], kind: String ): XML.Tree = {
|
wneuper@4848
|
83 |
XML.Elem(("POSITION", Nil), List(
|
wneuper@4757
|
84 |
xml_of_ints(ints),
|
wneuper@4848
|
85 |
XML.Elem(("POS", Nil), List(XML.Text(kind)))))
|
wneuper@4757
|
86 |
}
|
wneuper@4757
|
87 |
def xml_to_pos (t: XML.Tree): (List[scala.math.BigInt], String) = t match {
|
wneuper@4848
|
88 |
case XML.Elem(("POSITION", Nil), List(
|
wneuper@4848
|
89 |
is, XML.Elem(("POS", Nil), List(XML.Text(kind))))) => (xml_to_ints(is), kind)
|
wneuper@4757
|
90 |
case _ => throw new IllegalArgumentException("xml_to_pos exn")
|
wneuper@4757
|
91 |
}
|
wneuper@4758
|
92 |
def xml_to_VectorString (t: XML.Tree): Vector[java.lang.String] = t match {
|
wneuper@4848
|
93 |
case XML.Elem(("STRINGLIST", Nil), is) => {
|
wneuper@4758
|
94 |
val v = new java.util.Vector[java.lang.String];
|
wneuper@4759
|
95 |
is.foreach {
|
wneuper@4848
|
96 |
case (XML.Elem(("STRING", Nil), List(XML.Text(str))))
|
wneuper@4759
|
97 |
=> v.add(str)
|
wneuper@4759
|
98 |
case _ => throw new IllegalArgumentException("xml_to_VectorString 1 wrong arg: " + t)
|
wneuper@4759
|
99 |
}
|
wneuper@4758
|
100 |
v
|
wneuper@4758
|
101 |
}
|
wneuper@4759
|
102 |
case _ => throw new IllegalArgumentException("xml_to_VectorString 2 wrong arg: " + t)
|
wneuper@4758
|
103 |
}
|
wneuper@4771
|
104 |
def xml_of_VectorString(strs: Vector[java.lang.String]): XML.Tree = {
|
wneuper@4848
|
105 |
XML.Elem(("STRINGLIST", Nil),
|
wneuper@4771
|
106 |
strs.asScala.toList map xml_of_str)
|
wneuper@4771
|
107 |
}
|
wneuper@4787
|
108 |
def xml_to_VectorTactic (t: XML.Tree): Vector[Tactic] = t match {
|
wneuper@4848
|
109 |
case XML.Elem(("TACLIST", Nil), tacs_xml) => {
|
wneuper@4787
|
110 |
val v = new java.util.Vector[Tactic];
|
wneuper@4787
|
111 |
tacs_xml.foreach { tac_xml => v.add(xml_to_Tactic(tac_xml)) }
|
wneuper@4787
|
112 |
v
|
wneuper@4787
|
113 |
}
|
wneuper@4787
|
114 |
case _ => throw new IllegalArgumentException("xml_to_VectorTactic wrong arg: " + t)
|
wneuper@4787
|
115 |
}
|
wneuper@4787
|
116 |
|
wneuper@4758
|
117 |
// Note: java.int-->scala.BigInt not done here, because "int" is unknown in Scala.
|
wneuper@4758
|
118 |
def Integer_to_BigInt (i: java.lang.Integer): scala.math.BigInt = {
|
wneuper@4771
|
119 |
new scala.math.BigInt(new BigInteger(i.toString)) //TODO: improve conversion ?
|
wneuper@4758
|
120 |
}
|
wneuper@4758
|
121 |
// UNUSED conversion scala.math.BigInt --> java.lang.Integer
|
wneuper@4758
|
122 |
def BigInt_to_Integer (i: scala.math.BigInt): java.lang.Integer = {
|
wneuper@4771
|
123 |
new java.lang.Integer(i.toString) //TODO: improve conversion ?
|
wneuper@4758
|
124 |
}
|
wneuper@4757
|
125 |
def xml_of_str (s: String): XML.Tree = {
|
wneuper@4848
|
126 |
XML.Elem(("STRING", Nil), List(XML.Text(s)))
|
wneuper@4757
|
127 |
}
|
wneuper@4757
|
128 |
def xml_to_str (t: XML.Tree): String = t match {
|
wneuper@4848
|
129 |
case XML.Elem(("STRING", Nil), List(XML.Text(s))) => s
|
wneuper@4757
|
130 |
case _ => throw new IllegalArgumentException("xml_to_str exn")
|
wneuper@4757
|
131 |
}
|
wneuper@4757
|
132 |
def xml_of_strs (ss: List[String]): XML.Tree = {
|
wneuper@4848
|
133 |
XML.Elem(("STRINGLIST", Nil), ss map xml_of_str)
|
wneuper@4757
|
134 |
}
|
wneuper@4757
|
135 |
def xml_to_strs (t: XML.Tree): List[String] = t match {
|
wneuper@4848
|
136 |
case XML.Elem(("STRINGLIST", Nil), ss) => ss map xml_to_str
|
wneuper@4757
|
137 |
case _ => throw new IllegalArgumentException("xml_to_strs exn")
|
wneuper@4757
|
138 |
}
|
wneuper@4757
|
139 |
def xml_of_spec (thy: String, pbl: ArrayList[String], met: ArrayList[String]): XML.Tree = {
|
wneuper@4848
|
140 |
XML.Elem(("SPECIFICATION", Nil), List(
|
wneuper@4848
|
141 |
XML.Elem(("THEORYID", Nil), List(XML.Text(thy))),
|
wneuper@4848
|
142 |
XML.Elem(("PROBLEMID", Nil), List(xml_of_strs(pbl.asScala.toList))),
|
wneuper@4848
|
143 |
XML.Elem(("METHODID", Nil), List(xml_of_strs(met.asScala.toList)))))
|
wneuper@4757
|
144 |
}
|
wneuper@4757
|
145 |
def xml_to_spec (t: XML.Tree) = t match {
|
wneuper@4848
|
146 |
case XML.Elem(("SPECIFICATION", Nil), List(
|
wneuper@4848
|
147 |
XML.Elem(("THEORYID", Nil), List(XML.Text(thy))),
|
wneuper@4848
|
148 |
XML.Elem(("PROBLEMID", Nil), List(pbl)),
|
wneuper@4848
|
149 |
XML.Elem(("METHODID", Nil), List(met)))) =>
|
wneuper@4759
|
150 |
(thy, DataTypes.xml_to_strs(pbl), xml_to_strs(met))
|
wneuper@4757
|
151 |
case _ => throw new IllegalArgumentException("xml_to_spec exn")
|
wneuper@4757
|
152 |
}
|
wneuper@4759
|
153 |
def xml_to_VectorInteger (t: XML.Tree): Vector[java.lang.Integer] = t match {
|
wneuper@4848
|
154 |
case XML.Elem(("INTLIST", Nil), is) => {
|
wneuper@4759
|
155 |
val v = new java.util.Vector[java.lang.Integer];
|
wneuper@4759
|
156 |
is.foreach {
|
wneuper@4848
|
157 |
case (XML.Elem(("INT", Nil), List(XML.Text(i))))
|
wneuper@4759
|
158 |
=> v.add(new java.lang.Integer(i))
|
wneuper@4759
|
159 |
case _ => throw new IllegalArgumentException("xml_to_VectorInteger 1 wrong arg: " + t)
|
wneuper@4759
|
160 |
}
|
wneuper@4759
|
161 |
v
|
wneuper@4759
|
162 |
}
|
wneuper@4759
|
163 |
case _ => throw new IllegalArgumentException("xml_to_VectorInteger 2 wrong arg: " + t)
|
wneuper@4759
|
164 |
}
|
wneuper@4759
|
165 |
def sListToVectorCalcFormula (forms: List[CalcFormula]): Vector[CalcFormula] = {
|
wneuper@4759
|
166 |
val v = new java.util.Vector[CalcFormula];
|
wneuper@4759
|
167 |
forms.foreach { form => v.add(form) }
|
wneuper@4759
|
168 |
v
|
wneuper@4759
|
169 |
}
|
wneuper@4787
|
170 |
def sListToVectorFormula (forms: List[Formula]): Vector[Formula] = {
|
wneuper@4787
|
171 |
val v = new java.util.Vector[Formula];
|
wneuper@4787
|
172 |
forms.foreach { form => v.add(form) }
|
wneuper@4787
|
173 |
v
|
wneuper@4787
|
174 |
}
|
wneuper@4789
|
175 |
def sListToVectorFormulaPair (forms: List[FormulaPair]): Vector[FormulaPair] = {
|
wneuper@4789
|
176 |
val v = new java.util.Vector[FormulaPair];
|
wneuper@4789
|
177 |
forms.foreach { form => v.add(form) }
|
wneuper@4789
|
178 |
v
|
wneuper@4789
|
179 |
}
|
wneuper@4759
|
180 |
def xml_to_String (t: XML.Tree): java.lang.String = t match {
|
wneuper@4759
|
181 |
case XML.Text(str) => str
|
wneuper@4789
|
182 |
case _ => throw new IllegalArgumentException("xml_to_String wrong arg: " + t)
|
wneuper@4759
|
183 |
}
|
wneuper@4789
|
184 |
def xml_of_term (str: String): XML.Tree = {
|
wneuper@4848
|
185 |
XML.Elem(("MATHML", Nil), List(
|
wneuper@4848
|
186 |
XML.Elem(("ISA", Nil), List(XML.Text(str)))))
|
wneuper@4771
|
187 |
}
|
wneuper@4789
|
188 |
def xml_to_term (t: XML.Tree): java.lang.String = t match {
|
wneuper@4789
|
189 |
case
|
wneuper@4848
|
190 |
XML.Elem(("MATHML", Nil), List(
|
wneuper@4848
|
191 |
XML.Elem(("ISA", Nil), List(XML.Text(str)))))
|
wneuper@4789
|
192 |
=> str
|
wneuper@4789
|
193 |
case _ => throw new IllegalArgumentException("xml_to_term wrong arg: " + t)
|
wneuper@4789
|
194 |
}
|
wneuper@4932
|
195 |
def xml_of_Term (t: Term): XML.Tree =
|
wneuper@4932
|
196 |
XML.Elem(("MATHML", Nil), List(
|
wneuper@4932
|
197 |
XML.Elem(("ISA", Nil), List(XML.Text(Util.string_of(t)))),
|
wneuper@4932
|
198 |
XML.Elem(("TERM", Nil), List(Codec[Term].encode(t)))))
|
wneuper@4932
|
199 |
|
wneuper@4842
|
200 |
def xml_to_prog (t: XML.Tree): java.lang.String = t match {
|
wneuper@4842
|
201 |
case
|
wneuper@4848
|
202 |
XML.Elem(("NOCODE", Nil), List(XML.Text(str)))
|
wneuper@4842
|
203 |
=> str
|
wneuper@4842
|
204 |
case
|
wneuper@4848
|
205 |
XML.Elem(("CODE", Nil), List(term_xml))
|
wneuper@4842
|
206 |
=> xml_to_term(term_xml)
|
wneuper@4842
|
207 |
case _ => throw new IllegalArgumentException("xml_to_prog wrong arg: " + t)
|
wneuper@4842
|
208 |
}
|
wneuper@4771
|
209 |
|
wneuper@4759
|
210 |
/**
|
wneuper@4759
|
211 |
* conversion XML <--> Java-objects in isac-java used by libisabelle
|
wneuper@4759
|
212 |
**/
|
wneuper@4758
|
213 |
|
wneuper@4781
|
214 |
// <--ISA carries a "status" computed by Math_Engine
|
wneuper@4781
|
215 |
def xml_to_ModelItem(t: XML.Tree): isac.util.formulae.ModelItem = t match {
|
wneuper@4759
|
216 |
case
|
wneuper@4848
|
217 |
XML.Elem(("ITEM", List(("status", status))), List(
|
wneuper@4848
|
218 |
XML.Elem(("MATHML", Nil), List(
|
wneuper@4848
|
219 |
XML.Elem(("ISA", Nil), List(XML.Text(form_isa)))))))
|
wneuper@4759
|
220 |
=> new ModelItem(status, form_isa)
|
wneuper@4759
|
221 |
case _ => throw new IllegalArgumentException("xml_to_ModelItem wrong arg: " + t)
|
wneuper@4759
|
222 |
}
|
wneuper@4781
|
223 |
// -->ISA carries NO "status" coming from user.
|
wneuper@4770
|
224 |
def xml_of_ModelItem(item: ModelItem): XML.Tree = {
|
wneuper@4848
|
225 |
XML.Elem(("ITEM", Nil), List(
|
wneuper@4848
|
226 |
XML.Elem(("MATHML", Nil), List(
|
wneuper@4848
|
227 |
XML.Elem(("ISA", Nil), List(XML.Text(item.getFormula.toSMLString)))))))
|
wneuper@4770
|
228 |
}
|
wneuper@4759
|
229 |
def sList2jVectorModelItem(ilist: List[ModelItem]): Vector[ModelItem] = {
|
wneuper@4771
|
230 |
val ivect = new Vector[ModelItem]
|
wneuper@4759
|
231 |
for (n <- 0 to ilist.size - 1) ivect.add(ilist(n))
|
wneuper@4759
|
232 |
ivect
|
wneuper@4759
|
233 |
}
|
wneuper@4759
|
234 |
//for test on console:
|
wneuper@4759
|
235 |
def sList2jVector(ilist: List[Integer]): Vector[Integer] = {
|
wneuper@4771
|
236 |
val ivect = new Vector[Integer]
|
wneuper@4759
|
237 |
for (n <- 0 to ilist.size - 1) ivect.add(ilist(n))
|
wneuper@4759
|
238 |
ivect
|
wneuper@4759
|
239 |
}
|
wneuper@4759
|
240 |
def xml_to_VectorModelItem(t: XML.Tree): java.util.Vector[ModelItem] = t match {
|
wneuper@4759
|
241 |
case
|
wneuper@4848
|
242 |
XML.Elem(("GIVEN", Nil), list_xml)
|
wneuper@4759
|
243 |
=> sList2jVectorModelItem(list_xml map xml_to_ModelItem)
|
wneuper@4759
|
244 |
case
|
wneuper@4848
|
245 |
XML.Elem(("WHERE", Nil), list_xml)
|
wneuper@4759
|
246 |
=> sList2jVectorModelItem(list_xml map xml_to_ModelItem)
|
wneuper@4759
|
247 |
case
|
wneuper@4848
|
248 |
XML.Elem(("FIND", Nil), list_xml)
|
wneuper@4759
|
249 |
=> sList2jVectorModelItem(list_xml map xml_to_ModelItem)
|
wneuper@4759
|
250 |
case
|
wneuper@4848
|
251 |
XML.Elem(("RELATE", Nil), list_xml)
|
wneuper@4759
|
252 |
=> sList2jVectorModelItem(list_xml map xml_to_ModelItem)
|
wneuper@4759
|
253 |
case _ => throw new IllegalArgumentException("xml_to_VectorModelItem wrong arg: " + t)
|
wneuper@4759
|
254 |
}
|
wneuper@4759
|
255 |
def xml_to_Model(t: XML.Tree): Model = t match {
|
wneuper@4759
|
256 |
case
|
wneuper@4848
|
257 |
XML.Elem(("MODEL", Nil), List(xml_given, xml_where, xml_find, xml_relate))
|
wneuper@4759
|
258 |
=> new Model(
|
wneuper@4759
|
259 |
new ModelItemList(xml_to_VectorModelItem(xml_given)),
|
wneuper@4759
|
260 |
new ModelItemList(xml_to_VectorModelItem(xml_where)),
|
wneuper@4759
|
261 |
new ModelItemList(xml_to_VectorModelItem(xml_find)),
|
wneuper@4759
|
262 |
new ModelItemList(xml_to_VectorModelItem(xml_relate)))
|
wneuper@4759
|
263 |
case _ => throw new IllegalArgumentException("xml_to_Model wrong arg: " + t)
|
wneuper@4759
|
264 |
}
|
wneuper@4781
|
265 |
//
|
wneuper@4781
|
266 |
// status (coming from user) is irrelevant: status is computed by Math_Engine
|
wneuper@4781
|
267 |
def xml_of_Item(item: ModelItem): XML.Tree = {
|
wneuper@4848
|
268 |
XML.Elem(("ITEM", Nil), List(
|
wneuper@4781
|
269 |
xml_of_term(item.getFormula.toString)))
|
wneuper@4781
|
270 |
}
|
wneuper@4781
|
271 |
def xml_of_items(tag: String, items: java.util.Vector[ModelItem]): XML.Tree = {
|
wneuper@4781
|
272 |
var xml: List[XML.Tree] = List()
|
wneuper@4781
|
273 |
for (n <- 0 to items.size - 1) { ((xml_of_Item(items.elementAt(n))) :: xml) }
|
wneuper@4848
|
274 |
XML.Elem((tag, Nil), xml.reverse)
|
wneuper@4781
|
275 |
}
|
wneuper@4781
|
276 |
// status (coming from user) is irrelevant: status is computed by Math_Engine
|
wneuper@4781
|
277 |
def xml_of_Model(model: Model): XML.Tree = {
|
wneuper@4848
|
278 |
XML.Elem(("MODEL", Nil), List(
|
wneuper@4781
|
279 |
xml_of_items("GIVEN", model.getGiven.getItems),
|
wneuper@4781
|
280 |
// xml_where, is never input by user
|
wneuper@4781
|
281 |
xml_of_items("FIND", model.getFind.getItems),
|
wneuper@4781
|
282 |
xml_of_items("RELATE", model.getRelate.getItems)
|
wneuper@4781
|
283 |
))
|
wneuper@4781
|
284 |
}
|
wneuper@4759
|
285 |
|
wneuper@4759
|
286 |
def xml_to_Specification(t: XML.Tree): isac.util.formulae.Specification = t match {
|
wneuper@4759
|
287 |
case
|
wneuper@4848
|
288 |
XML.Elem(("SPECIFICATION", Nil), List(
|
wneuper@4848
|
289 |
XML.Elem(("THEORYID", Nil), List(xml_thy)),
|
wneuper@4848
|
290 |
XML.Elem(("PROBLEMID", Nil), List(xml_pbl)),
|
wneuper@4848
|
291 |
XML.Elem(("METHODID", Nil), List(xml_met))))
|
wneuper@4771
|
292 |
=> { val thy_key = new CalcHeadSimpleID
|
wneuper@4759
|
293 |
thy_key.setID(DataTypes.xml_to_String(xml_thy))
|
wneuper@4771
|
294 |
val pbl_key = new HierarchyKey
|
wneuper@4771
|
295 |
pbl_key.setID(xml_to_VectorString(xml_pbl))
|
wneuper@4771
|
296 |
val met_key = new HierarchyKey
|
wneuper@4771
|
297 |
met_key.setID(xml_to_VectorString(xml_met))
|
wneuper@4759
|
298 |
new Specification(thy_key, pbl_key, met_key)
|
wneuper@4759
|
299 |
}
|
wneuper@4759
|
300 |
case _ => throw new IllegalArgumentException("xml_to_Specification wrong arg: " + t)
|
wneuper@4759
|
301 |
}
|
wneuper@4759
|
302 |
|
wneuper@4759
|
303 |
def xml_to_CalcHead(t: XML.Tree): CalcHead = t match {
|
wneuper@4759
|
304 |
case
|
wneuper@4848
|
305 |
XML.Elem(("CALCHEAD", List(("status", status))), List(
|
wneuper@4759
|
306 |
xml_pos, xml_head, xml_model,
|
wneuper@4848
|
307 |
XML.Elem(("BELONGSTO", Nil), List(XML.Text(pbl_met))),
|
wneuper@4759
|
308 |
xml_spec))
|
wneuper@4928
|
309 |
=> {
|
wneuper@4928
|
310 |
println("1a xml_to_CalcHead "+xml_head);
|
wneuper@4928
|
311 |
println("1b xml_to_CalcHead "+DataTypes.xml_to_Head(xml_head));
|
wneuper@4787
|
312 |
new CalcHead(DataTypes.xml_to_Position(xml_pos),
|
wneuper@4928
|
313 |
DataTypes.xml_to_Head(xml_head), xml_to_Model(xml_model),
|
wneuper@4759
|
314 |
pbl_met, xml_to_Specification(xml_spec), status)
|
wneuper@4759
|
315 |
}
|
wneuper@4759
|
316 |
case _ => throw new IllegalArgumentException("xml_to_CalcHead wrong arg: " + t)
|
wneuper@4759
|
317 |
}
|
wneuper@4770
|
318 |
def xml_of_CalcHead(chead: CalcHead): XML.Tree = {
|
wneuper@4848
|
319 |
XML.Elem(("CALCHEAD", List(("status", chead.getStatusString))), List(
|
wneuper@4771
|
320 |
xml_of_Position(chead.getPosition),
|
wneuper@4928
|
321 |
xml_of_Head(chead.getHeadLine),
|
wneuper@4781
|
322 |
xml_of_Model(chead.getModel),
|
wneuper@4848
|
323 |
XML.Elem(("BELONGSTO", Nil), List(XML.Text(chead.getBelongsTo))),
|
wneuper@4771
|
324 |
xml_of_Specification(chead.getSpecification)))
|
wneuper@4770
|
325 |
}
|
wneuper@4787
|
326 |
def xml_to_Formula(t: XML.Tree): isac.util.formulae.Formula = t match {
|
wneuper@4759
|
327 |
case
|
wneuper@4848
|
328 |
XML.Elem(("FORMULA", Nil), List(
|
wneuper@4848
|
329 |
XML.Elem(("MATHML", Nil), List(
|
wneuper@4848
|
330 |
XML.Elem(("ISA", Nil), List(XML.Text(form_isa)))))))
|
wneuper@4787
|
331 |
=> new Formula(form_isa)
|
wneuper@4928
|
332 |
case _ => throw new IllegalArgumentException("xml_to_Formula wrong arg: " + t)
|
wneuper@4928
|
333 |
}
|
wneuper@4928
|
334 |
def xml_to_Head(t: XML.Tree): isac.util.formulae.Formula = t match {
|
wneuper@4759
|
335 |
case
|
wneuper@4928
|
336 |
XML.Elem(("HEAD", Nil), List(form_xml)) => {
|
wneuper@4928
|
337 |
println("2a xml_to_Head "+"found HEAD");
|
wneuper@4928
|
338 |
xml_to_Formula_NEW(form_xml)
|
wneuper@4928
|
339 |
}
|
wneuper@4928
|
340 |
case _ => {
|
wneuper@4928
|
341 |
println("2b xml_to_Head "+"Exception");
|
wneuper@4928
|
342 |
throw new IllegalArgumentException("xml_to_Formula wrong arg: " + t)
|
wneuper@4928
|
343 |
}
|
wneuper@4759
|
344 |
}
|
wneuper@4853
|
345 |
def xml_to_Formula_NEW(t: XML.Tree): isac.util.formulae.Formula = t match {
|
wneuper@4853
|
346 |
case
|
wneuper@4928
|
347 |
XML.Elem(("FORMULA", Nil), List(
|
wneuper@4853
|
348 |
XML.Elem(("ISA", Nil), List(XML.Text(str))),
|
wneuper@4855
|
349 |
XML.Elem(("TERM", Nil), List(term))))
|
wneuper@5070
|
350 |
=> new Formula(str, Syntax_Phases.term_to_ast(Codec[Term].decode(term).right.get))
|
wneuper@4855
|
351 |
// TODO: catch exn which might be thrown by "right.get"
|
wneuper@4853
|
352 |
case _ => throw new IllegalArgumentException("xml_to_Formula_NEW wrong arg: " + t)
|
wneuper@4853
|
353 |
}
|
wneuper@5130
|
354 |
// for test purposes
|
wneuper@5130
|
355 |
def xml_to_Term(t: XML.Tree): Term = t match {
|
wneuper@5130
|
356 |
case
|
wneuper@5130
|
357 |
XML.Elem(("FORMULA", Nil), List(
|
wneuper@5130
|
358 |
XML.Elem(("ISA", Nil), List(XML.Text(str))),
|
wneuper@5130
|
359 |
XML.Elem(("TERM", Nil), List(term))))
|
wneuper@5130
|
360 |
=> Codec[Term].decode(term).right.get
|
wneuper@5130
|
361 |
// TODO: catch exn which might be thrown by "right.get"
|
wneuper@5130
|
362 |
case _ => throw new IllegalArgumentException("xml_to_Term wrong arg: " + t)
|
wneuper@5130
|
363 |
}
|
wneuper@5130
|
364 |
|
wneuper@4884
|
365 |
/*
|
wneuper@4884
|
366 |
* WN160512 presently there is no transport of Terms from the GUI to the MathEngine
|
wneuper@4884
|
367 |
* and it is questionable whether such transport will be implemented at all.
|
wneuper@4884
|
368 |
* So this method might take a String as argument (and send no TERM), like xml_of_Formula.
|
wneuper@4884
|
369 |
*/
|
wneuper@4916
|
370 |
def xml_of_Formula_UNUSED(form: Formula): XML.Tree = {
|
wneuper@4884
|
371 |
XML.Elem(("MATHML", Nil), List(
|
wneuper@4884
|
372 |
XML.Elem(("ISA", Nil), List(XML.Text("TODO form.getString() OR form.toSMLString()"))),
|
wneuper@5070
|
373 |
XML.Elem(("TERM", Nil), List(Codec[Term].encode(Syntax_Phases.ast_to_term(form.getTerm))))))
|
wneuper@4884
|
374 |
}
|
s1520454056@5120
|
375 |
/* TODO we plan to send both, String and Term to Isabelle_Isac.
|
s1520454056@5120
|
376 |
* In a later phase of development Isabelle_Isac will decide whether to use
|
s1520454056@5120
|
377 |
* either String or Term (after conversion from Ast).
|
s1520454056@5120
|
378 |
*/
|
wneuper@4916
|
379 |
def xml_of_Formula_NEW(form: Formula): XML.Tree = {
|
wneuper@4916
|
380 |
XML.Elem(("FORMULA", Nil), List(
|
s1520454056@5120
|
381 |
XML.Elem(("ISA", Nil), List(XML.Text(form.toString)))//,
|
s1520454056@5120
|
382 |
//XML.Elem(("TERM", Nil), List(Codec[Term].encode(Syntax_Phases.ast_to_term(form.getTerm))))
|
s1520454056@5120
|
383 |
))
|
wneuper@4916
|
384 |
}
|
wneuper@4787
|
385 |
def xml_of_Formula(form_isa: Formula): XML.Tree = {
|
wneuper@4848
|
386 |
XML.Elem(("FORMULA", Nil), List(
|
wneuper@4848
|
387 |
XML.Elem(("MATHML", Nil), List(
|
wneuper@4848
|
388 |
XML.Elem(("ISA", Nil), List(XML.Text(form_isa.toString)))))))
|
wneuper@4767
|
389 |
}
|
wneuper@4928
|
390 |
def xml_of_Head(head_isa: Formula): XML.Tree = {
|
wneuper@4928
|
391 |
XML.Elem(("HEAD", Nil), List(xml_of_Formula_NEW(head_isa)))
|
wneuper@4767
|
392 |
}
|
wneuper@4759
|
393 |
def xml_to_CalcFormula(t: XML.Tree): CalcFormula = t match {
|
wneuper@4759
|
394 |
case
|
wneuper@4848
|
395 |
XML.Elem(("CALCFORMULA", Nil), List(pos, form))
|
wneuper@4933
|
396 |
=> new CalcFormula(xml_to_Position(pos), xml_to_Formula_NEW(form))
|
wneuper@4759
|
397 |
case _ => throw new IllegalArgumentException("xml_to_CalcFormula wrong arg: " + t)
|
wneuper@4759
|
398 |
}
|
wneuper@4767
|
399 |
def xml_of_CalcFormula(calc_form: CalcFormula): XML.Tree = {
|
wneuper@4848
|
400 |
XML.Elem(("CALCFORMULA", Nil), List(
|
wneuper@4771
|
401 |
xml_of_Position(calc_form.getPosition),
|
wneuper@4771
|
402 |
xml_of_Formula(calc_form.getFormula)))
|
wneuper@4767
|
403 |
}
|
wneuper@4758
|
404 |
def xml_of_Formalization(fmz: Formalization): XML.Tree = {
|
wneuper@4892
|
405 |
if (fmz.getVariants.size == 0) { //..from <NEW> on GUI, then Isabelle/Isac expects..
|
wneuper@4892
|
406 |
XML.Elem(("FORMALIZATION", Nil), List(
|
wneuper@4892
|
407 |
XML.Elem(("VARIANT", Nil), List(
|
wneuper@4892
|
408 |
XML.Elem(("STRINGLIST", Nil), Nil),
|
wneuper@4892
|
409 |
XML.Elem(("SPECIFICATION", Nil), List(
|
wneuper@4892
|
410 |
XML.Elem(("THEORYID", Nil), List(XML.Text("e_domID"))),
|
wneuper@4892
|
411 |
XML.Elem(("PROBLEMID", Nil), List(
|
wneuper@4892
|
412 |
XML.Elem(("STRINGLIST", Nil), List(
|
wneuper@4892
|
413 |
XML.Elem(("STRING", Nil), List(XML.Text("e_pblID"))))))),
|
wneuper@4892
|
414 |
XML.Elem(("METHODID", Nil), List(
|
wneuper@4892
|
415 |
XML.Elem(("STRINGLIST", Nil), List(
|
wneuper@4892
|
416 |
XML.Elem(("STRING", Nil), List(XML.Text("e_metID")))))))))))))
|
wneuper@4892
|
417 |
} else {
|
wneuper@4892
|
418 |
XML.Elem(("FORMALIZATION", Nil), fmz.getVariants.asScala.toList map xml_of_Variant)
|
wneuper@4892
|
419 |
}
|
wneuper@4758
|
420 |
}
|
wneuper@4758
|
421 |
def xml_of_Position(pos: Position): XML.Tree = {
|
wneuper@4771
|
422 |
val is: List[Integer] = pos.getIntList.asInstanceOf[Vector[Integer]].asScala.toList
|
wneuper@4771
|
423 |
xml_of_pos(is map Integer_to_BigInt, pos.getKind)
|
wneuper@4758
|
424 |
}
|
wneuper@4759
|
425 |
def xml_to_Position(t: XML.Tree): Position = t match {
|
wneuper@4759
|
426 |
case
|
wneuper@4848
|
427 |
XML.Elem(("POSITION", Nil), List(
|
wneuper@4848
|
428 |
ints, XML.Elem(("POS", Nil), List(XML.Text(kind)))))
|
wneuper@4759
|
429 |
=> new Position(xml_to_VectorInteger(ints), kind)
|
wneuper@4759
|
430 |
case _ => throw new IllegalArgumentException("xml_to_Position wrong arg: " + t)
|
wneuper@4759
|
431 |
}
|
wneuper@4758
|
432 |
def xml_of_Specification(spec: Specification): XML.Tree = {
|
wneuper@4848
|
433 |
XML.Elem(("SPECIFICATION", Nil), List(
|
wneuper@4848
|
434 |
XML.Elem(("THEORYID", Nil), List(XML.Text(spec.getTheory.getID))),
|
wneuper@4848
|
435 |
XML.Elem(("PROBLEMID", Nil), List(
|
wneuper@4771
|
436 |
DataTypes.xml_of_strs(spec.getProblem.getID.asScala.toList))),
|
wneuper@4848
|
437 |
XML.Elem(("METHODID", Nil), List(
|
wneuper@4771
|
438 |
DataTypes.xml_of_strs(spec.getMethod.getID.asScala.toList)))))
|
wneuper@4758
|
439 |
}
|
wneuper@4848
|
440 |
def xml_of_Variant(vat: isac.util.Variant): XML.Tree = {
|
wneuper@4848
|
441 |
XML.Elem(("VARIANT", Nil), List(
|
wneuper@4771
|
442 |
DataTypes.xml_of_strs(vat.getIsaStrings.asScala.toList),
|
wneuper@4771
|
443 |
xml_of_Specification(vat.getSpecification)))
|
wneuper@4758
|
444 |
}
|
wneuper@4848
|
445 |
def xml_of_ContextType(ctxt_typ: isac.wsdialog.IContextProvider.ContextType): XML.Tree = {
|
wneuper@4848
|
446 |
XML.Elem(("KETYPE", Nil), List(XML.Text(ctxt_typ.toString)))
|
wneuper@4771
|
447 |
}
|
wneuper@4771
|
448 |
|
wneuper@4932
|
449 |
// from isac-java to kernel goes only "ISA", no "TERM"
|
wneuper@4932
|
450 |
// repair: replace "FORMULA" by "ISA"
|
wneuper@4848
|
451 |
def xml_of_Theorem(thm: Theorem): XML.Tree = {
|
wneuper@4848
|
452 |
XML.Elem(("THEOREM", Nil), List(
|
wneuper@4848
|
453 |
XML.Elem(("ID", Nil), List(XML.Text(thm.getId))),
|
wneuper@4848
|
454 |
XML.Elem(("FORMULA", Nil), List(
|
wneuper@4771
|
455 |
XML.Text(thm.getFormula))))) // term instead String for MathML
|
wneuper@4771
|
456 |
}
|
wneuper@4932
|
457 |
// from isac-java to kernel goes only "ISA", no "TERM"
|
wneuper@4932
|
458 |
// repair: replace "FORMULA" by "ISA"
|
wneuper@4771
|
459 |
def xml_to_Theorem(t: XML.Tree): Theorem = t match {
|
wneuper@4771
|
460 |
case
|
wneuper@4848
|
461 |
XML.Elem(("THEOREM", Nil), List(
|
wneuper@4848
|
462 |
XML.Elem(("ID", Nil), List(XML.Text(id))),
|
wneuper@4848
|
463 |
XML.Elem(("FORMULA", Nil), List(
|
wneuper@4771
|
464 |
XML.Text(form))))) // term instead String for MathML
|
wneuper@4771
|
465 |
=> new Theorem(id, form)
|
wneuper@4771
|
466 |
case x => throw new IllegalArgumentException("xml_to_Theorem WRONG arg = " + x)
|
wneuper@4771
|
467 |
}
|
wneuper@4771
|
468 |
|
wneuper@4771
|
469 |
//----- FOR xml_of_Tactic --------------------------------------------*)
|
wneuper@4848
|
470 |
def xml_of_SubProblemTactic(tac: SubProblemTactic): XML.Tree = {
|
wneuper@4848
|
471 |
XML.Elem(("SUBPROBLEMTACTIC", List(("name", tac.getName))), List(
|
wneuper@4848
|
472 |
XML.Elem(("THEORY", Nil), List(XML.Text(tac.getTheoryID))),
|
wneuper@4848
|
473 |
XML.Elem(("PROBLEM", Nil), List(xml_of_VectorString(tac.getProblemID)))))
|
wneuper@4771
|
474 |
}
|
wneuper@4771
|
475 |
// Substitute see //----- STRINGLISTTACTIC below
|
wneuper@4771
|
476 |
|
wneuper@4771
|
477 |
//----- Rewrite* -----------------------------------------------------*)
|
wneuper@4848
|
478 |
def xml_of_Rewrite(tac: Rewrite): XML.Tree = {
|
wneuper@4848
|
479 |
XML.Elem(("REWRITETACTIC", List(("name", tac.getName))), List(
|
wneuper@4771
|
480 |
xml_of_Theorem(tac.getTheorem)))
|
wneuper@4771
|
481 |
}
|
wneuper@4848
|
482 |
def xml_of_RewriteInst(tac: RewriteInst): XML.Tree = {
|
wneuper@4848
|
483 |
XML.Elem(("REWRITEINSTTACTIC", List(("name", tac.getName))), List(
|
wneuper@4771
|
484 |
//this will be generalised at introduction of MathML
|
wneuper@4848
|
485 |
XML.Elem(("PAIR", Nil), List(
|
wneuper@4848
|
486 |
XML.Elem(("VARIABLE", Nil), List(
|
wneuper@4848
|
487 |
XML.Elem(("MATHML", Nil), List(
|
wneuper@4848
|
488 |
XML.Elem(("ISA", Nil), List(XML.Text(tac.getVariable))))))),
|
wneuper@4848
|
489 |
XML.Elem(("VALUE", Nil), List(
|
wneuper@4848
|
490 |
XML.Elem(("MATHML", Nil), List(
|
wneuper@4848
|
491 |
XML.Elem(("ISA", Nil), List(XML.Text(tac.getValue))))))))),
|
wneuper@4771
|
492 |
xml_of_Theorem(tac.getTheorem)))
|
wneuper@4771
|
493 |
}
|
wneuper@4848
|
494 |
def xml_of_RewriteSet(tac: RewriteSet): XML.Tree = {
|
wneuper@4848
|
495 |
XML.Elem(("REWRITESETTACTIC", List(("name", tac.getName))), List(
|
wneuper@4771
|
496 |
XML.Text(tac.getRuleSet)))
|
wneuper@4771
|
497 |
}
|
wneuper@4848
|
498 |
def xml_of_RewriteSetInst(tac: RewriteSetInst): XML.Tree = {
|
wneuper@4848
|
499 |
XML.Elem(("REWRITESETINSTTACTIC", List(("name", tac.getName))), List(
|
wneuper@4771
|
500 |
//this will be generalised at introduction of MathML
|
wneuper@4848
|
501 |
XML.Elem(("PAIR", Nil), List(
|
wneuper@4848
|
502 |
XML.Elem(("VARIABLE", Nil), List(
|
wneuper@4848
|
503 |
XML.Elem(("MATHML", Nil), List(
|
wneuper@4848
|
504 |
XML.Elem(("ISA", Nil), List(XML.Text(tac.getVariable))))))),
|
wneuper@4848
|
505 |
XML.Elem(("VALUE", Nil), List(
|
wneuper@4848
|
506 |
XML.Elem(("MATHML", Nil), List(
|
wneuper@4848
|
507 |
XML.Elem(("ISA", Nil), List(XML.Text(tac.getValue))))))))),
|
wneuper@4771
|
508 |
XML.Text(tac.getRuleSet)))
|
wneuper@4770
|
509 |
}
|
wneuper@4758
|
510 |
|
wneuper@4771
|
511 |
//----- FORMTACTIC ---------------------------------------------------*)
|
wneuper@4848
|
512 |
def xml_of_TermTactic(formtac: TermTactic): XML.Tree = {
|
wneuper@4848
|
513 |
XML.Elem(("FORMTACTIC", List(("name", formtac.getName))), List(
|
wneuper@4810
|
514 |
xml_of_term(formtac.getTerm)))
|
wneuper@4771
|
515 |
}
|
wneuper@4771
|
516 |
//----- SIMPLETACTIC -------------------------------------------------*)
|
wneuper@4848
|
517 |
def xml_of_SimpleTactic(tac: SimpleTactic): XML.Tree = {
|
wneuper@4848
|
518 |
XML.Elem(("SIMPLETACTIC", List(("name", tac.getName))), List(
|
wneuper@4771
|
519 |
xml_of_term(tac.getArgument)))
|
wneuper@4771
|
520 |
}
|
wneuper@4771
|
521 |
//----- STRINGLISTTACTIC ---------------------------------------------*)
|
wneuper@4771
|
522 |
def dest_eq(equality: String): (String, String) = {
|
wneuper@4771
|
523 |
val pair = equality.split("=")
|
wneuper@4771
|
524 |
if (pair.length == 2) (pair(0), pair(1))
|
wneuper@4771
|
525 |
else throw new IllegalArgumentException("dest_eq WRONG arg = " + equality)
|
wneuper@4771
|
526 |
}
|
wneuper@4771
|
527 |
def xml_of_val_var_pair(vv: (String, String)): XML.Tree = {
|
wneuper@4848
|
528 |
XML.Elem(("PAIR", Nil), List(
|
wneuper@4848
|
529 |
XML.Elem(("VARIABLE", Nil), List(
|
wneuper@4848
|
530 |
XML.Elem(("MATHML", Nil), List(
|
wneuper@4848
|
531 |
XML.Elem(("ISA", Nil), List(XML.Text(vv._1))))))),
|
wneuper@4848
|
532 |
XML.Elem(("VALUE", Nil), List(
|
wneuper@4848
|
533 |
XML.Elem(("MATHML", Nil), List(
|
wneuper@4848
|
534 |
XML.Elem(("ISA", Nil), List(XML.Text(vv._2)))))))))
|
wneuper@4771
|
535 |
}
|
wneuper@4771
|
536 |
def xml_of_sube(equs: Vector[String]): XML.Tree = {
|
wneuper@4848
|
537 |
XML.Elem(("SUBSTITUTION", Nil),
|
wneuper@4771
|
538 |
(equs.asScala.toList map dest_eq) map xml_of_val_var_pair)
|
wneuper@4771
|
539 |
}
|
wneuper@4848
|
540 |
def xml_of_StringListTactic(strs_tac: StringListTactic): XML.Tree = {
|
wneuper@4771
|
541 |
var xml = XML.Text("DUMMY"): XML.Tree
|
wneuper@4771
|
542 |
if (strs_tac.getName == "Substitute")
|
wneuper@4771
|
543 |
xml = xml_of_VectorString(strs_tac.getStrings)
|
wneuper@4771
|
544 |
else
|
wneuper@4771
|
545 |
xml = xml_of_VectorString(strs_tac.getStrings)
|
wneuper@4848
|
546 |
XML.Elem(("STRINGLISTTACTIC", List(("name", strs_tac.getName))), List(
|
wneuper@4771
|
547 |
xml))
|
wneuper@4771
|
548 |
}
|
wneuper@4848
|
549 |
// def xml_of_Tactic(tac: Tactic): XML.Tree = tac.getClass match {
|
wneuper@4781
|
550 |
// was shifted to DataTypesCompanion.java
|
wneuper@4771
|
551 |
def xml_to_Tactic(t: XML.Tree): Tactic = t match {
|
wneuper@4771
|
552 |
case
|
wneuper@4848
|
553 |
XML.Elem(("SUBPROBLEMTACTIC", List(("name", "Subproblem"))), List(
|
wneuper@4848
|
554 |
XML.Elem(("THEORY", Nil), List(XML.Text(thy))),
|
wneuper@4848
|
555 |
XML.Elem(("PROBLEM", Nil), List(pbl))))
|
wneuper@4771
|
556 |
=> new SubProblemTactic("Subproblem", thy, xml_to_VectorString(pbl))
|
wneuper@4771
|
557 |
case
|
wneuper@4848
|
558 |
XML.Elem(("STRINGLISTTACTIC", List(("name", "Substitute"))), List(
|
wneuper@4848
|
559 |
XML.Elem(("PAIR", Nil), List(
|
wneuper@4848
|
560 |
XML.Elem(("VARIABLE", Nil), List(
|
wneuper@4848
|
561 |
XML.Elem(("MATHML", Nil), List(
|
wneuper@4848
|
562 |
XML.Elem(("ISA", Nil), List(XML.Text(variable))))))),
|
wneuper@4848
|
563 |
XML.Elem(("VALUE", Nil), List(
|
wneuper@4848
|
564 |
XML.Elem(("MATHML", Nil), List(
|
wneuper@4848
|
565 |
XML.Elem(("ISA", Nil), List(XML.Text(value)))))))))))
|
wneuper@4771
|
566 |
=> new SubstituteTactic("Substitute", variable, value)
|
wneuper@4771
|
567 |
|
wneuper@4771
|
568 |
//----- Rewrite* -----------------------------------------------------*)
|
wneuper@4771
|
569 |
case
|
wneuper@4848
|
570 |
XML.Elem(("REWRITETACTIC", List(("name", "Rewrite"))), List(
|
wneuper@4771
|
571 |
thm))
|
wneuper@4771
|
572 |
=> new Rewrite("Rewrite", xml_to_Theorem(thm))
|
wneuper@4771
|
573 |
case // faked until introduction of MathML
|
wneuper@4848
|
574 |
XML.Elem(("REWRITEINSTTACTIC", List(("name", "Rewrite_Inst"))), List(
|
wneuper@4848
|
575 |
XML.Elem(("SUBSTITUTION", Nil), List(
|
wneuper@4848
|
576 |
XML.Elem(("PAIR", Nil), List(
|
wneuper@4848
|
577 |
XML.Elem(("VARIABLE", Nil), List(
|
wneuper@4848
|
578 |
XML.Elem(("MATHML", Nil), List(
|
wneuper@4848
|
579 |
XML.Elem(("ISA", Nil), List(XML.Text(variable))))))),
|
wneuper@4848
|
580 |
XML.Elem(("VALUE", Nil), List(
|
wneuper@4848
|
581 |
XML.Elem(("MATHML", Nil), List(
|
wneuper@4848
|
582 |
XML.Elem(("ISA", Nil), List(XML.Text(value)))))))
|
wneuper@4771
|
583 |
)))),
|
wneuper@4771
|
584 |
thm))
|
wneuper@4771
|
585 |
=> new RewriteInst("Rewrite_Inst", variable, value, xml_to_Theorem(thm))
|
wneuper@4771
|
586 |
case
|
wneuper@4848
|
587 |
XML.Elem(("REWRITESETTACTIC", List(("name", "Rewrite_Set"))), List(
|
wneuper@4771
|
588 |
XML.Text(rule_set)))
|
wneuper@4771
|
589 |
=> new RewriteSet("Rewrite_Set", rule_set)
|
wneuper@4810
|
590 |
case // faked Term by String until introduction of MathML
|
wneuper@4848
|
591 |
XML.Elem(("REWRITESETINSTTACTIC", List(("name", "Rewrite_Set_Inst"))), List(
|
wneuper@4848
|
592 |
XML.Elem(("SUBSTITUTION", Nil), List(
|
wneuper@4848
|
593 |
XML.Elem(("PAIR", Nil), List(
|
wneuper@4848
|
594 |
XML.Elem(("VARIABLE", Nil), List(
|
wneuper@4848
|
595 |
XML.Elem(("MATHML", Nil), List(
|
wneuper@4848
|
596 |
XML.Elem(("ISA", Nil), List(XML.Text(variable))))))),
|
wneuper@4848
|
597 |
XML.Elem(("VALUE", Nil), List(
|
wneuper@4848
|
598 |
XML.Elem(("MATHML", Nil), List(
|
wneuper@4848
|
599 |
XML.Elem(("ISA", Nil), List(XML.Text(value))))))))))),
|
wneuper@4848
|
600 |
XML.Elem(("RULESET", Nil), List(XML.Text(rule_set)))))
|
wneuper@4810
|
601 |
// ATTENTION: args--vv are shuffled wrt. RewriteInst
|
wneuper@4771
|
602 |
=> new RewriteSetInst("Rewrite_Set_Inst", rule_set, variable, value)
|
wneuper@4771
|
603 |
|
wneuper@4771
|
604 |
//----- FORMTACTIC ---------------------------------------------------*)
|
wneuper@4771
|
605 |
case
|
wneuper@4848
|
606 |
XML.Elem(("FORMTACTIC", List(("name", "Add_Find"))), List(
|
wneuper@4810
|
607 |
term))
|
wneuper@4810
|
608 |
=> new TermTactic("Add_Find", xml_to_term(term))
|
wneuper@4771
|
609 |
case
|
wneuper@4848
|
610 |
XML.Elem(("FORMTACTIC", List(("name", "Add_Given"))), List(
|
wneuper@4810
|
611 |
term))
|
wneuper@4810
|
612 |
=> new TermTactic("Add_Given", xml_to_term(term))
|
wneuper@4771
|
613 |
case
|
wneuper@4848
|
614 |
XML.Elem(("FORMTACTIC", List(("name", "Add_Relation"))), List(
|
wneuper@4810
|
615 |
term))
|
wneuper@4810
|
616 |
=> new TermTactic("Add_Relation", xml_to_term(term))
|
wneuper@4771
|
617 |
case
|
wneuper@4848
|
618 |
XML.Elem(("FORMTACTIC", List(("name", "Check_elementwise"))), List(
|
wneuper@4810
|
619 |
term))
|
wneuper@4810
|
620 |
=> new TermTactic("Check_elementwise", xml_to_term(term))
|
wneuper@4771
|
621 |
case
|
wneuper@4848
|
622 |
XML.Elem(("FORMTACTIC", List(("name", "Take"))), List(
|
wneuper@4810
|
623 |
term))
|
wneuper@4810
|
624 |
=> new TermTactic("Take", xml_to_term(term))
|
wneuper@4771
|
625 |
|
wneuper@4771
|
626 |
//----- SIMPLETACTIC -------------------------------------------------*)
|
wneuper@4771
|
627 |
case
|
wneuper@4848
|
628 |
XML.Elem(("SIMPLETACTIC", List(("name", "Or_to_List"))), List(
|
wneuper@4771
|
629 |
XML.Text(_)))
|
wneuper@4787
|
630 |
=> new SimpleTactic("Or_to_List", "DUMMY")
|
wneuper@4771
|
631 |
case
|
wneuper@4848
|
632 |
XML.Elem(("SIMPLETACTIC", List(("name", "Specify_Theory"))), List(
|
wneuper@4771
|
633 |
XML.Text(str)))
|
wneuper@4787
|
634 |
=> new SimpleTactic("Specify_Theory", str)
|
wneuper@4771
|
635 |
|
wneuper@4771
|
636 |
//----- STRINGLISTTACTIC ---------------------------------------------*)
|
wneuper@4771
|
637 |
case
|
wneuper@4848
|
638 |
XML.Elem(("STRINGLISTTACTIC", List(("name", "Apply_Method"))), List(
|
wneuper@4771
|
639 |
strs))
|
wneuper@4771
|
640 |
=> new StringListTactic("Apply_Method", xml_to_VectorString(strs))
|
wneuper@4771
|
641 |
case
|
wneuper@4848
|
642 |
XML.Elem(("STRINGLISTTACTIC", List(("name", "Check_Postcond"))), List(
|
wneuper@4771
|
643 |
strs))
|
wneuper@4771
|
644 |
=> new StringListTactic("Check_Postcond", xml_to_VectorString(strs))
|
wneuper@4771
|
645 |
case
|
wneuper@4848
|
646 |
XML.Elem(("STRINGLISTTACTIC", List(("name", "Model_Problem"))), List(
|
wneuper@4771
|
647 |
strs))
|
wneuper@4771
|
648 |
=> new StringListTactic("Model_Problem", xml_to_VectorString(strs))
|
wneuper@4771
|
649 |
case
|
wneuper@4848
|
650 |
XML.Elem(("STRINGLISTTACTIC", List(("name", "Refine_Tacitly"))), List(
|
wneuper@4771
|
651 |
strs))
|
wneuper@4771
|
652 |
=> new StringListTactic("Refine_Tacitly", xml_to_VectorString(strs))
|
wneuper@4771
|
653 |
case
|
wneuper@4848
|
654 |
XML.Elem(("STRINGLISTTACTIC", List(("name", "Specify_Method"))), List(
|
wneuper@4771
|
655 |
strs))
|
wneuper@4771
|
656 |
=> new StringListTactic("Specify_Method", xml_to_VectorString(strs))
|
wneuper@4771
|
657 |
case
|
wneuper@4848
|
658 |
XML.Elem(("STRINGLISTTACTIC", List(("name", "Specify_Problem"))), List(
|
wneuper@4771
|
659 |
strs))
|
wneuper@4771
|
660 |
=> new StringListTactic("Specify_Problem", xml_to_VectorString(strs))
|
wneuper@4771
|
661 |
case x => throw new IllegalArgumentException("xml_to_Tactic WRONG arg = " + x)
|
wneuper@4771
|
662 |
}
|
wneuper@4771
|
663 |
|
wneuper@4787
|
664 |
//------- for xml_of_contthy
|
wneuper@4787
|
665 |
//--- see Isabelle/Isac:../datatypes.sml
|
wneuper@4789
|
666 |
def xml_to_Reference(t: XML.Tree): Reference = t match {
|
wneuper@4787
|
667 |
case
|
wneuper@4848
|
668 |
XML.Elem(("KESTOREREF", Nil), List(
|
wneuper@4848
|
669 |
XML.Elem(("TAG", Nil), List(XML.Text(tag))),
|
wneuper@4848
|
670 |
XML.Elem(("ID", Nil), List(XML.Text(xstring))),
|
wneuper@4848
|
671 |
XML.Elem(("GUH", Nil), List(XML.Text(guh)))))
|
wneuper@4789
|
672 |
=> new Reference(tag, xstring, new KEStoreKey(guh))
|
wneuper@4789
|
673 |
case t => throw new IllegalArgumentException("xml_to_Reference wrong arg: " + t)
|
wneuper@4787
|
674 |
}
|
wneuper@4757
|
675 |
|
wneuper@4789
|
676 |
def xml_to_asm_val(t: XML.Tree): FormulaPair = t match {
|
wneuper@4787
|
677 |
case
|
wneuper@4848
|
678 |
XML.Elem(("ASMEVALUATED", Nil), List(
|
wneuper@4848
|
679 |
XML.Elem(("ASM", Nil), List(asm)),
|
wneuper@4848
|
680 |
XML.Elem(("VALUE", Nil), List(vl))))
|
wneuper@4789
|
681 |
=> new FormulaPair(new Formula(xml_to_term(asm)), /*new Formula((xml_to_term(vl)))*/true)
|
wneuper@4789
|
682 |
case t => throw new IllegalArgumentException("xml_to_asm_val wrong arg: " + t)
|
wneuper@4789
|
683 |
}
|
wneuper@4825
|
684 |
def xml_to_ContextTheory(t: XML.Tree): ContextTheory = t match {
|
wneuper@4789
|
685 |
// | xml_of_contthy (ContThm {thyID, thm, applto, applat, reword,
|
wneuper@4789
|
686 |
// asms,lhs, rhs, result, resasms, asmrls}) =
|
wneuper@4789
|
687 |
case
|
wneuper@4848
|
688 |
XML.Elem(("CONTEXTDATA", Nil), List(
|
wneuper@4848
|
689 |
XML.Elem(("GUH", Nil), List(XML.Text(guh))),
|
wneuper@4848
|
690 |
XML.Elem(("APPLTO", Nil), List(applto_xml)),
|
wneuper@4848
|
691 |
XML.Elem(("APPLAT", Nil), List(applat_xml)),
|
wneuper@4848
|
692 |
XML.Elem(("ORDER", Nil), List(
|
wneuper@4848
|
693 |
XML.Elem(("ID", Nil), List(XML.Text(reword))))),
|
wneuper@4848
|
694 |
XML.Elem(("ASMSEVAL", Nil), asmevs_xml), //Nil is possible
|
wneuper@4848
|
695 |
XML.Elem(("LHS", Nil), List(lhs_xml)),
|
wneuper@4848
|
696 |
XML.Elem(("LHSINST", Nil), List(lhsinst_xml)),
|
wneuper@4848
|
697 |
XML.Elem(("RHS", Nil), List(rhs_xml)),
|
wneuper@4848
|
698 |
XML.Elem(("RHSINST", Nil), List(rhsinst_xml)),
|
wneuper@4848
|
699 |
XML.Elem(("RESULT", Nil), List(result_xml)),
|
wneuper@4848
|
700 |
XML.Elem(("ASSUMPTIONS", Nil), asms_xml), //Nil is possible
|
wneuper@4848
|
701 |
XML.Elem(("EVALRLS", Nil), List(rlskey_xml))))
|
wneuper@4832
|
702 |
=> new ContextTheory(new KEStoreKey(guh),
|
wneuper@4789
|
703 |
null, null,
|
wneuper@4789
|
704 |
new Formula(xml_to_term(applto_xml)), new Formula(xml_to_term(applat_xml)),
|
wneuper@4789
|
705 |
reword,
|
wneuper@4789
|
706 |
sListToVectorFormulaPair(asmevs_xml map xml_to_asm_val), //WN150820 bug: Boolean form_2
|
wneuper@4789
|
707 |
new Formula(xml_to_term(lhs_xml)), new Formula(xml_to_term(lhsinst_xml)),
|
wneuper@4789
|
708 |
new Formula(xml_to_term(rhs_xml)), new Formula(xml_to_term(rhsinst_xml)),
|
wneuper@4789
|
709 |
new Formula(xml_to_term(result_xml)), "xml_to_ContextTheory: ASSUMPTIONS wrong type",
|
wneuper@4789
|
710 |
xml_to_Reference(rlskey_xml))
|
wneuper@4789
|
711 |
// | xml_of_contthy (ContThmInst {thyID, thm, bdvs, thminst, applto, applat,
|
wneuper@4789
|
712 |
// reword, asms, lhs, rhs, result, resasms, asmrls}) =
|
wneuper@4789
|
713 |
case
|
wneuper@4848
|
714 |
XML.Elem(("CONTEXTDATA", Nil), List(
|
wneuper@4848
|
715 |
XML.Elem(("GUH", Nil), List(XML.Text(guh))),
|
wneuper@4848
|
716 |
XML.Elem(("SUBSLIST", Nil), List(subst_xml)), // WRONG type
|
wneuper@4848
|
717 |
XML.Elem(("INSTANTIATED", Nil), List(thminst_xml)),
|
wneuper@4848
|
718 |
XML.Elem(("APPLTO", Nil), List(applto_xml)),
|
wneuper@4848
|
719 |
XML.Elem(("APPLAT", Nil), List(applat_xml)),
|
wneuper@4848
|
720 |
XML.Elem(("ORDER", Nil), List(
|
wneuper@4848
|
721 |
XML.Elem(("ID", Nil), List(XML.Text(reword))))),
|
wneuper@4848
|
722 |
XML.Elem(("ASMSEVAL", Nil), asmevs_xml), //Nil is possible
|
wneuper@4848
|
723 |
XML.Elem(("LHS", Nil), List(lhs_xml)),
|
wneuper@4848
|
724 |
XML.Elem(("LHSINST", Nil), List(lhsinst_xml)),
|
wneuper@4848
|
725 |
XML.Elem(("RHS", Nil), List(rhs_xml)),
|
wneuper@4848
|
726 |
XML.Elem(("RHSINST", Nil), List(rhsinst_xml)),
|
wneuper@4848
|
727 |
XML.Elem(("RESULT", Nil), List(result_xml)),
|
wneuper@4848
|
728 |
XML.Elem(("ASSUMPTIONS", Nil), asms_xml), //Nil is possible
|
wneuper@4848
|
729 |
XML.Elem(("EVALRLS", Nil), List(rlskey_xml))))
|
wneuper@4832
|
730 |
=> new ContextTheory(new KEStoreKey(guh),
|
wneuper@4789
|
731 |
new Formula(xml_to_term(subst_xml)), new Formula(xml_to_term(thminst_xml)),
|
wneuper@4789
|
732 |
new Formula(xml_to_term(applto_xml)), new Formula(xml_to_term(applat_xml)),
|
wneuper@4789
|
733 |
reword,
|
wneuper@4789
|
734 |
sListToVectorFormulaPair(asmevs_xml map xml_to_asm_val),
|
wneuper@4789
|
735 |
new Formula(xml_to_term(lhs_xml)), new Formula(xml_to_term(lhsinst_xml)),
|
wneuper@4789
|
736 |
new Formula(xml_to_term(rhs_xml)), new Formula(xml_to_term(rhsinst_xml)),
|
wneuper@4789
|
737 |
new Formula(xml_to_term(result_xml)), "xml_to_ContextTheory: ASSUMPTIONS wrong type",
|
wneuper@4789
|
738 |
xml_to_Reference(rlskey_xml))
|
wneuper@4789
|
739 |
// | xml_of_contthy (ContRls {thyID = _, rls, applto, result, asms}) =
|
wneuper@4789
|
740 |
case
|
wneuper@4848
|
741 |
XML.Elem(("CONTEXTDATA", Nil), List(
|
wneuper@4848
|
742 |
XML.Elem(("GUH", Nil), List(XML.Text(guh))),
|
wneuper@4848
|
743 |
XML.Elem(("APPLTO", Nil), List(applto_xml)),
|
wneuper@4848
|
744 |
XML.Elem(("RESULT", Nil), List(result_xml)),
|
wneuper@4848
|
745 |
XML.Elem(("ASSUMPTIONS", Nil), asms_xml))) //Nil is possible
|
wneuper@4832
|
746 |
=> new ContextTheory(new KEStoreKey(guh), null, null,
|
wneuper@4789
|
747 |
new Formula(xml_to_term(applto_xml)), null,
|
wneuper@4789
|
748 |
null,
|
wneuper@4789
|
749 |
null,
|
wneuper@4789
|
750 |
null, null,
|
wneuper@4789
|
751 |
null, null,
|
wneuper@4789
|
752 |
new Formula(xml_to_term(result_xml)), "xml_to_ContextTheory: ASSUMPTIONS wrong type",
|
wneuper@4789
|
753 |
null)
|
wneuper@4789
|
754 |
// | xml_of_contthy (ContRlsInst {thyID = _, rls, bdvs, applto, result, asms}) =
|
wneuper@4789
|
755 |
case
|
wneuper@4848
|
756 |
XML.Elem(("CONTEXTDATA", Nil), List(
|
wneuper@4848
|
757 |
XML.Elem(("GUH", Nil), List(XML.Text(guh))),
|
wneuper@4848
|
758 |
XML.Elem(("SUBSLIST", Nil), List(subst_xml)), // WRONG type
|
wneuper@4848
|
759 |
XML.Elem(("INSTANTIATED", Nil), List(thminst_xml)),
|
wneuper@4848
|
760 |
XML.Elem(("APPLTO", Nil), List(applto_xml)),
|
wneuper@4848
|
761 |
XML.Elem(("RESULT", Nil), List(result_xml)),
|
wneuper@4848
|
762 |
XML.Elem(("ASSUMPTIONS", Nil), List(asms_xml))))
|
wneuper@4832
|
763 |
=> new ContextTheory(new KEStoreKey(guh),
|
wneuper@4789
|
764 |
new Formula(xml_to_term(subst_xml)), new Formula(xml_to_term(thminst_xml)),
|
wneuper@4789
|
765 |
new Formula(xml_to_term(applto_xml)), null,
|
wneuper@4789
|
766 |
null,
|
wneuper@4789
|
767 |
null,
|
wneuper@4789
|
768 |
null, null,
|
wneuper@4789
|
769 |
null, null,
|
wneuper@4789
|
770 |
new Formula(xml_to_term(result_xml)), "xml_to_ContextTheory: ASSUMPTIONS wrong type",
|
wneuper@4789
|
771 |
null)
|
wneuper@4789
|
772 |
// | xml_of_contthy (ContNOrew {thyID = _, thm_rls, applto}) =
|
wneuper@4789
|
773 |
case
|
wneuper@4848
|
774 |
XML.Elem(("CONTEXTDATA", Nil), List(
|
wneuper@4848
|
775 |
XML.Elem(("GUH", Nil), List(XML.Text(guh))),
|
wneuper@4848
|
776 |
XML.Elem(("APPLTO", Nil), List(applto_xml))))
|
wneuper@4832
|
777 |
=> new ContextTheory(new KEStoreKey(guh), null, null,
|
wneuper@4789
|
778 |
new Formula(xml_to_term(applto_xml)), null,
|
wneuper@4789
|
779 |
null,
|
wneuper@4789
|
780 |
null,
|
wneuper@4789
|
781 |
null, null,
|
wneuper@4789
|
782 |
null, null,
|
wneuper@4789
|
783 |
null, null,
|
wneuper@4789
|
784 |
null)
|
wneuper@4789
|
785 |
// | xml_of_contthy (ContNOrewInst{thyID = _, thm_rls, bdvs, thminst, applto}) =
|
wneuper@4789
|
786 |
case
|
wneuper@4848
|
787 |
XML.Elem(("CONTEXTDATA", Nil), List(
|
wneuper@4848
|
788 |
XML.Elem(("GUH", Nil), List(XML.Text(guh))),
|
wneuper@4848
|
789 |
XML.Elem(("SUBSLIST", Nil), List(subst_xml)), // WRONG type
|
wneuper@4848
|
790 |
XML.Elem(("INSTANTIATED", Nil), List(thminst_xml)),
|
wneuper@4848
|
791 |
XML.Elem(("APPLTO", Nil), List(applto_xml))))
|
wneuper@4832
|
792 |
=> new ContextTheory(new KEStoreKey(guh),
|
wneuper@4789
|
793 |
new Formula(xml_to_term(subst_xml)), new Formula(xml_to_term(thminst_xml)),
|
wneuper@4789
|
794 |
new Formula(xml_to_term(applto_xml)), null,
|
wneuper@4789
|
795 |
null,
|
wneuper@4789
|
796 |
null,
|
wneuper@4789
|
797 |
null, null,
|
wneuper@4789
|
798 |
null, null,
|
wneuper@4789
|
799 |
null, null,
|
wneuper@4789
|
800 |
null)
|
wneuper@4789
|
801 |
case _ => throw new IllegalArgumentException("xml_to_ContextTheory wrong arg: " + t)
|
wneuper@4789
|
802 |
}
|
wneuper@4789
|
803 |
|
wneuper@4825
|
804 |
def xml_to_ContextProblem(t: XML.Tree): ContextProblem = t match {
|
wneuper@4825
|
805 |
case
|
wneuper@4848
|
806 |
XML.Elem(("CONTEXTDATA", Nil), List(
|
wneuper@4848
|
807 |
XML.Elem(("GUH", Nil), List(XML.Text(guh))),
|
wneuper@4848
|
808 |
XML.Elem(("STATUS", Nil), List(XML.Text(status))),
|
wneuper@4848
|
809 |
XML.Elem(("HEAD", Nil), List(head_xml)),
|
wneuper@4825
|
810 |
model_xml))
|
wneuper@4832
|
811 |
=> new ContextProblem(new KEStoreKey(guh),
|
wneuper@4928
|
812 |
status, xml_to_Formula_NEW(head_xml), xml_to_Model(model_xml))
|
wneuper@4825
|
813 |
case _ => throw new IllegalArgumentException("xml_to_ContextProblem wrong arg: " + t)
|
wneuper@4825
|
814 |
}
|
wneuper@4825
|
815 |
|
wneuper@4825
|
816 |
def xml_to_ContextMethod(t: XML.Tree): ContextMethod = t match {
|
wneuper@4825
|
817 |
case
|
wneuper@4848
|
818 |
XML.Elem(("CONTEXTDATA", Nil), List(
|
wneuper@4848
|
819 |
XML.Elem(("GUH", Nil), List(XML.Text(guh))),
|
wneuper@4848
|
820 |
XML.Elem(("STATUS", Nil), List(XML.Text(status))),
|
wneuper@4848
|
821 |
XML.Elem(("PROGRAM", Nil), List(prog_xml)),
|
wneuper@4825
|
822 |
model_xml))
|
wneuper@4832
|
823 |
=> new ContextMethod(new KEStoreKey(guh),
|
wneuper@4842
|
824 |
status, new Formula(xml_to_prog(prog_xml)), xml_to_Model(model_xml))
|
wneuper@4825
|
825 |
case _ => throw new IllegalArgumentException("xml_to_ContextMethod wrong arg: " + t)
|
wneuper@4825
|
826 |
}
|
wneuper@4825
|
827 |
|
wneuper@4788
|
828 |
def xml_to_CEvent(t: XML.Tree): CEvent = t match {
|
wneuper@4788
|
829 |
case
|
wneuper@4848
|
830 |
XML.Elem(("CALCCHANGED", Nil), List(
|
wneuper@4848
|
831 |
XML.Elem(("UNCHANGED", Nil), List(
|
wneuper@4848
|
832 |
unc_is, XML.Elem(("POS", Nil), List(XML.Text(unc_kind))))),
|
wneuper@4848
|
833 |
XML.Elem(("DELETED", Nil), List(
|
wneuper@4848
|
834 |
del_is, XML.Elem(("POS", Nil), List(XML.Text(del_kind))))),
|
wneuper@4848
|
835 |
XML.Elem(("GENERATED", Nil), List(
|
wneuper@4848
|
836 |
gen_is, XML.Elem(("POS", Nil), List(XML.Text(gen_kind)))))))
|
wneuper@4788
|
837 |
=> new CChanged(
|
wneuper@4788
|
838 |
new Position(DataTypes.xml_to_VectorInteger(unc_is), unc_kind),
|
wneuper@4788
|
839 |
new Position(DataTypes.xml_to_VectorInteger(del_is), del_kind),
|
wneuper@4788
|
840 |
new Position(DataTypes.xml_to_VectorInteger(gen_is), gen_kind))
|
wneuper@4788
|
841 |
case
|
wneuper@4848
|
842 |
XML.Elem(("CALCMESSAGE", Nil), List(XML.Text(msg)))
|
wneuper@4788
|
843 |
=> new CMessage(msg)
|
wneuper@4788
|
844 |
case _ => throw new IllegalArgumentException("xml_to_CChanged wrong arg: " + t)
|
wneuper@4788
|
845 |
}
|
wneuper@4825
|
846 |
|
walther@5239
|
847 |
}
|