equal
deleted
inserted
replaced
14 |
14 |
15 (* commands *) |
15 (* commands *) |
16 |
16 |
17 fun boogie_open ((quiet, base_name), offsets) thy = |
17 fun boogie_open ((quiet, base_name), offsets) thy = |
18 let |
18 let |
19 val path = Path.explode (base_name ^ ".b2i") |
19 val ext = "b2i" |
20 val _ = File.exists path orelse |
20 fun add_ext path = path |> snd (Path.split_ext path) <> ext ? Path.ext ext |
21 error ("Unable to find file " ^ quote (Path.implode path)) |
21 val base_path = add_ext (Path.explode base_name) |
|
22 val path_id = Thy_Load.check_file [Thy_Load.master_directory thy] base_path |
|
23 |
22 val _ = Boogie_VCs.is_closed thy orelse |
24 val _ = Boogie_VCs.is_closed thy orelse |
23 error ("Found the beginning of a new Boogie environment, " ^ |
25 error ("Found the beginning of a new Boogie environment, " ^ |
24 "but another Boogie environment is still open.") |
26 "but another Boogie environment is still open.") |
25 in Boogie_Loader.load_b2i (not quiet) offsets path thy end |
27 in |
|
28 thy |
|
29 |> Thy_Load.require base_path |
|
30 |> Boogie_Loader.load_b2i (not quiet) offsets (fst path_id) |
|
31 |> Thy_Load.provide (base_path, path_id) |
|
32 end |
26 |
33 |
27 |
34 |
28 datatype vc_opts = |
35 datatype vc_opts = |
29 VC_Complete | |
36 VC_Complete | |
30 VC_Take of int list * (bool * string list) option | |
37 VC_Take of int list * (bool * string list) option | |