proper thy_load command 'boogie_file' -- avoid direct access to file-system;

--- a/etc/isar-keywords.el	Sat Nov 16 13:12:02 2013 +0100
+++ b/etc/isar-keywords.el	Sat Nov 16 16:57:09 2013 +0100
@@ -1,6 +1,6 @@
 ;;
 ;; Keyword classification tables for Isabelle/Isar.
-;; Generated from HOL + HOL-Auth + HOL-BNF + HOL-BNF-LFP + HOL-Bali + HOL-Decision_Procs + HOL-IMP + HOL-Imperative_HOL + HOL-Import + HOL-Library + HOL-Mutabelle + HOL-Nominal + HOL-Proofs + HOL-Proofs-Extraction + HOL-SPARK + HOL-Statespace + HOL-TPTP + HOL-ex + HOLCF + Pure.
+;; Generated from HOL + HOL-Auth + HOL-BNF + HOL-BNF-LFP + HOL-Bali + HOL-Decision_Procs + HOL-IMP + HOL-Imperative_HOL + HOL-Import + HOL-Library + HOL-Mutabelle + HOL-Nominal + HOL-Proofs + HOL-Proofs-Extraction + HOL-SPARK + HOL-Statespace + HOL-TPTP + HOL-Word-SMT_Examples + HOL-ex + HOLCF + Pure.
 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
 
@@ -33,6 +33,7 @@
     "axiomatization"
     "back"
     "bnf"
+    "boogie_file"
     "bundle"
     "by"
     "cannot_undo"
@@ -487,6 +488,7 @@
     "atom_decl"
     "attribute_setup"
     "axiomatization"
+    "boogie_file"
     "bundle"
     "case_of_simps"
     "class"

--- a/src/HOL/ROOT	Sat Nov 16 13:12:02 2013 +0100
+++ b/src/HOL/ROOT	Sat Nov 16 16:57:09 2013 +0100
@@ -779,13 +779,10 @@
   theories [condition = ISABELLE_FULL_TEST]
     SMT_Tests
   files
-    "Boogie_Dijkstra.b2i"
     "Boogie_Dijkstra.certs"
-    "Boogie_Max.b2i"
     "Boogie_Max.certs"
     "SMT_Examples.certs"
     "SMT_Word_Examples.certs"
-    "VCC_Max.b2i"
     "VCC_Max.certs"
 
 session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +

--- a/src/HOL/SMT_Examples/Boogie.thy	Sat Nov 16 13:12:02 2013 +0100
+++ b/src/HOL/SMT_Examples/Boogie.thy	Sat Nov 16 16:57:09 2013 +0100
@@ -6,6 +6,7 @@
 
 theory Boogie
 imports Main
+keywords "boogie_file" :: thy_load ("b2i")
 begin
 
 text {*
@@ -56,17 +57,17 @@
 
 declare [[smt_certificates = "Boogie_Max.certs"]]
 
-setup {* Boogie.boogie_prove "Boogie_Max.b2i" *}
+boogie_file Boogie_Max
 
 
 declare [[smt_certificates = "Boogie_Dijkstra.certs"]]
 
-setup {* Boogie.boogie_prove "Boogie_Dijkstra.b2i" *}
+boogie_file Boogie_Dijkstra
 
 
 declare [[z3_with_extensions = true]]
 declare [[smt_certificates = "VCC_Max.certs"]]
 
-setup {* Boogie.boogie_prove "VCC_Max.b2i" *}
+boogie_file VCC_Max
 
 end

--- a/src/HOL/SMT_Examples/boogie.ML	Sat Nov 16 13:12:02 2013 +0100
+++ b/src/HOL/SMT_Examples/boogie.ML	Sat Nov 16 16:57:09 2013 +0100
@@ -6,7 +6,7 @@
 
 signature BOOGIE =
 sig
-  val boogie_prove: string -> theory -> theory
+  val boogie_prove: theory -> string -> unit
 end
 
 structure Boogie: BOOGIE =
@@ -299,21 +299,33 @@
   ALLGOALS (SMT_Solver.smt_tac ctxt (boogie_rules @ axioms))
 
 
-fun boogie_prove file_name thy =
+fun boogie_prove thy text =
   let
-    val (text, thy') = Thy_Load.use_file (Path.explode file_name) thy
     val lines = explode_lines text
 
     val ((axioms, vc), ctxt) =
       empty_context
       |> parse_lines lines
       |> add_unique_axioms
-      |> build_proof_context thy'
+      |> build_proof_context thy
 
     val _ = Goal.prove ctxt [] axioms vc (fn {prems, context} =>
       boogie_tac context prems)
     val _ = writeln "Verification condition proved successfully"
 
-  in thy' end
+  in () end
+
+
+(* Isar command *)
+
+val _ =
+  Outer_Syntax.command @{command_spec "boogie_file"}
+    "prove verification condition from .b2i file"
+    (Thy_Load.provide_parse_files "boogie_file" >> (fn files =>
+      Toplevel.theory (fn thy =>
+        let
+          val ([{text, ...}], thy') = files thy;
+          val _ = boogie_prove thy' text;
+        in thy' end)))
 
 end