# HG changeset patch
# User boehmes
# Date 1289982143 -3600
# Node ID 0592d3a39c085d0c327d5e1cfb0a20cf956f39b8
# Parent  98ebd2300823310fd5b711c92fb482c124e7eecb
require the b2i file ending in the boogie_open command (for consistency with the theory header)

diff -r 98ebd2300823 -r 0592d3a39c08 NEWS
--- a/NEWS	Wed Nov 17 08:14:56 2010 +0100
+++ b/NEWS	Wed Nov 17 09:22:23 2010 +0100
@@ -355,6 +355,9 @@
     cvc3_options
     yices_options
 
+* Boogie output files (.b2i files) need to be declared in the
+theory header.
+
 * Removed [split_format ... and ... and ...] version of
 [split_format].  Potential INCOMPATIBILITY.
 
diff -r 98ebd2300823 -r 0592d3a39c08 src/HOL/Boogie/Examples/Boogie_Dijkstra.thy
--- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Wed Nov 17 08:14:56 2010 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Wed Nov 17 09:22:23 2010 +0100
@@ -80,7 +80,7 @@
 *}
 
 
-boogie_open "Boogie_Dijkstra"
+boogie_open "Boogie_Dijkstra.b2i"
 
 declare [[smt_certificates="Boogie_Dijkstra.certs"]]
 declare [[smt_fixed=true]]
diff -r 98ebd2300823 -r 0592d3a39c08 src/HOL/Boogie/Examples/Boogie_Max.thy
--- a/src/HOL/Boogie/Examples/Boogie_Max.thy	Wed Nov 17 08:14:56 2010 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Max.thy	Wed Nov 17 09:22:23 2010 +0100
@@ -37,7 +37,7 @@
 \end{verbatim}
 *}
 
-boogie_open "Boogie_Max"
+boogie_open "Boogie_Max.b2i"
 
 declare [[smt_certificates="Boogie_Max.certs"]]
 declare [[smt_fixed=true]]
diff -r 98ebd2300823 -r 0592d3a39c08 src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy
--- a/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy	Wed Nov 17 08:14:56 2010 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy	Wed Nov 17 09:22:23 2010 +0100
@@ -37,7 +37,7 @@
 \end{verbatim}
 *}
 
-boogie_open "Boogie_Max"
+boogie_open "Boogie_Max.b2i"
 
 boogie_status -- {* gives an overview of all verification conditions *}
 
diff -r 98ebd2300823 -r 0592d3a39c08 src/HOL/Boogie/Examples/VCC_Max.thy
--- a/src/HOL/Boogie/Examples/VCC_Max.thy	Wed Nov 17 08:14:56 2010 +0100
+++ b/src/HOL/Boogie/Examples/VCC_Max.thy	Wed Nov 17 09:22:23 2010 +0100
@@ -45,7 +45,7 @@
 \end{verbatim}
 *}
 
-boogie_open (quiet) "VCC_Max"
+boogie_open (quiet) "VCC_Max.b2i"
 
 declare [[smt_certificates="VCC_Max.certs"]]
 declare [[smt_fixed=true]]
diff -r 98ebd2300823 -r 0592d3a39c08 src/HOL/Boogie/Tools/boogie_commands.ML
--- a/src/HOL/Boogie/Tools/boogie_commands.ML	Wed Nov 17 08:14:56 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Wed Nov 17 09:22:23 2010 +0100
@@ -17,8 +17,11 @@
 fun boogie_open ((quiet, base_name), offsets) thy =
   let
     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)
+    fun check_ext path = snd (Path.split_ext path) = ext orelse
+      error ("Bad file ending of file " ^ quote (Path.implode path) ^ ", " ^
+        "expected file ending " ^ quote ext)
+
+    val base_path = Path.explode base_name |> tap check_ext
     val (full_path, _) =
       Thy_Load.check_file [Thy_Load.master_directory thy] base_path