# HG changeset patch
# User wenzelm
# Date 1300030734 -3600
# Node ID 30732d2390c8e11466c9fe058dbb8b1c20bfcb27
# Parent  0b8a13b145e98044017fd5f08aa7828ab8bfbb09
more basic use of Path.position/File.read;

diff -r 0b8a13b145e9 -r 30732d2390c8 src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Sun Mar 13 16:38:14 2011 +0100
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Sun Mar 13 16:38:54 2011 +0100
@@ -13,8 +13,6 @@
 structure SPARK_Commands: SPARK_COMMANDS =
 struct
 
-fun read f path = f (Position.file (Path.implode path)) (File.read path);
-
 fun spark_open vc_name thy =
   let
     val (vc_path, _) = Thy_Load.check_file
@@ -28,9 +26,9 @@
     val rls_path = Path.ext "rls" base;
   in
     SPARK_VCs.set_vcs
-      (snd (read Fdl_Parser.parse_declarations fdl_path))
-      (read Fdl_Parser.parse_rules rls_path)
-      (snd (snd (read (Fdl_Parser.parse_vcs header) vc_path)))
+      (snd (Fdl_Parser.parse_declarations (Path.position fdl_path) (File.read fdl_path)))
+      (Fdl_Parser.parse_rules (Path.position rls_path) (File.read rls_path))
+      (snd (snd (Fdl_Parser.parse_vcs header (Path.position vc_path) (File.read vc_path))))
       base thy
   end;