# HG changeset patch
# User wenzelm
# Date 1345729408 -7200
# Node ID 713f24d7a40f05b402fafc852cfd0434d91cbd91
# Parent  5c4275c3b5b8162dd18f08db84502f4006e35e51
added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;

diff -r 5c4275c3b5b8 -r 713f24d7a40f etc/isar-keywords.el
--- a/etc/isar-keywords.el	Thu Aug 23 15:06:15 2012 +0200
+++ b/etc/isar-keywords.el	Thu Aug 23 15:43:28 2012 +0200
@@ -238,6 +238,8 @@
     "sorry"
     "spark_end"
     "spark_open"
+    "spark_open_siv"
+    "spark_open_vcg"
     "spark_proof_functions"
     "spark_status"
     "spark_types"
@@ -543,6 +545,8 @@
     "sledgehammer_params"
     "spark_end"
     "spark_open"
+    "spark_open_siv"
+    "spark_open_vcg"
     "spark_proof_functions"
     "spark_types"
     "statespace"
diff -r 5c4275c3b5b8 -r 713f24d7a40f src/HOL/SPARK/SPARK_Setup.thy
--- a/src/HOL/SPARK/SPARK_Setup.thy	Thu Aug 23 15:06:15 2012 +0200
+++ b/src/HOL/SPARK/SPARK_Setup.thy	Thu Aug 23 15:43:28 2012 +0200
@@ -8,6 +8,8 @@
 theory SPARK_Setup
 imports Word
 keywords
+  "spark_open_vcg" :: thy_load ("vcg", "fdl", "rls") and
+  "spark_open_siv" :: thy_load ("siv", "fdl", "rls") and
   "spark_open" "spark_proof_functions" "spark_types" "spark_end" :: thy_decl and
   "spark_vc" :: thy_goal and "spark_status" :: diag
 begin
diff -r 5c4275c3b5b8 -r 713f24d7a40f src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Thu Aug 23 15:06:15 2012 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Thu Aug 23 15:43:28 2012 +0200
@@ -13,8 +13,22 @@
 structure SPARK_Commands: SPARK_COMMANDS =
 struct
 
-(* FIXME proper Thy_Load.use_file, also for fdl_path and rls_path (!?) *)
-fun spark_open (vc_name, prfx) thy =
+fun spark_open header (prfx, files) thy =
+  let
+    val ([{src_path, text = vc_text, pos = vc_pos, ...},
+      {text = fdl_text, pos = fdl_pos, ...},
+      {text = rls_text, pos = rls_pos, ...}], thy') = files thy;
+    val base = fst (Path.split_ext (File.full_path (Thy_Load.master_directory thy') src_path));
+  in
+    SPARK_VCs.set_vcs
+      (snd (Fdl_Parser.parse_declarations fdl_pos fdl_text))
+      (Fdl_Parser.parse_rules rls_pos rls_text)
+      (snd (Fdl_Parser.parse_vcs header vc_pos vc_text))
+      base prfx thy'
+  end;
+
+(* FIXME *)
+fun spark_open_old (vc_name, prfx) thy =
   let
     val ((vc_path, vc_id), vc_text) = Thy_Load.load_file thy (Path.explode vc_name);
     val (base, header) =
@@ -107,7 +121,19 @@
 val _ =
   Outer_Syntax.command @{command_spec "spark_open"}
     "open a new SPARK environment and load a SPARK-generated .vcg or .siv file"
-    (Parse.name -- Parse.parname >> (Toplevel.theory o spark_open));
+    (Parse.name -- Parse.parname >> (Toplevel.theory o spark_open_old));
+
+val _ =
+  Outer_Syntax.command @{command_spec "spark_open_vcg"}
+    "open a new SPARK environment and load a SPARK-generated .vcg file"
+    (Parse.parname -- Thy_Load.provide_parse_files "spark_open_vcg"
+      >> (Toplevel.theory o spark_open Fdl_Lexer.vcg_header));
+
+val _ =
+  Outer_Syntax.command @{command_spec "spark_open_siv"}
+    "open a new SPARK environment and load a SPARK-generated .siv file"
+    (Parse.parname -- Thy_Load.provide_parse_files "spark_open_siv"
+      >> (Toplevel.theory o spark_open Fdl_Lexer.siv_header));
 
 val pfun_type = Scan.option
   (Args.parens (Parse.list1 Parse.name) --| Args.colon -- Parse.name);