summaryrefslogtreecommitdiff
path: root/toplevel/vernac.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
commite978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch)
tree0de2a907ee93c795978f3c843155bee91c11ed60 /toplevel/vernac.ml
parent3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff)
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'toplevel/vernac.ml')
-rw-r--r--toplevel/vernac.ml47
1 files changed, 25 insertions, 22 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 64d77b74..afe72f0f 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: vernac.ml 7744 2005-12-27 09:16:06Z herbelin $ *)
+(* $Id: vernac.ml 8924 2006-06-08 17:49:01Z notin $ *)
(* Parsing of vernacular. *)
@@ -126,27 +126,30 @@ let rec vernac_com interpfun (loc,com) =
(* end translator state *)
(* coqdoc state *)
let cds = Constrintern.coqdoc_freeze() in
- if !Options.translate_file then begin
- let _,f = find_file_in_path (Library.get_load_paths ())
- (make_suffix fname ".v") in
- chan_translate := open_out (f^"8");
- Pp.comments := []
- end;
- begin try
- read_vernac_file verbosely (make_suffix fname ".v");
- if !Options.translate_file then close_out !chan_translate;
- chan_translate := ch;
- Lexer.restore_com_state cs;
- Pp.comments := cl;
- Constrintern.coqdoc_unfreeze cds;
- with e ->
- if !Options.translate_file then close_out !chan_translate;
- chan_translate := ch;
- Lexer.restore_com_state cs;
- Pp.comments := cl;
- Constrintern.coqdoc_unfreeze cds;
- raise e end;
-
+ if !Options.translate_file then
+ begin
+ let _,f = find_file_in_path (Library.get_load_paths ())
+ (make_suffix fname ".v") in
+ chan_translate := open_out (f^"8");
+ Pp.comments := []
+ end;
+ begin
+ try
+ read_vernac_file verbosely (make_suffix fname ".v");
+ if !Options.translate_file then close_out !chan_translate;
+ chan_translate := ch;
+ Lexer.restore_com_state cs;
+ Pp.comments := cl;
+ Constrintern.coqdoc_unfreeze cds
+ with e ->
+ if !Options.translate_file then close_out !chan_translate;
+ chan_translate := ch;
+ Lexer.restore_com_state cs;
+ Pp.comments := cl;
+ Constrintern.coqdoc_unfreeze cds;
+ raise e
+ end
+
| VernacList l -> List.iter (fun (_,v) -> interp v) l
| VernacTime v ->