summaryrefslogtreecommitdiff
path: root/toplevel/vernac.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
treead89c6bb57ceee608fcba2bb3435b74e0f57919e /toplevel/vernac.ml
parent018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'toplevel/vernac.ml')
-rw-r--r--toplevel/vernac.ml86
1 files changed, 7 insertions, 79 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index a5716619..64d77b74 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: vernac.ml,v 1.59.2.3 2004/07/16 20:48:17 herbelin Exp $ *)
+(* $Id: vernac.ml 7744 2005-12-27 09:16:06Z herbelin $ *)
(* Parsing of vernacular. *)
@@ -15,10 +15,9 @@ open Lexer
open Util
open Options
open System
-open Coqast
open Vernacexpr
open Vernacinterp
-open Ppvernacnew
+open Ppvernac
(* The functions in this module may raise (unexplainable!) exceptions.
Use the module Coqtoplevel, which catches these exceptions
@@ -57,7 +56,7 @@ let real_error = function
the file we parse seems a bit risky to me. B.B. *)
let open_file_twice_if verbosely fname =
- let _,longfname = find_file_in_path (Library.get_load_path ()) fname in
+ let _,longfname = find_file_in_path (Library.get_load_paths ()) fname in
let in_chan = open_in longfname in
let verb_ch = if verbosely then Some (open_in longfname) else None in
let po = Pcoq.Gram.parsable (Stream.of_channel in_chan) in
@@ -95,62 +94,18 @@ let parse_phrase (po, verbch) =
let just_parsing = ref false
let chan_translate = ref stdout
-let last_char = ref '\000'
-(* postprocessor to avoid lexical icompatibilities between V7 and V8.
- Ex: auto.(* comment *) or simpl.auto
- *)
let set_formatter_translator() =
let ch = !chan_translate in
- let out s b e =
- let n = e-b in
- if n > 0 then begin
- (match !last_char with
- '.' ->
- (match s.[b] with
- '('|'a'..'z'|'A'..'Z' -> output ch " " 0 1
- | _ -> ())
- | _ -> ());
- last_char := s.[e-1]
- end;
- output ch s b e
- in
+ let out s b e = output ch s b e in
Format.set_formatter_output_functions out (fun () -> flush ch);
Format.set_max_boxes max_int
-let pre_printing = function
- | VernacSolve (i,tac,deftac) when Options.do_translate () ->
- (try
- let (_,env) = Pfedit.get_goal_context i in
- let t = Options.with_option Options.translate_syntax
- (Tacinterp.glob_tactic_env [] env) tac in
- let pfts = Pfedit.get_pftreestate () in
- let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in
- Some (env,t,Pfedit.focus(),List.length gls)
- with UserError _|Stdpp.Exc_located _ -> None)
- | _ -> None
-
-let post_printing loc (env,t,f,n) = function
- | VernacSolve (i,_,deftac) ->
- let loc = unloc loc in
- set_formatter_translator();
- let pp = Ppvernacnew.pr_vernac_solve (i,env,t,deftac) ++ sep_end () in
- (if !translate_file then begin
- msg (hov 0 (comment (fst loc) ++ pp ++ comment (snd loc - 1)));
- end
- else
- msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ pp)));
- Format.set_formatter_out_channel stdout
- | _ -> ()
-
let pr_new_syntax loc ocom =
let loc = unloc loc in
if !translate_file then set_formatter_translator();
let fs = States.freeze () in
let com = match ocom with
- | Some (VernacV7only _) ->
- Options.v7_only := true;
- mt()
| Some VernacNop -> mt()
| Some com -> pr_vernac com
| None -> mt() in
@@ -159,8 +114,6 @@ let pr_new_syntax loc ocom =
else
msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
States.unfreeze fs;
- Constrintern.set_temporary_implicits_in [];
- Constrextern.set_temporary_implicits_out [];
Format.set_formatter_out_channel stdout
let rec vernac_com interpfun (loc,com) =
@@ -174,7 +127,7 @@ let rec vernac_com interpfun (loc,com) =
(* coqdoc state *)
let cds = Constrintern.coqdoc_freeze() in
if !Options.translate_file then begin
- let _,f = find_file_in_path (Library.get_load_path ())
+ let _,f = find_file_in_path (Library.get_load_paths ())
(make_suffix fname ".v") in
chan_translate := open_out (f^"8");
Pp.comments := []
@@ -203,39 +156,14 @@ let rec vernac_com interpfun (loc,com) =
msgnl (str"Finished transaction in " ++
System.fmt_time_difference tstart tend)
- (* To be interpreted in v7 or translator input only *)
- | VernacV7only v ->
- Options.v7_only := true;
- if !Options.v7 || Options.do_translate() then interp v;
- Options.v7_only := false
-
- (* To be interpreted in translator output only *)
- | VernacV8only v ->
- if not !Options.v7 && not (do_translate()) then
- interp v
-
| v -> if not !just_parsing then interpfun v
in
try
- Options.v7_only := false;
- if do_translate () then
- match pre_printing com with
- None ->
- pr_new_syntax loc (Some com);
- interp com
- | Some state ->
- (try
- interp com;
- post_printing loc state com
- with e ->
- post_printing loc state com;
- raise e)
- else
- interp com
+ if do_translate () then pr_new_syntax loc (Some com);
+ interp com
with e ->
Format.set_formatter_out_channel stdout;
- Options.v7_only := false;
raise (DuringCommandInterp (loc, e))
and vernac interpfun input =