# HG changeset patch
# User wenzelm
# Date 1345727175 -7200
# Node ID 5c4275c3b5b8162dd18f08db84502f4006e35e51
# Parent  5b192d6b7a54226641566aedce9d8db0d4b6791d
turned 'boogie_open' into thy_load command, without any declarations of 'uses';

diff -r 5b192d6b7a54 -r 5c4275c3b5b8 src/HOL/Boogie/Boogie.thy
--- a/src/HOL/Boogie/Boogie.thy	Thu Aug 23 14:58:42 2012 +0200
+++ b/src/HOL/Boogie/Boogie.thy	Thu Aug 23 15:06:15 2012 +0200
@@ -7,7 +7,10 @@
 theory Boogie
 imports Word
 keywords
-  "boogie_open" "boogie_end" :: thy_decl and "boogie_vc" :: thy_goal and "boogie_status" :: diag
+  "boogie_open" :: thy_load and
+  "boogie_end" :: thy_decl and
+  "boogie_vc" :: thy_goal and
+  "boogie_status" :: diag
 begin
 
 text {*
@@ -64,7 +67,7 @@
 Proving Boogie-generated verification conditions happens inside
 a Boogie environment:
 
-  boogie_open "b2i file without extension"
+  boogie_open "b2i file with extension"
   boogie_vc "verification condition 1" ...
   boogie_vc "verification condition 2" ...
   boogie_vc "verification condition 3" ...
diff -r 5b192d6b7a54 -r 5c4275c3b5b8 src/HOL/Boogie/Examples/Boogie_Dijkstra.thy
--- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Thu Aug 23 14:58:42 2012 +0200
+++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Thu Aug 23 15:06:15 2012 +0200
@@ -6,7 +6,6 @@
 
 theory Boogie_Dijkstra
 imports Boogie
-uses ("Boogie_Dijkstra.b2i")
 begin
 
 text {*
diff -r 5b192d6b7a54 -r 5c4275c3b5b8 src/HOL/Boogie/Examples/Boogie_Max.thy
--- a/src/HOL/Boogie/Examples/Boogie_Max.thy	Thu Aug 23 14:58:42 2012 +0200
+++ b/src/HOL/Boogie/Examples/Boogie_Max.thy	Thu Aug 23 15:06:15 2012 +0200
@@ -6,7 +6,6 @@
 
 theory Boogie_Max
 imports Boogie
-uses ("Boogie_Max.b2i")
 begin
 
 text {*
diff -r 5b192d6b7a54 -r 5c4275c3b5b8 src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy
--- a/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy	Thu Aug 23 14:58:42 2012 +0200
+++ b/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy	Thu Aug 23 15:06:15 2012 +0200
@@ -6,7 +6,6 @@
 
 theory Boogie_Max_Stepwise
 imports Boogie
-uses ("Boogie_Max.b2i")
 begin
 
 text {*
diff -r 5b192d6b7a54 -r 5c4275c3b5b8 src/HOL/Boogie/Examples/VCC_Max.thy
--- a/src/HOL/Boogie/Examples/VCC_Max.thy	Thu Aug 23 14:58:42 2012 +0200
+++ b/src/HOL/Boogie/Examples/VCC_Max.thy	Thu Aug 23 15:06:15 2012 +0200
@@ -6,7 +6,6 @@
 
 theory VCC_Max
 imports Boogie
-uses ("VCC_Max.b2i")
 begin
 
 text {*
diff -r 5b192d6b7a54 -r 5c4275c3b5b8 src/HOL/Boogie/Tools/boogie_commands.ML
--- a/src/HOL/Boogie/Tools/boogie_commands.ML	Thu Aug 23 14:58:42 2012 +0200
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Thu Aug 23 15:06:15 2012 +0200
@@ -14,17 +14,16 @@
 
 (* commands *)
 
-fun boogie_open ((quiet, base_name), offsets) thy =
+fun boogie_open ((quiet, files), offsets) thy =
   let
+    val ([{src_path = path, text, ...}], thy') = files thy
+
     val ext = "b2i"
-    fun check_ext path = snd (Path.split_ext path) = ext orelse
+    val _ = snd (Path.split_ext path) = ext orelse
       error ("Bad file ending of file " ^ Path.print path ^ ", " ^
         "expected file ending " ^ quote ext)
 
-    val base_path = Path.explode base_name |> tap check_ext
-    val (text, thy') = Thy_Load.use_file base_path thy
-
-    val _ = Boogie_VCs.is_closed thy' orelse
+    val _ = Boogie_VCs.is_closed thy orelse
       error ("Found the beginning of a new Boogie environment, " ^
         "but another Boogie environment is still open.")
   in
@@ -44,7 +43,7 @@
 fun get_vc thy vc_name =
   (case Boogie_VCs.lookup thy vc_name of
     SOME vc => vc
-  | NONE => 
+  | NONE =>
       (case AList.lookup (op =) (Boogie_VCs.state_of thy) vc_name of
         SOME Boogie_VCs.Proved => error ("The verification condition " ^
           quote vc_name ^ " has already been proved.")
@@ -258,7 +257,7 @@
     val unproved = map_filter not_proved (Boogie_VCs.state_of thy)
   in
     if null unproved then Boogie_VCs.close thy
-    else error (Pretty.string_of (Pretty.big_list 
+    else error (Pretty.string_of (Pretty.big_list
       "The following verification conditions have not been proved:"
       (map Pretty.str unproved)))
   end
@@ -277,7 +276,7 @@
 val _ =
   Outer_Syntax.command @{command_spec "boogie_open"}
     "open a new Boogie environment and load a Boogie-generated .b2i file"
-    (scan_opt "quiet" -- Parse.name -- vc_offsets >> 
+    (scan_opt "quiet" -- Thy_Load.provide_parse_files "boogie_open" -- vc_offsets >>
       (Toplevel.theory o boogie_open))
 
 
@@ -350,7 +349,7 @@
 val setup = Theory.at_end (fn thy =>
   let
     val _ = Boogie_VCs.is_closed thy
-      orelse error ("Found the end of the theory, " ^ 
+      orelse error ("Found the end of the theory, " ^
         "but the last Boogie environment is still open.")
   in NONE end)