112 "val_nam" ("\"val\"") |
112 "val_nam" ("\"val\"") |
113 "next_nam" ("\"next\"") |
113 "next_nam" ("\"next\"") |
114 |
114 |
115 subsection {* Single step execution *} |
115 subsection {* Single step execution *} |
116 |
116 |
117 generate_code |
117 code_module JVM |
|
118 contains |
118 test = "exec (E, start_state E test_name makelist_name)" |
119 test = "exec (E, start_state E test_name makelist_name)" |
119 |
120 |
120 ML {* test *} |
121 ML {* JVM.test *} |
121 ML {* exec (E, the it) *} |
122 ML {* JVM.exec (JVM.E, JVM.the it) *} |
122 ML {* exec (E, the it) *} |
123 ML {* JVM.exec (JVM.E, JVM.the it) *} |
123 ML {* exec (E, the it) *} |
124 ML {* JVM.exec (JVM.E, JVM.the it) *} |
124 ML {* exec (E, the it) *} |
125 ML {* JVM.exec (JVM.E, JVM.the it) *} |
125 ML {* exec (E, the it) *} |
126 ML {* JVM.exec (JVM.E, JVM.the it) *} |
126 ML {* exec (E, the it) *} |
127 ML {* JVM.exec (JVM.E, JVM.the it) *} |
127 ML {* exec (E, the it) *} |
128 ML {* JVM.exec (JVM.E, JVM.the it) *} |
128 ML {* exec (E, the it) *} |
129 ML {* JVM.exec (JVM.E, JVM.the it) *} |
129 ML {* exec (E, the it) *} |
130 ML {* JVM.exec (JVM.E, JVM.the it) *} |
130 ML {* exec (E, the it) *} |
131 ML {* JVM.exec (JVM.E, JVM.the it) *} |
131 ML {* exec (E, the it) *} |
132 ML {* JVM.exec (JVM.E, JVM.the it) *} |
132 ML {* exec (E, the it) *} |
133 ML {* JVM.exec (JVM.E, JVM.the it) *} |
133 ML {* exec (E, the it) *} |
134 ML {* JVM.exec (JVM.E, JVM.the it) *} |
134 ML {* exec (E, the it) *} |
135 ML {* JVM.exec (JVM.E, JVM.the it) *} |
135 ML {* exec (E, the it) *} |
136 ML {* JVM.exec (JVM.E, JVM.the it) *} |
136 ML {* exec (E, the it) *} |
137 ML {* JVM.exec (JVM.E, JVM.the it) *} |
137 ML {* exec (E, the it) *} |
138 ML {* JVM.exec (JVM.E, JVM.the it) *} |
138 ML {* exec (E, the it) *} |
139 ML {* JVM.exec (JVM.E, JVM.the it) *} |
139 ML {* exec (E, the it) *} |
140 ML {* JVM.exec (JVM.E, JVM.the it) *} |
140 ML {* exec (E, the it) *} |
141 ML {* JVM.exec (JVM.E, JVM.the it) *} |
141 ML {* exec (E, the it) *} |
142 ML {* JVM.exec (JVM.E, JVM.the it) *} |
142 ML {* exec (E, the it) *} |
143 ML {* JVM.exec (JVM.E, JVM.the it) *} |
143 ML {* exec (E, the it) *} |
144 ML {* JVM.exec (JVM.E, JVM.the it) *} |
144 ML {* exec (E, the it) *} |
145 ML {* JVM.exec (JVM.E, JVM.the it) *} |
145 ML {* exec (E, the it) *} |
146 ML {* JVM.exec (JVM.E, JVM.the it) *} |
146 ML {* exec (E, the it) *} |
147 ML {* JVM.exec (JVM.E, JVM.the it) *} |
147 ML {* exec (E, the it) *} |
148 ML {* JVM.exec (JVM.E, JVM.the it) *} |
148 ML {* exec (E, the it) *} |
149 ML {* JVM.exec (JVM.E, JVM.the it) *} |
149 ML {* exec (E, the it) *} |
150 ML {* JVM.exec (JVM.E, JVM.the it) *} |
150 ML {* exec (E, the it) *} |
151 ML {* JVM.exec (JVM.E, JVM.the it) *} |
151 ML {* exec (E, the it) *} |
152 ML {* JVM.exec (JVM.E, JVM.the it) *} |
152 ML {* exec (E, the it) *} |
153 ML {* JVM.exec (JVM.E, JVM.the it) *} |
153 ML {* exec (E, the it) *} |
154 ML {* JVM.exec (JVM.E, JVM.the it) *} |
154 ML {* exec (E, the it) *} |
155 ML {* JVM.exec (JVM.E, JVM.the it) *} |
155 ML {* exec (E, the it) *} |
156 ML {* JVM.exec (JVM.E, JVM.the it) *} |
156 ML {* exec (E, the it) *} |
157 ML {* JVM.exec (JVM.E, JVM.the it) *} |
157 ML {* exec (E, the it) *} |
158 ML {* JVM.exec (JVM.E, JVM.the it) *} |
158 ML {* exec (E, the it) *} |
159 ML {* JVM.exec (JVM.E, JVM.the it) *} |
159 ML {* exec (E, the it) *} |
160 ML {* JVM.exec (JVM.E, JVM.the it) *} |
160 ML {* exec (E, the it) *} |
161 ML {* JVM.exec (JVM.E, JVM.the it) *} |
161 ML {* exec (E, the it) *} |
162 ML {* JVM.exec (JVM.E, JVM.the it) *} |
162 ML {* exec (E, the it) *} |
163 ML {* JVM.exec (JVM.E, JVM.the it) *} |
163 ML {* exec (E, the it) *} |
164 ML {* JVM.exec (JVM.E, JVM.the it) *} |
164 ML {* exec (E, the it) *} |
165 ML {* JVM.exec (JVM.E, JVM.the it) *} |
165 ML {* exec (E, the it) *} |
166 ML {* JVM.exec (JVM.E, JVM.the it) *} |
166 ML {* exec (E, the it) *} |
167 ML {* JVM.exec (JVM.E, JVM.the it) *} |
167 ML {* exec (E, the it) *} |
168 ML {* JVM.exec (JVM.E, JVM.the it) *} |
168 ML {* exec (E, the it) *} |
169 ML {* JVM.exec (JVM.E, JVM.the it) *} |
169 ML {* exec (E, the it) *} |
170 ML {* JVM.exec (JVM.E, JVM.the it) *} |
170 ML {* exec (E, the it) *} |
171 ML {* JVM.exec (JVM.E, JVM.the it) *} |
171 ML {* exec (E, the it) *} |
172 ML {* JVM.exec (JVM.E, JVM.the it) *} |
172 ML {* exec (E, the it) *} |
173 ML {* JVM.exec (JVM.E, JVM.the it) *} |
173 ML {* exec (E, the it) *} |
174 ML {* JVM.exec (JVM.E, JVM.the it) *} |
174 |
175 |
175 end |
176 end |