# HG changeset patch
# User boehmes
# Date 1289573768 -3600
# Node ID db5f14910dceeec901b53c9e57aedaddc631f850
# Parent  1204d268464ffb529c15947b9a58f9cfd64f3624
let the theory formally depend on the Boogie output

diff -r 1204d268464f -r db5f14910dce src/HOL/Boogie/Examples/Boogie_Dijkstra.thy
--- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Fri Nov 12 15:56:07 2010 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Fri Nov 12 15:56:08 2010 +0100
@@ -79,7 +79,7 @@
 *}
 
 
-boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Dijkstra"
+boogie_open "Boogie_Dijkstra"
 
 declare [[smt_certificates="Boogie_Dijkstra.certs"]]
 declare [[smt_fixed=true]]
diff -r 1204d268464f -r db5f14910dce src/HOL/Boogie/Examples/Boogie_Max.thy
--- a/src/HOL/Boogie/Examples/Boogie_Max.thy	Fri Nov 12 15:56:07 2010 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Max.thy	Fri Nov 12 15:56:08 2010 +0100
@@ -36,7 +36,7 @@
 \end{verbatim}
 *}
 
-boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Max"
+boogie_open "Boogie_Max"
 
 declare [[smt_certificates="Boogie_Max.certs"]]
 declare [[smt_fixed=true]]
diff -r 1204d268464f -r db5f14910dce src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy
--- a/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy	Fri Nov 12 15:56:07 2010 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy	Fri Nov 12 15:56:08 2010 +0100
@@ -36,7 +36,7 @@
 \end{verbatim}
 *}
 
-boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Max"
+boogie_open "Boogie_Max"
 
 boogie_status -- {* gives an overview of all verification conditions *}
 
diff -r 1204d268464f -r db5f14910dce src/HOL/Boogie/Examples/VCC_Max.thy
--- a/src/HOL/Boogie/Examples/VCC_Max.thy	Fri Nov 12 15:56:07 2010 +0100
+++ b/src/HOL/Boogie/Examples/VCC_Max.thy	Fri Nov 12 15:56:08 2010 +0100
@@ -44,7 +44,7 @@
 \end{verbatim}
 *}
 
-boogie_open (quiet) "~~/src/HOL/Boogie/Examples/VCC_Max"
+boogie_open (quiet) "VCC_Max"
 
 declare [[smt_certificates="VCC_Max.certs"]]
 declare [[smt_fixed=true]]
diff -r 1204d268464f -r db5f14910dce src/HOL/Boogie/Tools/boogie_commands.ML
--- a/src/HOL/Boogie/Tools/boogie_commands.ML	Fri Nov 12 15:56:07 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Fri Nov 12 15:56:08 2010 +0100
@@ -16,13 +16,20 @@
 
 fun boogie_open ((quiet, base_name), offsets) thy =
   let
-    val path = Path.explode (base_name ^ ".b2i")
-    val _ = File.exists path orelse
-      error ("Unable to find file " ^ quote (Path.implode path))
+    val ext = "b2i"
+    fun add_ext path = path |> snd (Path.split_ext path) <> ext ? Path.ext ext
+    val base_path = add_ext (Path.explode base_name)
+    val path_id = Thy_Load.check_file [Thy_Load.master_directory thy] base_path
+
     val _ = Boogie_VCs.is_closed thy orelse
       error ("Found the beginning of a new Boogie environment, " ^
         "but another Boogie environment is still open.")
-  in Boogie_Loader.load_b2i (not quiet) offsets path thy end
+  in
+    thy
+    |> Thy_Load.require base_path
+    |> Boogie_Loader.load_b2i (not quiet) offsets (fst path_id)
+    |> Thy_Load.provide (base_path, path_id)
+  end
 
 
 datatype vc_opts =