diff options
Diffstat (limited to 'toplevel/vernac.ml')
| -rw-r--r-- | toplevel/vernac.ml | 65 |
1 files changed, 44 insertions, 21 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 84e20f5e..ed20fc60 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -51,6 +51,8 @@ let real_error = function | Error_in_file (_, _, e) -> e | e -> e +let user_error loc s = Util.user_err_loc (loc,"_",str s) + (** Timeout handling *) (** A global default timeout, controled by option "Set Default Timeout n". @@ -97,6 +99,18 @@ let restore_timeout = function (* restore handler *) Sys.set_signal Sys.sigalrm psh + +(* Open an utf-8 encoded file and skip the byte-order mark if any *) + +let open_utf8_file_in fname = + let is_bom s = + Char.code s.[0] = 0xEF && Char.code s.[1] = 0xBB && Char.code s.[2] = 0xBF + in + let in_chan = open_in fname in + let s = " " in + if input in_chan s 0 3 < 3 || not (is_bom s) then seek_in in_chan 0; + in_chan + (* Opening and closing a channel. Open it twice when verbose: the first channel is used to read the commands, and the second one to print them. Note: we could use only one thanks to seek_in, but seeking on and on in @@ -106,8 +120,9 @@ let open_file_twice_if verbosely fname = let paths = Library.get_load_paths () in let _,longfname = find_file_in_path ~warn:(Flags.is_verbose()) paths fname in - let in_chan = open_in longfname in - let verb_ch = if verbosely then Some (open_in longfname) else None in + let in_chan = open_utf8_file_in longfname in + let verb_ch = + if verbosely then Some (open_utf8_file_in longfname) else None in let po = Pcoq.Gram.parsable (Stream.of_channel in_chan) in (in_chan, longfname, (po, verb_ch)) @@ -166,7 +181,7 @@ let pr_new_syntax loc ocom = States.unfreeze fs; Format.set_formatter_out_channel stdout -let rec vernac_com interpfun (loc,com) = +let rec vernac_com interpfun checknav (loc,com) = let rec interp = function | VernacLoad (verbosely, fname) -> let fname = expand_path_macros fname in @@ -204,9 +219,13 @@ let rec vernac_com interpfun (loc,com) = | VernacList l -> List.iter (fun (_,v) -> interp v) l + | v when !just_parsing -> () + | VernacFail v -> - if not !just_parsing then begin try - interp v; raise HasNotFailed + begin try + (* If the command actually works, ignore its effects on the state *) + States.with_state_protection + (fun v -> interp v; raise HasNotFailed) v with e -> match real_error e with | HasNotFailed -> errorlabstrm "Fail" (str "The command has not failed !") @@ -219,22 +238,17 @@ let rec vernac_com interpfun (loc,com) = end | VernacTime v -> - if not !just_parsing then begin let tstart = System.get_time() in interp v; let tend = System.get_time() in msgnl (str"Finished transaction in " ++ System.fmt_time_difference tstart tend) - end | VernacTimeout(n,v) -> - if not !just_parsing then begin current_timeout := Some n; interp v - end | v -> - if not !just_parsing then let psh = default_set_timeout () in try States.with_heavy_rollback interpfun @@ -243,6 +257,7 @@ let rec vernac_com interpfun (loc,com) = with e -> restore_timeout psh; raise e in try + checknav loc com; current_timeout := !default_timeout; if do_beautify () then pr_new_syntax loc (Some com); interp com @@ -256,13 +271,17 @@ and read_vernac_file verbosely s = if verbosely then Vernacentries.interp else Flags.silently Vernacentries.interp in + let checknav loc cmd = + if is_navigation_vernac cmd then + user_error loc "Navigation commands forbidden in files" + in let (in_chan, fname, input) = open_file_twice_if verbosely s in try (* we go out of the following infinite loop when a End_of_input is * raised, which means that we raised the end of the file being loaded *) while true do - vernac_com interpfun (parse_sentence input); + vernac_com interpfun checknav (parse_sentence input); pp_flush () done with e -> (* whatever the exception *) @@ -273,15 +292,21 @@ and read_vernac_file verbosely s = if do_beautify () then pr_new_syntax (make_loc (max_int,max_int)) None | _ -> raise_with_file fname e +(** [eval_expr : ?preserving:bool -> Pp.loc * Vernacexpr.vernac_expr -> unit] + It executes one vernacular command. By default the command is + considered as non-state-preserving, in which case we add it to the + Backtrack stack (triggering a save of a frozen state and the generation + of a new state label). An example of state-preserving command is one coming + from the query panel of Coqide. *) -(* eval_expr : Util.loc * Vernacexpr.vernac_expr -> unit - * execute one vernacular command. Marks the end of the command in the lib_stk - * with a new label to make vernac undoing easier. Also freeze state to speed up - * backtracking. *) -let eval_expr last = - vernac_com Vernacentries.interp last; - Lib.add_frozen_state(); - Lib.mark_end_of_command() +let checknav loc ast = + if is_deep_navigation_vernac ast then + user_error loc "Navigation commands forbidden in nested commands" + +let eval_expr ?(preserving=false) loc_ast = + vernac_com Vernacentries.interp checknav loc_ast; + if not preserving && not (is_navigation_vernac (snd loc_ast)) then + Backtrack.mark_command (snd loc_ast) (* raw_do_vernac : Pcoq.Gram.parsable -> unit * vernac_step . parse_sentence *) @@ -317,5 +342,3 @@ let compile verbosely f = if !Flags.xml_export then !xml_end_library (); Dumpglob.end_dump_glob (); Library.save_library_to ldir (long_f_dot_v ^ "o") - - |