aboutsummaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
2013-05-06New module Xml_printer (dual to Xml_parser)gareuselesinge
Code for printing XML moved from xml_utils.ml to xml_printer.ml and improved to generate less garbage using Buffer.t systematically. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16480 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-05Now printing body of abbreviations (i.e. notation with a name) withherbelin
full usage of notations instead of the previous cheap way to prevent circularity in printing by deactivating all notations. (Since "->" became a notation, printing abbreviations without notations at all had become even more inconvenient). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16470 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-25Coqide: Globalization feedback (proof of concept)gareuselesinge
A new feedback message for globalization infos can be sent by Coq to Coqide. Coqide stores the information in the proof of concept module wg_Tooltip, that also sets things up so that these infos are displayed as a tooltip when the mouse is over the text they are attached to. These infos are available only on locked text, and on the text just processed in the case of an error (on this piece of text, they vanish as the error tag vanishes as soon as the user edits the text). wg_Tooltip stocks these infos as lazy string. This is not needed in the proof of concept, but is necessary to scale up: Coq may not generate the full piece of info when the message is sent (because of high computational cost or big size) and just send an id; later on, when/if the user asks for the piece of info, the gui requests the info explicitly using the id. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16456 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-25Flag ide_slave moved into Flags modulegareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16454 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-25raise UnsafeSuccess -> feedback AddedAxiomgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16452 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-25Coqide: new feedback mechanism for structured contentgareuselesinge
This amounts to a new type of message called "feedback" and defined in Interface to hold structured data. Coq sends feedback messages asynchronously (they are all fetched, like regular messages, together with the main response to a call) and they are related to a specific sentence by an id. Other changes: - CoqOps pushes the sentence to be processed onto the cmd_stack before processing it and pulls it back if Coq.intep fails, in this way the handler for feedback messages can just look at the cmd_stack to find the offset of the sentence to eventually apply the new Gtk.tag. - The class coqops takes in input a coqtop to set its feedback_handle. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16451 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-25Fix indentationgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16450 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-23Remove deprecated option -no-hash-consing (currently doing nothing)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16442 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-19interface.mli and serialize.ml reworked to avoid copy/paste of typesgareuselesinge
With this commit the types involved in the protocol between Coq and Coqide are written once and for all in interface.mli serialize.ml is monkey code that contains a reified version of these types and the related machinery needed to marshal values in these types to/from xml in a modular way. This file should be automatically generated from the spec of the protocol in an ideal world. Phantom types are used to statically check that the reified form of the types is in sync with the one declared in interface.mli The benefit of this commit is that changing the protocol is easier: one changes the types in interface.mli and lets ocamlc spot all the places that needs to be modified. This is a necessity if one plays with the protocol very often, like in my Paral-ITP branch. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16438 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-16More in IArrayppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16408 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-15votour: a small tool for guided tours of .voletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16403 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-15More functional implementation of locality_flag and program_modegareuselesinge
This commit introduces 2 new vernac_expr constructors: - VernacLocal (b,v) that represents a vernacular v with the "Local" modifier - VernacProgram v that represents a vernacular v with the "Program" modifier This allows the parser to avoid using side effects to model the two modifiers, that are now represented in the AST. This also decouples the parsing phase from the interpretation phase, since parsing a second phrase does not alter the locality flag for the first phrase. As a consequence all the locality_flag components of vernac_expr have been removed, but for the ones that (for retro compatibility) allow an "infix" Local flag. In these cases the boolean is renamed obsolete_locality (as the grammar entry that parses it), and during interpretation we check that at most one locality flag is specified, using the idiom (where the input local is the obsolete one): let local = enforce_XXX_locality locality local in Another improvement is that the default locality is not chosen in the parser, but in the interpreter where the idiom let local = make_XXX_locality locality in is used to default the locality to XXX (module/section/whatever). Unfortunately not all side effects have been removed: - Flags.program_mode is still used to signal that we are in program mode - Locality.LocalityFixme.* functions are used in commands that do not have an AST, but are parsed as VernacExtend (see vernacinterp.ml) I guess one could fix the latter case systematically adding an extra argument "locality" to commands attached using VERNAC COMMAND EXTEND. Fixing plugins adding commands that honour "Local" should look like this: VERNAC COMMAND EXTEND Set_Solver | [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ set_default_tactic - (Locality.use_section_locality ()) + (Locality.make_section_locality (Locality.LocalityFixme.consume ())) (Tacintern.glob_tactic t) ] END In any case the side effects are set/consumed within then interpretation phase, and not set during the parsing phase and consumed during the interpretation phase. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16396 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-09Added a module of immutable arrays. Not as full as CArray, but shouldppedrot
be soon. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16391 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-23Minor code cleaning in CArray / CList.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16351 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-21Removing mandatory suffixes for library files.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16332 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-17Checker: simplify a bit its exception handlerletouzey
We use Errors.print for anomalies and other uncaught exceptions in the checker: this should print the same message, it is shorter this way, and we avoid using Errors.is_anomaly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16310 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-14Embedded exns in LtacLocated and EvaluatedError satisfy Errors.noncriticalletouzey
This was apparently already the case before, but this invariant is now explicited in comments + a few asserts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16305 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Made the backtrace type opaqueppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16298 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Vernac+Toplevel: get rid of Error_in_fileletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16294 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 13)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16290 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 8)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16284 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 5)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16281 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12Restrict (try...with...) to avoid catching critical exn (part 4)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16280 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12invalid_arg instead of raise (Invalid_argement ...)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16270 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12New function Errors.noncritical for restricting try ... with ...letouzey
For the moment, are considered critical : Sys.Break, Stack_overflow, Out_of_memory Assert_failure, Match_failure, Anomaly, Timeout, Drop, Exit These exceptions should normally *not* be catched by a "try", hence the suggested code for generic "try": try ... with e when Errors.noncritical e -> ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16269 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12Updated Exninfo to the new Store type.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16268 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12Allowing different types of, not to be mixed, generic Stores throughppedrot
functor application. Rewritten the interface btw. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16267 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-05More monomorphization.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16260 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-05Missing primitive in CArrayppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16259 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-24New -no-native-compiler flag for configure, globally disabling the nativemdenes
compiler (implemented on Matthieu's request). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16240 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-18Removing Exc_located and using the new exception enrichementppedrot
mechanism to retrieve the same information. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16215 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-18Adding more primitives to Exninfoppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16214 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-18Updating the backtrace handling mechanism to accomodate the newppedrot
exception information addition facility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16213 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-18Added exception enrichment. Now one can define additional arbitraryppedrot
information worn by exceptions. The implementation is quite hackish but it should work nonetheless. Basically, it adds an additional cell to exceptions arguments, in which you can put whatever you want. By typing invariants, you may not reach this cell by normal means, so it should be safe. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16212 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-01v8.4: Granting bug/wish #2976 (turning anomaly on input_value into nice message)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16183 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-28Actually adding backtrace handling.ppedrot
I hope I did not forget some [with] clauses. Otherwise, some stack frame will be missing from the debug. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16167 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-28Added backtrace primitives.ppedrot
Using OCaml 3.11+ builtin facilities to record stack frames during exception raising, we can now recover at runtime the backtrace of an uncaught toplevel exception and display it to the user, without the infamous OCaml debugger. The backtrace is displayed when using the [-debug] flag. This requires a bit of discipline, as each time we reraise an exception we need to keep track of those frames we discarded between the previous raise and the current [try-with] branch. Currently, only [Anomaly] is handled, but this can be ported to any exception as long as we add the backtrace info into the exception, and we provide the corresponding handler to [Backtracke.register_backtrace_handler]. Hopefully this should not be to costly, as we only do little work when reraising, and only with the [-debug] flag set. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16166 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-28Uniformization of the "anomaly" command.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-28Added backtrace information to anomaliesppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16161 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
native OCaml code. Warning: the "retroknowledge" mechanism has not been ported to the native compiler, because integers and persistent arrays will ultimately be defined as primitive constructions. Until then, computation on numbers may be faster using the VM, since it takes advantage of machine integers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16136 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-12Envar: in w32, add .exe when searching for caml binariesletouzey
Based on a patch by Pierre-Yves Strub git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16124 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-19Array.create is deprecatedpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16104 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-19Fix coqtop -config when absolute path have been given for ocaml*pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16102 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14Moving hcons_string to String namespace.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16069 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14Moved Stringset and Stringmap to String namespace.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16068 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14Moved Intset and Intmap to Int namespace.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16067 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-13Documented CString.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16064 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-13Renamed Option.Misc.compare to the more uniform Option.equal.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16063 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-08Ensure that a function declared with a label is used with itletouzey
This correspond to ocaml4 warning 6 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16053 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-08Removed a unused function in Ppppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16048 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 04:49:05 +0000