--- a/src/HOL/Boogie/Tools/boogie_commands.ML Fri Mar 16 14:46:13 2012 +0100
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML Fri Mar 16 18:20:12 2012 +0100
@@ -275,9 +275,8 @@
(Parse.string --| Args.colon -- Parse.nat))) []
val _ =
- Outer_Syntax.command "boogie_open"
+ Outer_Syntax.command @{command_spec "boogie_open"}
"open a new Boogie environment and load a Boogie-generated .b2i file"
- Keyword.thy_decl
(scan_opt "quiet" -- Parse.name -- vc_offsets >>
(Toplevel.theory o boogie_open))
@@ -303,9 +302,8 @@
Scan.succeed VC_Complete
val _ =
- Outer_Syntax.command "boogie_vc"
+ Outer_Syntax.command @{command_spec "boogie_vc"}
"enter into proof mode for a specific verification condition"
- Keyword.thy_goal
(vc_name -- vc_opts >> (fn args =>
(Toplevel.print o Toplevel.theory_to_proof (boogie_vc args))))
@@ -336,18 +334,16 @@
f (Toplevel.theory_of state))
val _ =
- Outer_Syntax.improper_command "boogie_status"
+ Outer_Syntax.improper_command @{command_spec "boogie_status"}
"show the name and state of all loaded verification conditions"
- Keyword.diag
(status_test >> status_cmd ||
status_vc >> status_cmd ||
Scan.succeed (status_cmd boogie_status))
val _ =
- Outer_Syntax.command "boogie_end"
+ Outer_Syntax.command @{command_spec "boogie_end"}
"close the current Boogie environment"
- Keyword.thy_decl
(Scan.succeed (Toplevel.theory boogie_end))