diff -r d07a0b9601aa -r da1a1eae93fa src/HOL/SPARK/Tools/spark_commands.ML --- a/src/HOL/SPARK/Tools/spark_commands.ML Thu Jun 28 09:18:58 2012 +0200 +++ b/src/HOL/SPARK/Tools/spark_commands.ML Fri Jun 29 09:45:48 2012 +0200 @@ -44,7 +44,7 @@ SPARK_VCs.add_type (s, (Syntax.read_typ_global thy raw_typ, cmap)) thy; fun get_vc thy vc_name = - (case SPARK_VCs.lookup_vc thy vc_name of + (case SPARK_VCs.lookup_vc thy false vc_name of SOME (ctxt, (_, proved, ctxt', stmt)) => if is_some proved then error ("The verification condition " ^ @@ -71,7 +71,7 @@ let val thy = Toplevel.theory_of state; - val (context, defs, vcs) = SPARK_VCs.get_vcs thy; + val (context, defs, vcs) = SPARK_VCs.get_vcs thy true; val vcs' = AList.coalesce (op =) (map_filter (fn (name, (trace, status, ctxt, stmt)) => @@ -144,7 +144,9 @@ val _ = Outer_Syntax.command @{command_spec "spark_end"} "close the current SPARK environment" - (Scan.succeed (Toplevel.theory SPARK_VCs.close)); + (Scan.optional (@{keyword "("} |-- Parse.!!! + (Parse.reserved "incomplete" --| @{keyword ")"}) >> K true) false >> + (Toplevel.theory o SPARK_VCs.close)); val setup = Theory.at_end (fn thy => let