diff options
| -rw-r--r-- | toplevel/vernac_classifier.ml | 6 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 38 |
2 files changed, 38 insertions, 6 deletions
diff --git a/toplevel/vernac_classifier.ml b/toplevel/vernac_classifier.ml index 3c14d5922..e6bb80be0 100644 --- a/toplevel/vernac_classifier.ml +++ b/toplevel/vernac_classifier.ml @@ -63,9 +63,6 @@ let rec classify_vernac e = | VernacStm (Observe id) -> VtStm (VtObserve id, true), VtNow | VernacStm (Command x) -> elide_part_of_script_and_now (classify_vernac x) | VernacStm (PGLast x) -> fst (classify_vernac x), VtNow - (* Impossible, Vernac handles these *) - | VernacList _ -> anomaly (str "VernacList not handled by Vernac") - | VernacLoad _ -> anomaly (str "VernacLoad not handled by Vernac") (* Nested vernac exprs *) | VernacProgram e -> classify_vernac e | VernacLocal (_,e) -> classify_vernac e @@ -149,6 +146,9 @@ let rec classify_vernac e = | VernacDeclareClass _ | VernacDeclareInstances _ | VernacRegister _ | VernacComments _ -> VtSideff [], VtLater + (* Who knows *) + | VernacList _ + | VernacLoad _ -> VtSideff [], VtNow (* (Local) Notations have to disappear *) | VernacEndSegment _ -> VtSideff [], VtNow (* Modules with parameters have to be executed: can import notations *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 6ddde1e3d..206a565f1 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1579,16 +1579,46 @@ let vernac_check_guard () = in msg_notice message +exception End_of_input + +let vernac_load interp fname = + let parse_sentence = Flags.with_option Flags.we_are_parsing + (fun po -> + match Pcoq.Gram.entry_parse Pcoq.main_entry po with + | Some x -> x + | None -> raise End_of_input) in + let open_utf8_file_in fname = + let is_bom s = + Int.equal (Char.code s.[0]) 0xEF && + Int.equal (Char.code s.[1]) 0xBB && + Int.equal (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 in + let fname = + Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in + let fname = CUnix.make_suffix fname ".v" in + let input = + let paths = Loadpath.get_paths () in + let _,longfname = + System.find_file_in_path ~warn:(Flags.is_verbose()) paths fname in + let in_chan = open_utf8_file_in longfname in + Pcoq.Gram.parsable (Stream.of_channel in_chan) in + try while true do interp (snd (parse_sentence input)) done + with End_of_input -> () + + (* "locality" is the prefix "Local" attribute, while the "local" component * is the outdated/deprecated "Local" attribute of some vernacular commands * still parsed as the obsolete_locality grammar entry for retrocompatibility *) let interp ?proof locality c = prerr_endline ("interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c)); match c with - (* Done in vernac *) - | (VernacList _|VernacLoad _) -> assert false - (* Done later in this file *) + | VernacList _ -> assert false + | VernacLoad _ -> assert false | VernacFail _ -> assert false | VernacTime _ -> assert false | VernacTimeout _ -> assert false @@ -1857,6 +1887,8 @@ let interp ?(verbosely=true) ?proof (loc,c) = let tend = System.get_time() in let msg = if !Flags.time then "" else "Finished transaction in " in msg_info (str msg ++ System.fmt_time_difference tstart tend) + | VernacList l -> List.iter (aux false) (List.map snd l) + | VernacLoad (_,fname) -> vernac_load (aux false) fname | c -> check_vernac_supports_locality c locality; Obligations.set_program_mode isprogcmd; |