equal
deleted
inserted
replaced
31 -- "method name + parameter types" |
31 -- "method name + parameter types" |
32 -- "program counter within frame" |
32 -- "program counter within frame" |
33 |
33 |
34 |
34 |
35 section {* Exceptions *} |
35 section {* Exceptions *} |
36 constdefs |
36 definition raise_system_xcpt :: "bool \<Rightarrow> xcpt \<Rightarrow> val option" where |
37 raise_system_xcpt :: "bool \<Rightarrow> xcpt \<Rightarrow> val option" |
|
38 "raise_system_xcpt b x \<equiv> raise_if b x None" |
37 "raise_system_xcpt b x \<equiv> raise_if b x None" |
39 |
38 |
40 section {* Runtime State *} |
39 section {* Runtime State *} |
41 types |
40 types |
42 jvm_state = "val option \<times> aheap \<times> frame list" -- "exception flag, heap, frames" |
41 jvm_state = "val option \<times> aheap \<times> frame list" -- "exception flag, heap, frames" |