diff options
| -rw-r--r-- | Makefile.build | 3 | ||||
| -rw-r--r-- | Makefile.common | 8 | ||||
| -rw-r--r-- | lib/lib.mllib | 5 | ||||
| -rw-r--r-- | myocamlbuild.ml | 3 | ||||
| -rw-r--r-- | stm/dag.ml (renamed from lib/dag.ml) | 0 | ||||
| -rw-r--r-- | stm/dag.mli (renamed from lib/dag.mli) | 0 | ||||
| -rw-r--r-- | stm/lemmas.ml (renamed from toplevel/lemmas.ml) | 0 | ||||
| -rw-r--r-- | stm/lemmas.mli (renamed from toplevel/lemmas.mli) | 0 | ||||
| -rw-r--r-- | stm/spawned.ml (renamed from lib/spawned.ml) | 0 | ||||
| -rw-r--r-- | stm/spawned.mli (renamed from lib/spawned.mli) | 0 | ||||
| -rw-r--r-- | stm/stm.ml (renamed from toplevel/stm.ml) | 13 | ||||
| -rw-r--r-- | stm/stm.mli (renamed from toplevel/stm.mli) | 5 | ||||
| -rw-r--r-- | stm/stm.mllib | 9 | ||||
| -rw-r--r-- | stm/tQueue.ml (renamed from lib/tQueue.ml) | 0 | ||||
| -rw-r--r-- | stm/tQueue.mli (renamed from lib/tQueue.mli) | 0 | ||||
| -rw-r--r-- | stm/vcs.ml (renamed from lib/vcs.ml) | 0 | ||||
| -rw-r--r-- | stm/vcs.mli (renamed from lib/vcs.mli) | 0 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml (renamed from toplevel/vernac_classifier.ml) | 0 | ||||
| -rw-r--r-- | stm/vernac_classifier.mli (renamed from toplevel/vernac_classifier.mli) | 0 | ||||
| -rw-r--r-- | stm/vi_checking.ml (renamed from toplevel/vi_checking.ml) | 0 | ||||
| -rw-r--r-- | stm/vi_checking.mli (renamed from toplevel/vi_checking.mli) | 0 | ||||
| -rw-r--r-- | stm/workerPool.ml (renamed from lib/workerPool.ml) | 0 | ||||
| -rw-r--r-- | stm/workerPool.mli (renamed from lib/workerPool.mli) | 0 | ||||
| -rw-r--r-- | toplevel/toplevel.mllib | 4 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 7 | ||||
| -rw-r--r-- | toplevel/vernacentries.mli | 1 |
26 files changed, 34 insertions, 24 deletions
diff --git a/Makefile.build b/Makefile.build index 91817a94a..dd7b20f0f 100644 --- a/Makefile.build +++ b/Makefile.build @@ -388,7 +388,7 @@ test-suite: world $(ALLSTDLIB).v ################################################################## .PHONY: lib kernel byterun library proofs tactics interp parsing pretyping -.PHONY: highparsing toplevel hightactics +.PHONY: highparsing stm toplevel hightactics lib: lib/clib.cma lib/lib.cma kernel: kernel/kernel.cma @@ -400,6 +400,7 @@ interp: interp/interp.cma parsing: parsing/parsing.cma pretyping: pretyping/pretyping.cma highparsing: parsing/highparsing.cma +stm: stm/stm.cma toplevel: toplevel/toplevel.cma hightactics: tactics/hightactics.cma diff --git a/Makefile.common b/Makefile.common index 7425d99af..d45c1d561 100644 --- a/Makefile.common +++ b/Makefile.common @@ -61,8 +61,8 @@ CSDPCERT:=plugins/micromega/csdpcert$(EXE) CORESRCDIRS:=\ config lib kernel kernel/byterun library \ - proofs tactics pretyping interp toplevel \ - parsing printing grammar intf + proofs tactics pretyping interp stm \ + toplevel parsing printing grammar intf PLUGINS:=\ omega romega micromega quote \ @@ -157,7 +157,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \ CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ parsing/parsing.cma printing/printing.cma tactics/tactics.cma \ - toplevel/toplevel.cma parsing/highparsing.cma tactics/hightactics.cma + stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma tactics/hightactics.cma GRAMMARCMA:=tools/compat5.cmo grammar/grammar.cma @@ -354,7 +354,7 @@ OCAMLDOCDIR=dev/ocamldoc DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \ ./pretyping/*.mli ./interp/*.mli printing/*.mli \ ./parsing/*.mli ./proofs/*.mli \ - ./tactics/*.mli ./toplevel/*.mli) + ./tactics/*.mli ./stm/*.mli ./toplevel/*.mli) # Defining options to generate dependencies graphs DOT=dot diff --git a/lib/lib.mllib b/lib/lib.mllib index 50621df20..edef3da03 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -10,7 +10,6 @@ Unicode System CThread Spawn -Spawned Trie Profile Explore @@ -23,7 +22,3 @@ Genarg Ephemeron Future RemoteCounter -Dag -Vcs -TQueue -WorkerPool diff --git a/myocamlbuild.ml b/myocamlbuild.ml index 6d3a24306..097a10425 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -106,7 +106,8 @@ let core_libs = ["lib/clib"; "lib/lib"; "kernel/kernel"; "library/library"; "pretyping/pretyping"; "interp/interp"; "proofs/proofs"; "parsing/parsing"; "printing/printing"; "tactics/tactics"; - "toplevel/toplevel"; "parsing/highparsing"; "tactics/hightactics"] + "stm/stm"; "toplevel/toplevel"; "parsing/highparsing"; + "tactics/hightactics"] let core_cma = List.map (fun s -> s^".cma") core_libs let core_cmxa = List.map (fun s -> s^".cmxa") core_libs let core_mllib = List.map (fun s -> s^".mllib") core_libs diff --git a/lib/dag.ml b/stm/dag.ml index 9622f4c1f..9622f4c1f 100644 --- a/lib/dag.ml +++ b/stm/dag.ml diff --git a/lib/dag.mli b/stm/dag.mli index 702ccd80f..702ccd80f 100644 --- a/lib/dag.mli +++ b/stm/dag.mli diff --git a/toplevel/lemmas.ml b/stm/lemmas.ml index 8f16ad5a4..8f16ad5a4 100644 --- a/toplevel/lemmas.ml +++ b/stm/lemmas.ml diff --git a/toplevel/lemmas.mli b/stm/lemmas.mli index bbe383a85..bbe383a85 100644 --- a/toplevel/lemmas.mli +++ b/stm/lemmas.mli diff --git a/lib/spawned.ml b/stm/spawned.ml index d02594569..d02594569 100644 --- a/lib/spawned.ml +++ b/stm/spawned.ml diff --git a/lib/spawned.mli b/stm/spawned.mli index 18b88dc64..18b88dc64 100644 --- a/lib/spawned.mli +++ b/stm/spawned.mli diff --git a/toplevel/stm.ml b/stm/stm.ml index cc6b7d0c4..e791e37cf 100644 --- a/toplevel/stm.ml +++ b/stm/stm.ml @@ -16,6 +16,10 @@ let pr_err s = Printf.eprintf "%s] %s\n" (process_id ()) s; flush stderr let prerr_endline s = if !Flags.debug then begin pr_err s end else () +let (f_process_error, process_error_hook) = Hook.make () +let ((f_interp : (?verbosely:bool -> ?proof:Proof_global.closed_proof -> + Loc.t * Vernacexpr.vernac_expr -> unit) Hook.value), interp_hook) = Hook.make () + open Vernacexpr open Errors open Pp @@ -48,10 +52,11 @@ let vernac_interp ?proof id { verbose; loc; expr } = Pp.set_id_for_feedback (Interface.State id); Aux_file.record_in_aux_set_at loc; prerr_endline ("interpreting " ^ string_of_ppcmds(pr_vernac expr)); - try Vernacentries.interp ~verbosely:verbose ?proof (loc, expr) + let interp = Hook.get f_interp in + try interp ~verbosely:verbose ?proof (loc, expr) with e -> let e = Errors.push e in - raise (Cerrors.process_vernac_interp_error e) + raise (Hook.get f_process_error e) end (* Wrapper for Vernac.parse_sentence to set the feedback id *) @@ -567,7 +572,7 @@ end = struct (* {{{ *) let loc = Option.default Loc.ghost (Loc.get_loc e) in let msg = string_of_ppcmds (print e) in Pp.feedback ~state_id:id (Interface.ErrorMsg (loc, msg)); - Stateid.add (Cerrors.process_vernac_interp_error e) ?valid id + Stateid.add (Hook.get f_process_error e) ?valid id let define ?(redefine=false) ?(cache=`No) f id = let str_id = Stateid.to_string id in @@ -2065,8 +2070,6 @@ let show_script ?proof () = msg_notice (v 0 (Pp.prlist_with_sep Pp.fnl (fun x -> x) indented_cmds)) with Vcs_aux.Expired -> () -let () = Vernacentries.show_script := show_script - (* }}} *) (* vim:set foldmethod=marker: *) diff --git a/toplevel/stm.mli b/stm/stm.mli index 3414ba4f4..a58100b5a 100644 --- a/toplevel/stm.mli +++ b/stm/stm.mli @@ -77,4 +77,9 @@ val interp : bool -> located_vernac_expr -> unit val current_proof_depth : unit -> int val get_all_proof_names : unit -> Id.t list val get_current_proof_name : unit -> Id.t option +val show_script : ?proof:Proof_global.closed_proof -> unit -> unit +(** Reverse dependency hooks *) +val process_error_hook : (exn -> exn) Hook.t +val interp_hook : (?verbosely:bool -> ?proof:Proof_global.closed_proof -> + Loc.t * Vernacexpr.vernac_expr -> unit) Hook.t diff --git a/stm/stm.mllib b/stm/stm.mllib new file mode 100644 index 000000000..347416099 --- /dev/null +++ b/stm/stm.mllib @@ -0,0 +1,9 @@ +Spawned +Dag +Vcs +TQueue +WorkerPool +Vernac_classifier +Lemmas +Stm +Vi_checking diff --git a/lib/tQueue.ml b/stm/tQueue.ml index 783c545fd..783c545fd 100644 --- a/lib/tQueue.ml +++ b/stm/tQueue.ml diff --git a/lib/tQueue.mli b/stm/tQueue.mli index a3ea5532f..a3ea5532f 100644 --- a/lib/tQueue.mli +++ b/stm/tQueue.mli diff --git a/lib/vcs.ml b/stm/vcs.ml index e2513b1c1..e2513b1c1 100644 --- a/lib/vcs.ml +++ b/stm/vcs.ml diff --git a/lib/vcs.mli b/stm/vcs.mli index 6c3571a08..6c3571a08 100644 --- a/lib/vcs.mli +++ b/stm/vcs.mli diff --git a/toplevel/vernac_classifier.ml b/stm/vernac_classifier.ml index 49cbcd246..49cbcd246 100644 --- a/toplevel/vernac_classifier.ml +++ b/stm/vernac_classifier.ml diff --git a/toplevel/vernac_classifier.mli b/stm/vernac_classifier.mli index bc0c0c2b3..bc0c0c2b3 100644 --- a/toplevel/vernac_classifier.mli +++ b/stm/vernac_classifier.mli diff --git a/toplevel/vi_checking.ml b/stm/vi_checking.ml index cb6e60136..cb6e60136 100644 --- a/toplevel/vi_checking.ml +++ b/stm/vi_checking.ml diff --git a/toplevel/vi_checking.mli b/stm/vi_checking.mli index 65414eda4..65414eda4 100644 --- a/toplevel/vi_checking.mli +++ b/stm/vi_checking.mli diff --git a/lib/workerPool.ml b/stm/workerPool.ml index fcae4f20d..fcae4f20d 100644 --- a/lib/workerPool.ml +++ b/stm/workerPool.ml diff --git a/lib/workerPool.mli b/stm/workerPool.mli index d7a546929..d7a546929 100644 --- a/lib/workerPool.mli +++ b/stm/workerPool.mli diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index d348ce747..a5519d586 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -5,7 +5,6 @@ Locality Metasyntax Auto_ind_decl Search -Lemmas Indschemes Obligations Command @@ -14,10 +13,7 @@ Record Vernacinterp Mltop Vernacentries -Vernac_classifier -Stm Whelp -Vi_checking Vernac Ide_slave Usage diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 22e2f0c54..d5559f976 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -495,12 +495,11 @@ let vernac_start_proof kind l lettop = start_proof_and_print (Global, Proof kind) l no_hook let qed_display_script = ref true -let show_script = ref (fun ?proof () -> ()) let vernac_end_proof ?proof = function | Admitted -> save_proof ?proof Admitted | Proved (_,_) as e -> - if is_verbose () && !qed_display_script then !show_script ?proof (); + if is_verbose () && !qed_display_script then Stm.show_script ?proof (); save_proof ?proof e (* A stupid macro that should be replaced by ``Exact c. Save.'' all along @@ -1594,7 +1593,7 @@ let vernac_show = function Constrextern.with_implicits msg_notice (pr_nth_open_subgoal n) | ShowProof -> show_proof () | ShowNode -> show_node () - | ShowScript -> !show_script () + | ShowScript -> Stm.show_script () | ShowExistentials -> show_top_evars () | ShowTree -> show_prooftree () | ShowProofNames -> @@ -1956,3 +1955,5 @@ let interp ?(verbosely=true) ?proof (loc,c) = if verbosely then Flags.verbosely (aux false) c else aux false c +let () = Hook.set Stm.interp_hook interp +let () = Hook.set Stm.process_error_hook Cerrors.process_vernac_interp_error diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index 9b49e5772..3fb3d001d 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -12,7 +12,6 @@ val dump_global : Libnames.reference or_by_notation -> unit (** Vernacular entries *) -val show_script : (?proof:Proof_global.closed_proof -> unit -> unit) ref val show_prooftree : unit -> unit val show_node : unit -> unit |