1 //
2 // THIS FILE IS AUTOMATICALLY GENERATED!!
3 //
4 // Generated at 2009-08-09 by the VDM++ to JAVA Code Generator
5 // (v8.2.1b - Wed 15-Jul-2009 14:09:22)
6 //
7 // Supported compilers: jdk 1.4/1.5/1.6
8 //
9
10 // ***** VDMTOOLS START Name=HeaderComment KEEP=NO
11 // ***** VDMTOOLS END Name=HeaderComment
12
13 // ***** VDMTOOLS START Name=package KEEP=NO
14 package org.overturetool.api.xml;
15
16 // ***** VDMTOOLS END Name=package
17
18 // ***** VDMTOOLS START Name=imports KEEP=NO
19
20 import jp.co.csk.vdm.toolbox.VDM.*;
21 import java.util.*;
22 // ***** VDMTOOLS END Name=imports
23
24
25
26 public class XmlData {
27
28 // ***** VDMTOOLS START Name=vdmComp KEEP=NO
29 static UTIL.VDMCompare vdmComp = new UTIL.VDMCompare();
30 // ***** VDMTOOLS END Name=vdmComp
31
32 // ***** VDMTOOLS START Name=data KEEP=NO
33 public String data = null;
34 // ***** VDMTOOLS END Name=data
35
36
37 // ***** VDMTOOLS START Name=vdm_init_XmlData KEEP=NO
38 private void vdm_init_XmlData () throws CGException {
39 try {
40 data = new String("");
41 }
42 catch (Exception e){
43
44 e.printStackTrace(System.out);
45 System.out.println(e.getMessage());
46 }
47 }
48 // ***** VDMTOOLS END Name=vdm_init_XmlData
49
50
51 // ***** VDMTOOLS START Name=XmlData KEEP=NO
52 public XmlData () throws CGException {
53 vdm_init_XmlData();
54 }
55 // ***** VDMTOOLS END Name=XmlData
56
57
58 // ***** VDMTOOLS START Name=XmlData#1|String KEEP=NO
59 public XmlData (final String pdata) throws CGException {
60
61 vdm_init_XmlData();
62 data = UTIL.ConvertToString(UTIL.clone(pdata));
63 }
64 // ***** VDMTOOLS END Name=XmlData#1|String
65
66
67 // ***** VDMTOOLS START Name=accept#1|XmlVisitor KEEP=NO
68 public void accept (final XmlVisitor pxv) throws CGException {
69 pxv.VisitXmlData((XmlData) this);
70 }
71 // ***** VDMTOOLS END Name=accept#1|XmlVisitor
72
73 }
74 ;