protection contre certaines exceptions levees par marshal_{in,out}

possibilite de declarer une def syntaxique comme infix (utilise par FTA)


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1442 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 19 insertions, 24 deletions

diff --git a/lib/system.ml b/lib/system.ml
index d3b222922..db478d9e3 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -110,7 +110,9 @@ let try_remove f =
                      'sTR f ; 'sTR" which is corrupted!" >]
 
 let marshal_out ch v = Marshal.to_channel ch v []
-let marshal_in ch = Marshal.from_channel ch
+let marshal_in ch =
+  try Marshal.from_channel ch
+  with End_of_file -> error "corrupted file: reached end of file"
 
 exception Bad_magic_number of string
 
diff --git a/library/library.ml b/library/library.ml
index ba41615a9..e58f71659 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -210,12 +210,13 @@ let save_module_to process s f =
     md_nametab = process seg;
     md_deps = current_imports () } in
   let (f',ch) = raw_extern_module f in
-  System.marshal_out ch md;
-  flush ch;
-  let di = Digest.file f' in
-  System.marshal_out ch di;
-  close_out ch
-
+  try
+    System.marshal_out ch md;
+    flush ch;
+    let di = Digest.file f' in
+    System.marshal_out ch di;
+    close_out ch
+  with e -> (warning ("Removed file "^f');close_out ch; Sys.remove f'; raise e)
 (*s Iterators. *)
 
 let fold_all_segments insec f x =
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index d95e254c8..c567a2f94 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -224,11 +224,10 @@ let add_infix assoc n inf pr =
     errorlabstrm "Vernacentries.infix_grammar_entry"
       [< 'sTR"Associativity Precedence must be 6,7,8 or 9." >];
   (* check the grammar entry *)
-  let prefast = Termast.ast_of_ref pr in
-  let prefname = (Names.string_of_path (Global.sp_of_global pr))^"_infix" in
-  let gram_rule = gram_infix assoc n (split inf) prefname prefast in
+  let prefname = inf^"_infix" in
+  let gram_rule = gram_infix assoc n (split inf) prefname pr in
   (* check the syntax entry *)
-  let syntax_rule = infix_syntax_entry assoc n inf prefname prefast in
+  let syntax_rule = infix_syntax_entry assoc n inf prefname pr in
   Lib.add_anonymous_leaf (inInfix(gram_rule,syntax_rule))
 
 (* Distfix *)
@@ -272,8 +271,7 @@ let distfix assoc n sl fname astf  =
       ]
   }
 
-let add_distfix a n df f =
-  let fname = (Names.string_of_path (Global.sp_of_global f))^"_distfix" in
-  let astf = Termast.ast_of_ref f in
+let add_distfix a n df astf =
+  let fname = df^"_distfix" in
   Lib.add_anonymous_leaf (inInfix(distfix a n (split df) fname astf, []))
 
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 08fb2800d..b51a9a43d 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -1,12 +1,6 @@
 
 (*i $Id$ i*)
 
-(*i*)
-open Extend
-open Names
-open Term
-(*i*)
-
 (* Adding grammar and pretty-printing objects in the environment *)
 
 val add_syntax_obj : string -> Coqast.t list -> unit
@@ -15,8 +9,8 @@ val add_grammar_obj : string -> Coqast.t list -> unit
 val add_token_obj : string -> unit
 
 val add_infix :
-  Gramext.g_assoc option -> int -> string -> global_reference -> unit
+  Gramext.g_assoc option -> int -> string -> Coqast.t -> unit
 val add_distfix :
-  Gramext.g_assoc option -> int -> string -> global_reference -> unit
+  Gramext.g_assoc option -> int -> string -> Coqast.t -> unit
 
 val print_grammar : string -> string -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 11e65b934..02d2ce6a3 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1469,8 +1469,8 @@ let _ =
   add "INFIX"
     (function
        | [VARG_AST assoc; VARG_NUMBER n; VARG_STRING inf; VARG_QUALID pref] ->
+	   let ref = Termast.ast_of_qualid pref in
            (fun () ->
-	      let ref = global dummy_loc pref in
 	      Metasyntax.add_infix (Extend.gram_assoc assoc) n inf ref)
        | _ -> bad_vernac_args "INFIX")
 
@@ -1478,8 +1478,8 @@ let _ =
   add "DISTFIX"
     (function
        | [VARG_AST assoc; VARG_NUMBER n; VARG_STRING s; VARG_QUALID pref] ->
+	   let ref = Termast.ast_of_qualid pref in
            (fun () ->
-	      let ref = global dummy_loc pref in
               Metasyntax.add_distfix (Extend.gram_assoc assoc) n s ref)
        | _ -> bad_vernac_args "DISTFIX")