equal
deleted
inserted
replaced
18 { |
18 { |
19 /** main entry point **/ |
19 /** main entry point **/ |
20 |
20 |
21 def main(args: Array[String]) |
21 def main(args: Array[String]) |
22 { |
22 { |
23 val system_dialog = new System_Dialog |
23 val system_dialog = new System_Dialog() |
24 |
24 |
25 def exit_error(exn: Throwable): Nothing = |
25 def exit_error(exn: Throwable): Nothing = |
26 { |
26 { |
27 GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn))) |
27 GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn))) |
28 system_dialog.return_code(Exn.return_code(exn, 2)) |
28 system_dialog.return_code(Exn.return_code(exn, 2)) |