# HG changeset patch # User boehmes # Date 1289776836 -3600 # Node ID 293f9f211be0268bf8918f573984030ba18e612f # Parent b6f1da38fa24b94147b095f513b1a0be3c657d5a formal dependency on b2i files diff -r b6f1da38fa24 -r 293f9f211be0 src/HOL/Boogie/Examples/Boogie_Dijkstra.thy --- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy Sun Nov 14 23:55:25 2010 +0100 +++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy Mon Nov 15 00:20:36 2010 +0100 @@ -6,6 +6,7 @@ theory Boogie_Dijkstra imports Boogie +uses ("Boogie_Dijkstra.b2i") begin text {* diff -r b6f1da38fa24 -r 293f9f211be0 src/HOL/Boogie/Examples/Boogie_Max.thy --- a/src/HOL/Boogie/Examples/Boogie_Max.thy Sun Nov 14 23:55:25 2010 +0100 +++ b/src/HOL/Boogie/Examples/Boogie_Max.thy Mon Nov 15 00:20:36 2010 +0100 @@ -6,6 +6,7 @@ theory Boogie_Max imports Boogie +uses ("Boogie_Max.b2i") begin text {* diff -r b6f1da38fa24 -r 293f9f211be0 src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy --- a/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy Sun Nov 14 23:55:25 2010 +0100 +++ b/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy Mon Nov 15 00:20:36 2010 +0100 @@ -6,6 +6,7 @@ theory Boogie_Max_Stepwise imports Boogie +uses ("Boogie_Max.b2i") begin text {* diff -r b6f1da38fa24 -r 293f9f211be0 src/HOL/Boogie/Examples/VCC_Max.thy --- a/src/HOL/Boogie/Examples/VCC_Max.thy Sun Nov 14 23:55:25 2010 +0100 +++ b/src/HOL/Boogie/Examples/VCC_Max.thy Mon Nov 15 00:20:36 2010 +0100 @@ -6,6 +6,7 @@ theory VCC_Max imports Boogie +uses ("VCC_Max.b2i") begin text {* diff -r b6f1da38fa24 -r 293f9f211be0 src/HOL/Boogie/Tools/boogie_commands.ML --- a/src/HOL/Boogie/Tools/boogie_commands.ML Sun Nov 14 23:55:25 2010 +0100 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML Mon Nov 15 00:20:36 2010 +0100 @@ -19,16 +19,16 @@ 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 (full_path, _) = + 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 thy - |> Thy_Load.require base_path - |> Boogie_Loader.load_b2i (not quiet) offsets (fst path_id) - |> Thy_Load.provide (base_path, path_id) + |> Boogie_Loader.load_b2i (not quiet) offsets full_path + |> Thy_Load.provide_file base_path end