diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqinit.ml | 11 | ||||
| -rw-r--r-- | toplevel/coqinit.mli | 2 | ||||
| -rw-r--r-- | toplevel/coqloop.ml | 59 | ||||
| -rw-r--r-- | toplevel/coqloop.mli | 2 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 39 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 182 | ||||
| -rw-r--r-- | toplevel/vernac.mli | 26 |
7 files changed, 128 insertions, 193 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index ffd0d7805..2b9a04dad 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -27,12 +27,12 @@ let set_rcfile s = rcfile := s; rcfile_specified := true let load_rc = ref true let no_load_rc () = load_rc := false -let load_rcfile() = +let load_rcfile sid = if !load_rc then try if !rcfile_specified then if CUnix.file_readable_p !rcfile then - Vernac.load_vernac false !rcfile + Vernac.load_vernac false sid !rcfile else raise (Sys_error ("Cannot read rcfile: "^ !rcfile)) else try @@ -43,8 +43,8 @@ let load_rcfile() = Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version; Envars.home ~warn / "."^rcdefaultname ] in - Vernac.load_vernac false inferedrc - with Not_found -> () + Vernac.load_vernac false sid inferedrc + with Not_found -> sid (* Flags.if_verbose mSGNL (str ("No coqrc or coqrc."^Coq_config.version^ @@ -55,7 +55,8 @@ let load_rcfile() = let () = Feedback.msg_info (str"Load of rcfile failed.") in iraise reraise else - Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading.") + (Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); + sid) (* Recursively puts dir in the LoadPath if -nois was not passed *) let add_stdlib_path ~unix_path ~coq_root ~with_ml = diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 4ff87628c..3b42289ee 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -13,7 +13,7 @@ val set_debug : unit -> unit val set_rcfile : string -> unit val no_load_rc : unit -> unit -val load_rcfile : unit -> unit +val load_rcfile : Stateid.t -> Stateid.t val push_include : string -> Names.DirPath.t -> bool -> unit (** [push_include phys_path log_path implicit] *) diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 2282932d4..4641a2bc8 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -7,11 +7,6 @@ (************************************************************************) open Pp -open CErrors -open Util -open Flags -open Vernac -open Pcoq let top_stderr x = Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with x @@ -24,7 +19,7 @@ type input_buffer = { mutable str : Bytes.t; (* buffer of already read characters *) mutable len : int; (* number of chars in the buffer *) mutable bols : int list; (* offsets in str of beginning of lines *) - mutable tokens : Gram.coq_parsable; (* stream of tokens *) + mutable tokens : Pcoq.Gram.coq_parsable; (* stream of tokens *) mutable start : int } (* stream count of the first char of the buffer *) (* Double the size of the buffer. *) @@ -61,7 +56,7 @@ let prompt_char ic ibuf count = | ll::_ -> Int.equal ibuf.len ll | [] -> Int.equal ibuf.len 0 in - if bol && not !print_emacs then top_stderr (str (ibuf.prompt())); + if bol && not !Flags.print_emacs then top_stderr (str (ibuf.prompt())); try let c = input_char ic in if c == '\n' then ibuf.bols <- (ibuf.len+1) :: ibuf.bols; @@ -78,7 +73,7 @@ let reset_input_buffer ic ibuf = ibuf.str <- Bytes.empty; ibuf.len <- 0; ibuf.bols <- []; - ibuf.tokens <- Gram.parsable (Stream.from (prompt_char ic ibuf)); + ibuf.tokens <- Pcoq.Gram.parsable (Stream.from (prompt_char ic ibuf)); ibuf.start <- 0 (* Functions to print underlined locations from an input buffer. *) @@ -89,7 +84,7 @@ module TopErr = struct let get_bols_of_loc ibuf (bp,ep) = let add_line (b,e) lines = - if b < 0 || e < b then anomaly (Pp.str "Bad location"); + if b < 0 || e < b then CErrors.anomaly (Pp.str "Bad location"); match lines with | ([],None) -> ([], Some (b,e)) | (fl,oe) -> ((b,e)::fl, oe) @@ -174,7 +169,7 @@ let error_info_for_buffer ?loc buf = let fname = loc.Loc.fname in let hl, loc = (* We are in the toplevel *) - if String.equal fname "" then + if CString.equal fname "" then let nloc = adjust_loc_buf buf loc in if valid_buffer_loc buf loc then (fnl () ++ print_highlight_location buf nloc, nloc) @@ -223,7 +218,7 @@ let make_emacs_prompt() = let pending = Stm.get_all_proof_names() in let pendingprompt = List.fold_left - (fun acc x -> acc ^ (if String.is_empty acc then "" else "|") ^ Names.Id.to_string x) + (fun acc x -> acc ^ (if CString.is_empty acc then "" else "|") ^ Names.Id.to_string x) "" pending in let proof_info = if dpth >= 0 then string_of_int dpth else "0" in if !Flags.print_emacs then statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < " @@ -243,7 +238,7 @@ let top_buffer = str = Bytes.empty; len = 0; bols = []; - tokens = Gram.parsable (Stream.of_list []); + tokens = Pcoq.Gram.parsable (Stream.of_list []); start = 0 } let set_prompt prompt = @@ -257,10 +252,10 @@ let set_prompt prompt = let parse_to_dot = let rec dot st = match Stream.next st with | Tok.KEYWORD ("."|"...") -> () - | Tok.EOI -> raise End_of_input + | Tok.EOI -> raise Stm.End_of_input | _ -> dot st in - Gram.Entry.of_parser "Coqtoplevel.dot" dot + Pcoq.Gram.Entry.of_parser "Coqtoplevel.dot" dot (* If an error occurred while parsing, we try to read the input until a dot token is encountered. @@ -268,21 +263,19 @@ let parse_to_dot = let rec discard_to_dot () = try - Gram.entry_parse parse_to_dot top_buffer.tokens + Pcoq.Gram.entry_parse parse_to_dot top_buffer.tokens with | Token.Error _ | CLexer.Error.E _ -> discard_to_dot () - | End_of_input -> raise End_of_input + | Stm.End_of_input -> raise Stm.End_of_input | e when CErrors.noncritical e -> () -let read_sentence input = - try - let (loc, _ as r) = Vernac.parse_sentence input in - CWarnings.set_current_loc loc; r +let read_sentence sid input = + try Stm.parse_sentence sid input with reraise -> let reraise = CErrors.push reraise in discard_to_dot (); TopErr.print_toplevel_parse_error reraise top_buffer; - iraise reraise + Exninfo.iraise reraise (** Coqloop Console feedback handler *) let coqloop_feed (fb : Feedback.feedback) = let open Feedback in @@ -312,25 +305,24 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in is caught and handled (i.e. not re-raised). *) -let do_vernac () = +let do_vernac sid = top_stderr (fnl()); - if !print_emacs then top_stderr (str (top_buffer.prompt())); + if !Flags.print_emacs then top_stderr (str (top_buffer.prompt())); resynch_buffer top_buffer; try let input = (top_buffer.tokens, None) in - Vernac.process_expr top_buffer.tokens (read_sentence input) + Vernac.process_expr sid top_buffer.tokens (read_sentence sid (fst input)) with - | End_of_input | CErrors.Quit -> + | Stm.End_of_input | CErrors.Quit -> top_stderr (fnl ()); raise CErrors.Quit | CErrors.Drop -> (* Last chance *) if Mltop.is_ocaml_top() then raise CErrors.Drop - else Feedback.msg_error (str "There is no ML toplevel.") + else (Feedback.msg_error (str "There is no ML toplevel."); sid) (* Exception printing is done now by the feedback listener. *) (* XXX: We need this hack due to the side effects of the exception printer and the reliance of Stm.define on attaching crutial state to exceptions *) - | any -> ignore (CErrors.(iprint (push any))) - + | any -> ignore (CErrors.(iprint (push any))); sid (** Main coq loop : read vernacular expressions until Drop is entered. Ctrl-C is handled internally as Sys.Break instead of aborting Coq. @@ -348,11 +340,16 @@ let loop_flush_all () = let rec loop () = Sys.catch_break true; - if !Flags.print_emacs then Vernacentries.qed_display_script := false; - Flags.coqtop_ui := true; try reset_input_buffer stdin top_buffer; - while true do do_vernac(); loop_flush_all () done + (* Be careful to keep this loop tail-recursive *) + let rec vernac_loop sid = + let nsid = do_vernac sid in + loop_flush_all (); + vernac_loop nsid + (* We recover the current stateid, threading from the caller is + not possible due exceptions. *) + in vernac_loop (Stm.get_current_state ()) with | CErrors.Drop -> () | CErrors.Quit -> exit 0 diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index 8a34ded6d..66bbf43f6 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -31,7 +31,7 @@ val coqloop_feed : Feedback.feedback -> unit (** Parse and execute one vernac command. *) -val do_vernac : unit -> unit +val do_vernac : Stateid.t -> Stateid.t (** Main entry point of Coq: read and execute vernac commands. *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index aca94e63d..c259beb17 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -8,11 +8,8 @@ open Pp open CErrors -open Util open Flags -open Names open Libnames -open States open Coqinit let () = at_exit flush_all @@ -133,10 +130,10 @@ let engage () = let set_batch_mode () = batch_mode := true -let toplevel_default_name = DirPath.make [Id.of_string "Top"] +let toplevel_default_name = Names.(DirPath.make [Id.of_string "Top"]) let toplevel_name = ref toplevel_default_name let set_toplevel_name dir = - if DirPath.is_empty dir then error "Need a non empty toplevel module name"; + if Names.DirPath.is_empty dir then error "Need a non empty toplevel module name"; toplevel_name := dir let remove_top_ml () = Mltop.remove () @@ -150,9 +147,9 @@ let set_inputstate s = warn_deprecated_inputstate (); inputstate:=s let inputstate () = - if not (String.is_empty !inputstate) then + if not (CString.is_empty !inputstate) then let fname = Loadpath.locate_file (CUnix.make_suffix !inputstate ".coq") in - intern_state fname + States.intern_state fname let warn_deprecated_outputstate = CWarnings.create ~name:"deprecated-outputstate" ~category:"deprecated" @@ -164,9 +161,9 @@ let set_outputstate s = warn_deprecated_outputstate (); outputstate:=s let outputstate () = - if not (String.is_empty !outputstate) then + if not (CString.is_empty !outputstate) then let fname = CUnix.make_suffix !outputstate ".coq" in - extern_state fname + States.extern_state fname let set_include d p implicit = let p = dirpath_of_string p in @@ -175,15 +172,15 @@ let set_include d p implicit = let load_vernacular_list = ref ([] : (string * bool) list) let add_load_vernacular verb s = load_vernacular_list := ((CUnix.make_suffix s ".v"),verb) :: !load_vernacular_list -let load_vernacular () = - List.iter - (fun (s,b) -> +let load_vernacular sid = + List.fold_left + (fun sid (s,v) -> let s = Loadpath.locate_file s in if !Flags.beautify then - with_option beautify_file (Vernac.load_vernac b) s + with_option beautify_file (Vernac.load_vernac v sid) s else - Vernac.load_vernac b s) - (List.rev !load_vernacular_list) + Vernac.load_vernac v sid s) + sid (List.rev !load_vernacular_list) let load_vernacular_obj = ref ([] : string list) let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj @@ -250,7 +247,6 @@ let set_emacs () = if not (Option.is_empty !toploop) then error "Flag -emacs is incompatible with a custom toplevel loop"; Flags.print_emacs := true; - Vernacentries.qed_display_script := false; color := `OFF (** Options for CoqIDE *) @@ -380,7 +376,7 @@ let get_host_port opt s = let get_error_resilience opt = function | "on" | "all" | "yes" -> `All | "off" | "no" -> `None - | s -> `Only (String.split ',' s) + | s -> `Only (CString.split ',' s) let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s) @@ -625,7 +621,7 @@ let init_toplevel arglist = init_load_path (); Option.iter Mltop.load_ml_object_raw !toploop; let extras = !toploop_init extras in - if not (List.is_empty extras) then begin + if not (CList.is_empty extras) then begin prerr_endline ("Don't know what to do with "^String.concat " " extras); prerr_endline "See -help for the list of supported options"; exit 1 @@ -634,15 +630,16 @@ let init_toplevel arglist = inputstate (); Mltop.init_known_plugins (); engage (); - if (not !batch_mode || List.is_empty !compile_list) + if (not !batch_mode || CList.is_empty !compile_list) && Global.env_is_initial () then Declaremods.start_library !toplevel_name; init_library_roots (); load_vernac_obj (); require (); Stm.init (); - load_rcfile(); - load_vernacular (); + let sid = load_rcfile (Stm.get_current_state ()) in + (* XXX: We ignore this for now, but should be threaded to the toplevels *) + let _sid = load_vernacular sid in compile_files (); schedule_vio_checking (); schedule_vio_compilation (); diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 9917a49b4..98458a57a 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -13,111 +13,30 @@ open CErrors open Util open Flags open Vernacexpr +open Vernacprop (* The functions in this module may raise (unexplainable!) exceptions. Use the module Coqtoplevel, which catches these exceptions (the exceptions are explained only at the toplevel). *) -let user_error loc s = CErrors.user_err ~loc (str s) - -(* Navigation commands are allowed in a coqtop session but not in a .v file *) - -let rec is_navigation_vernac = function - | VernacResetInitial - | VernacResetName _ - | VernacBacktrack _ - | VernacBackTo _ - | VernacBack _ - | VernacStm _ -> true - | VernacRedirect (_, (_,c)) - | VernacTime (_,c) -> - is_navigation_vernac c (* Time Back* is harmless *) - | c -> is_deep_navigation_vernac c - -and is_deep_navigation_vernac = function - | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c - | _ -> false - -(* NB: Reset is now allowed again as asked by A. Chlipala *) - -let is_reset = function - | VernacResetInitial | VernacResetName _ -> true - | _ -> false - -let checknav_simple loc cmd = +let checknav_simple (loc, cmd) = if is_navigation_vernac cmd && not (is_reset cmd) then - user_error loc "Navigation commands forbidden in files." + CErrors.user_err ~loc (str "Navigation commands forbidden in files.") -let checknav_deep loc ast = +let checknav_deep (loc, ast) = if is_deep_navigation_vernac ast then - user_error loc "Navigation commands forbidden in nested commands." - -(* When doing Load on a file, two behaviors are possible: - - - either the history stack is grown by only one command, - the "Load" itself. This is mandatory for command-counting - interfaces (CoqIDE). - - - either each individual sub-commands in the file is added - to the history stack. This allows commands like Show Script - to work across the loaded file boundary (cf. bug #2820). - - The best of the two could probably be combined someday, - in the meanwhile we use a flag. *) - -let atomic_load = ref true - -let _ = - Goptions.declare_bool_option - { Goptions.optsync = true; - Goptions.optdepr = false; - Goptions.optname = "atomic registration of commands in a Load"; - Goptions.optkey = ["Atomic";"Load"]; - Goptions.optread = (fun () -> !atomic_load); - Goptions.optwrite = ((:=) atomic_load) } + CErrors.user_err ~loc (str "Navigation commands forbidden in nested commands.") let disable_drop = function | Drop -> CErrors.error "Drop is forbidden." | e -> e -(* 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 - the file we parse seems a bit risky to me. B.B. *) - -let open_file_twice_if verbosely longfname = - 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 ~file:longfname (Stream.of_channel in_chan) in - (in_chan, longfname, (po, verb_ch)) - -let close_input in_chan (_,verb) = - try - close_in in_chan; - match verb with - | Some verb_ch -> close_in verb_ch - | _ -> () - with e when CErrors.noncritical e -> () - -let verbose_phrase verbch loc = - let loc = Loc.unloc loc in - match verbch with - | Some ch -> - let len = snd loc - fst loc in - let s = Bytes.create len in - seek_in ch (fst loc); - really_input ch s 0 len; - Feedback.msg_notice (str (Bytes.to_string s)) - | None -> () - -exception End_of_input - -let parse_sentence = Flags.with_option Flags.we_are_parsing - (fun (po, verbch) -> - match Pcoq.Gram.entry_parse Pcoq.main_entry po with - | Some (loc,_ as com) -> verbose_phrase verbch loc; com - | None -> raise End_of_input) +(* Echo from a buffer based on position. + XXX: Should move to utility file. *) +let vernac_echo loc in_chan = let open Loc in + let len = loc.ep - loc.bp in + seek_in in_chan loc.bp; + Feedback.msg_notice @@ str @@ really_input_string in_chan len (* vernac parses the given stream, executes interpfun on the syntax tree it * parses, and is verbose on "primitives" commands if verbosely is true *) @@ -184,20 +103,43 @@ let print_cmd_header loc com = Pp.pp_with !Topfmt.std_ft (pp_cmd_header loc com); Format.pp_print_flush !Topfmt.std_ft () -let rec interp_vernac po chan_beautify checknav (loc,com) = +let pr_open_cur_subgoals () = + try Printer.pr_open_subgoals () + with Proof_global.NoCurrentProof -> Pp.str "" + +let rec interp_vernac sid po (loc,com) = let interp = function | VernacLoad (verbosely, fname) -> let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in let fname = CUnix.make_suffix fname ".v" in let f = Loadpath.locate_file fname in - load_vernac verbosely f - - | v -> Stm.interp (Flags.is_verbose()) (loc,v) + load_vernac verbosely sid f + | v -> + try + let nsid, ntip = Stm.add sid (Flags.is_verbose()) (loc,v) in + + (* Main STM interaction *) + if ntip <> `NewTip then + anomaly (str "vernac.ml: We got an unfocus operation on the toplevel!"); + (* Due to bug #5363 we cannot use observe here as we should, + it otherwise reveals bugs *) + (* Stm.observe nsid; *) + Stm.finish (); + + (* We could use a more refined criteria depending on the + vernac. For now we imitate the old approach. *) + let print_goals = not (!Flags.batch_mode || is_query v) in + + if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); + nsid + + with exn when CErrors.noncritical exn -> + ignore(Stm.edit_at sid); + raise exn in try - checknav loc com; - if !beautify then pr_new_syntax po chan_beautify loc (Some com); - (* XXX: This is not 100% correct if called from an IDE context *) + (* The -time option is only supported from console-based + clients due to the way it prints. *) if !Flags.time then print_cmd_header loc com; let com = if !Flags.time then VernacTime (loc,com) else com in interp com @@ -208,26 +150,39 @@ let rec interp_vernac po chan_beautify checknav (loc,com) = else iraise (reraise, info) (* Load a vernac file. CErrors are annotated with file and location *) -and load_vernac verbosely file = +and load_vernac verbosely sid file = let chan_beautify = if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout in - let (in_chan, fname, input) = open_file_twice_if verbosely file in + let in_chan = open_utf8_file_in file in + let in_echo = if verbosely then Some (open_utf8_file_in file) else None in + let in_pa = Pcoq.Gram.parsable ~file (Stream.of_channel in_chan) in + let rsid = ref sid 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 - let loc_ast = Flags.silently parse_sentence input in - CWarnings.set_current_loc (fst loc_ast); - Flags.silently (interp_vernac (fst input) chan_beautify checknav_simple) loc_ast; - done + let loc, ast = Stm.parse_sentence !rsid in_pa in + + (* Printing of vernacs *) + if !beautify then pr_new_syntax in_pa chan_beautify loc (Some ast); + Option.iter (vernac_echo loc) in_echo; + + checknav_simple (loc, ast); + let nsid = Flags.silently (interp_vernac !rsid in_pa) (loc, ast) in + rsid := nsid + done; + !rsid with any -> (* whatever the exception *) let (e, info) = CErrors.push any in - close_input in_chan input; (* we must close the file first *) + close_in in_chan; + Option.iter close_in in_echo; match e with - | End_of_input -> + | Stm.End_of_input -> + (* Is this called so comments at EOF are printed? *) if !beautify then - pr_new_syntax (fst input) chan_beautify (Loc.make_loc (max_int,max_int)) None; + pr_new_syntax in_pa chan_beautify (Loc.make_loc (max_int,max_int)) None; if !Flags.beautify_file then close_out chan_beautify; + !rsid | reraise -> if !Flags.beautify_file then close_out chan_beautify; iraise (disable_drop e, info) @@ -239,7 +194,9 @@ and load_vernac verbosely file = of a new state label). An example of state-preserving command is one coming from the query panel of Coqide. *) -let process_expr po loc_ast = interp_vernac po stdout checknav_deep loc_ast +let process_expr sid po loc_ast = + checknav_deep loc_ast; + interp_vernac sid po loc_ast (* XML output hooks *) let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore () @@ -308,7 +265,7 @@ let compile verbosely f = Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); if !Flags.xml_export then Hook.get f_xml_start_library (); let wall_clock1 = Unix.gettimeofday () in - let _ = load_vernac verbosely long_f_dot_v in + let _ = load_vernac verbosely (Stm.get_current_state ()) long_f_dot_v in Stm.join (); let wall_clock2 = Unix.gettimeofday () in check_pending_proofs (); @@ -328,7 +285,7 @@ let compile verbosely f = let ldir = Flags.verbosely Library.start_library long_f_dot_vio in Dumpglob.noglob (); Stm.set_compilation_hints long_f_dot_vio; - let _ = load_vernac verbosely long_f_dot_v in + let _ = load_vernac verbosely (Stm.get_current_state ()) long_f_dot_v in Stm.finish (); check_pending_proofs (); Stm.snapshot_vio ldir long_f_dot_vio; @@ -347,6 +304,3 @@ let compile v f = ignore(CoqworkmgrApi.get 1); compile v f; CoqworkmgrApi.giveback 1 - -let () = Hook.set Stm.process_error_hook - ExplainErr.process_vernac_interp_error diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index 0d9f5871a..e75f8f9e8 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -8,30 +8,16 @@ (** Parsing of vernacular. *) -(** Read a vernac command on the specified input (parse only). - Raises [End_of_file] if EOF (or Ctrl-D) is reached. *) - -val parse_sentence : Pcoq.Gram.coq_parsable * in_channel option -> - Loc.t * Vernacexpr.vernac_expr - (** Reads and executes vernac commands from a stream. *) +val process_expr : Stateid.t -> Pcoq.Gram.coq_parsable -> Vernacexpr.vernac_expr Loc.located -> Stateid.t -exception End_of_input +(** [load_vernac echo sid file] Loads [file] on top of [sid], will + echo the commands if [echo] is set. *) +val load_vernac : bool -> Stateid.t -> string -> Stateid.t -val process_expr : Pcoq.Gram.coq_parsable -> Loc.t * Vernacexpr.vernac_expr -> unit +(** Compile a vernac file, (f is assumed without .v suffix) *) +val compile : bool -> string -> unit (** Set XML hooks *) val xml_start_library : (unit -> unit) Hook.t val xml_end_library : (unit -> unit) Hook.t - -(** Load a vernac file, verbosely or not. Errors are annotated with file - and location *) - -val load_vernac : bool -> string -> unit - - -(** Compile a vernac file, verbosely or not (f is assumed without .v suffix) *) - -val compile : bool -> string -> unit - -val is_navigation_vernac : Vernacexpr.vernac_expr -> bool |